ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1827

User:	Jiri Slaby
Error type:	Reachable Error Location
Error type description:	A specified error location is reachable in some program path
File location:	product-lines/email_spec9_product16_unsafe.cil.c
Line in file:	2226
Project:	SV-COMP 2013
Project version:	2.6.28
Tools:	Manual Work
Entered:	2013-01-17 16:57:54 UTC
Source:

   1extern int __VERIFIER_nondet_int(void);
   2/* Generated by CIL v. 1.3.7 */
   3/* print_CIL_Input is true */
   4
   5#line 2 "libacc.c"
   6struct JoinPoint {
   7   void **(*fp)(struct JoinPoint * ) ;
   8   void **args ;
   9   int argsCount ;
  10   char const   **argsType ;
  11   void *(*arg)(int  , struct JoinPoint * ) ;
  12   char const   *(*argType)(int  , struct JoinPoint * ) ;
  13   void **retValue ;
  14   char const   *retType ;
  15   char const   *funcName ;
  16   char const   *targetName ;
  17   char const   *fileName ;
  18   char const   *kind ;
  19   void *excep_return ;
  20};
  21#line 18 "libacc.c"
  22struct __UTAC__CFLOW_FUNC {
  23   int (*func)(int  , int  ) ;
  24   int val ;
  25   struct __UTAC__CFLOW_FUNC *next ;
  26};
  27#line 18 "libacc.c"
  28struct __UTAC__EXCEPTION {
  29   void *jumpbuf ;
  30   unsigned long long prtValue ;
  31   int pops ;
  32   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
  33};
  34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
  35typedef unsigned long size_t;
  36#line 76 "libacc.c"
  37struct __ACC__ERR {
  38   void *v ;
  39   struct __ACC__ERR *next ;
  40};
  41#line 1 "EncryptForward_spec.o"
  42#pragma merger(0,"EncryptForward_spec.i","")
  43#line 4 "wsllib.h"
  44void __automaton_fail(void) ;
  45#line 8 "featureselect.h"
  46int __SELECTED_FEATURE_Base  ;
  47#line 11 "featureselect.h"
  48int __SELECTED_FEATURE_Keys  ;
  49#line 14 "featureselect.h"
  50int __SELECTED_FEATURE_Encrypt  ;
  51#line 17 "featureselect.h"
  52int __SELECTED_FEATURE_AutoResponder  ;
  53#line 20 "featureselect.h"
  54int __SELECTED_FEATURE_AddressBook  ;
  55#line 23 "featureselect.h"
  56int __SELECTED_FEATURE_Sign  ;
  57#line 26 "featureselect.h"
  58int __SELECTED_FEATURE_Forward  ;
  59#line 29 "featureselect.h"
  60int __SELECTED_FEATURE_Verify  ;
  61#line 32 "featureselect.h"
  62int __SELECTED_FEATURE_Decrypt  ;
  63#line 35 "featureselect.h"
  64int __GUIDSL_ROOT_PRODUCTION  ;
  65#line 37 "featureselect.h"
  66int __GUIDSL_NON_TERMINAL_main  ;
  67#line 26 "EmailLib.h"
  68int isEncrypted(int handle ) ;
  69#line 359 "/usr/include/stdio.h"
  70extern int printf(char const   * __restrict  __format  , ...) ;
  71#line 688
  72extern int puts(char const   *__s ) ;
  73#line 7 "EncryptForward_spec.c"
  74int in_encrypted  =    0;
  75#line 11 "EncryptForward_spec.c"
  76__inline void __utac_acc__EncryptForward_spec__1(int msg ) 
  77{ char const   * __restrict  __cil_tmp2 ;
  78
  79  {
  80  {
  81#line 13
  82  puts("before incoming\n");
  83#line 14
  84  in_encrypted = isEncrypted(msg);
  85#line 15
  86  __cil_tmp2 = (char const   * __restrict  )"in_encrypted=%d\n";
  87#line 15
  88  printf(__cil_tmp2, in_encrypted);
  89  }
  90#line 15
  91  return;
  92}
  93}
  94#line 19 "EncryptForward_spec.c"
  95__inline void __utac_acc__EncryptForward_spec__2(int msg ) 
  96{ int tmp ;
  97  char const   * __restrict  __cil_tmp3 ;
  98
  99  {
 100  {
 101#line 21
 102  puts("before mail\n");
 103#line 22
 104  __cil_tmp3 = (char const   * __restrict  )"in_encrypted=%d\n";
 105#line 22
 106  printf(__cil_tmp3, in_encrypted);
 107  }
 108#line 23
 109  if (in_encrypted) {
 110    {
 111#line 23
 112    tmp = isEncrypted(msg);
 113    }
 114#line 23
 115    if (tmp) {
 116
 117    } else {
 118      {
 119#line 24
 120      __automaton_fail();
 121      }
 122    }
 123  } else {
 124
 125  }
 126#line 24
 127  return;
 128}
 129}
 130#line 1 "Email.o"
 131#pragma merger(0,"Email.i","")
 132#line 6 "EmailLib.h"
 133int getEmailId(int handle ) ;
 134#line 10
 135int getEmailFrom(int handle ) ;
 136#line 12
 137void setEmailFrom(int handle , int value ) ;
 138#line 14
 139int getEmailTo(int handle ) ;
 140#line 16
 141void setEmailTo(int handle , int value ) ;
 142#line 30
 143int getEmailEncryptionKey(int handle ) ;
 144#line 6 "Email.h"
 145void printMail(int msg ) ;
 146#line 9
 147int isReadable(int msg ) ;
 148#line 12
 149int createEmail(int from , int to ) ;
 150#line 15
 151int cloneEmail(int msg ) ;
 152#line 9 "Email.c"
 153void printMail__wrappee__Keys(int msg ) 
 154{ int tmp ;
 155  int tmp___0 ;
 156  int tmp___1 ;
 157  int tmp___2 ;
 158  char const   * __restrict  __cil_tmp6 ;
 159  char const   * __restrict  __cil_tmp7 ;
 160  char const   * __restrict  __cil_tmp8 ;
 161  char const   * __restrict  __cil_tmp9 ;
 162
 163  {
 164  {
 165#line 10
 166  tmp = getEmailId(msg);
 167#line 10
 168  __cil_tmp6 = (char const   * __restrict  )"ID:\n  %i\n";
 169#line 10
 170  printf(__cil_tmp6, tmp);
 171#line 11
 172  tmp___0 = getEmailFrom(msg);
 173#line 11
 174  __cil_tmp7 = (char const   * __restrict  )"FROM:\n  %i\n";
 175#line 11
 176  printf(__cil_tmp7, tmp___0);
 177#line 12
 178  tmp___1 = getEmailTo(msg);
 179#line 12
 180  __cil_tmp8 = (char const   * __restrict  )"TO:\n  %i\n";
 181#line 12
 182  printf(__cil_tmp8, tmp___1);
 183#line 13
 184  tmp___2 = isReadable(msg);
 185#line 13
 186  __cil_tmp9 = (char const   * __restrict  )"IS_READABLE\n  %i\n";
 187#line 13
 188  printf(__cil_tmp9, tmp___2);
 189  }
 190#line 601 "Email.c"
 191  return;
 192}
 193}
 194#line 17 "Email.c"
 195void printMail(int msg ) 
 196{ int tmp ;
 197  int tmp___0 ;
 198  char const   * __restrict  __cil_tmp4 ;
 199  char const   * __restrict  __cil_tmp5 ;
 200
 201  {
 202  {
 203#line 18
 204  printMail__wrappee__Keys(msg);
 205#line 19
 206  tmp = isEncrypted(msg);
 207#line 19
 208  __cil_tmp4 = (char const   * __restrict  )"ENCRYPTED\n  %d\n";
 209#line 19
 210  printf(__cil_tmp4, tmp);
 211#line 20
 212  tmp___0 = getEmailEncryptionKey(msg);
 213#line 20
 214  __cil_tmp5 = (char const   * __restrict  )"ENCRYPTION KEY\n  %d\n";
 215#line 20
 216  printf(__cil_tmp5, tmp___0);
 217  }
 218#line 625 "Email.c"
 219  return;
 220}
 221}
 222#line 26 "Email.c"
 223int isReadable__wrappee__Keys(int msg ) 
 224{ int retValue_acc ;
 225
 226  {
 227#line 643 "Email.c"
 228  retValue_acc = 1;
 229#line 645
 230  return (retValue_acc);
 231#line 652
 232  return (retValue_acc);
 233}
 234}
 235#line 34 "Email.c"
 236int isReadable(int msg ) 
 237{ int retValue_acc ;
 238  int tmp ;
 239
 240  {
 241  {
 242#line 38
 243  tmp = isEncrypted(msg);
 244  }
 245#line 38 "Email.c"
 246  if (tmp) {
 247#line 681
 248    retValue_acc = 0;
 249#line 683
 250    return (retValue_acc);
 251  } else {
 252    {
 253#line 675 "Email.c"
 254    retValue_acc = isReadable__wrappee__Keys(msg);
 255    }
 256#line 677
 257    return (retValue_acc);
 258  }
 259#line 690 "Email.c"
 260  return (retValue_acc);
 261}
 262}
 263#line 42 "Email.c"
 264int cloneEmail(int msg ) 
 265{ int retValue_acc ;
 266
 267  {
 268#line 712 "Email.c"
 269  retValue_acc = msg;
 270#line 714
 271  return (retValue_acc);
 272#line 721
 273  return (retValue_acc);
 274}
 275}
 276#line 47 "Email.c"
 277int createEmail(int from , int to ) 
 278{ int retValue_acc ;
 279  int msg ;
 280
 281  {
 282  {
 283#line 48
 284  msg = 1;
 285#line 49
 286  setEmailFrom(msg, from);
 287#line 50
 288  setEmailTo(msg, to);
 289#line 751 "Email.c"
 290  retValue_acc = msg;
 291  }
 292#line 753
 293  return (retValue_acc);
 294#line 760
 295  return (retValue_acc);
 296}
 297}
 298#line 1 "Util.o"
 299#pragma merger(0,"Util.i","")
 300#line 1 "Util.h"
 301int prompt(char *msg ) ;
 302#line 9 "Util.c"
 303int prompt(char *msg ) 
 304{ int retValue_acc ;
 305  int retval ;
 306  char const   * __restrict  __cil_tmp4 ;
 307
 308  {
 309  {
 310#line 10
 311  __cil_tmp4 = (char const   * __restrict  )"%s\n";
 312#line 10
 313  printf(__cil_tmp4, msg);
 314#line 518 "Util.c"
 315  retValue_acc = retval;
 316  }
 317#line 520
 318  return (retValue_acc);
 319#line 527
 320  return (retValue_acc);
 321}
 322}
 323#line 1 "libacc.o"
 324#pragma merger(0,"libacc.i","")
 325#line 73 "/usr/include/assert.h"
 326extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 327                                                                      char const   *__file ,
 328                                                                      unsigned int __line ,
 329                                                                      char const   *__function ) ;
 330#line 471 "/usr/include/stdlib.h"
 331extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 332#line 488
 333extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
 334#line 32 "libacc.c"
 335void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int  ,
 336                                                                           int  ) ,
 337                                       int val ) 
 338{ struct __UTAC__EXCEPTION *excep ;
 339  struct __UTAC__CFLOW_FUNC *cf ;
 340  void *tmp ;
 341  unsigned long __cil_tmp7 ;
 342  unsigned long __cil_tmp8 ;
 343  unsigned long __cil_tmp9 ;
 344  unsigned long __cil_tmp10 ;
 345  unsigned long __cil_tmp11 ;
 346  unsigned long __cil_tmp12 ;
 347  unsigned long __cil_tmp13 ;
 348  unsigned long __cil_tmp14 ;
 349  int (**mem_15)(int  , int  ) ;
 350  int *mem_16 ;
 351  struct __UTAC__CFLOW_FUNC **mem_17 ;
 352  struct __UTAC__CFLOW_FUNC **mem_18 ;
 353  struct __UTAC__CFLOW_FUNC **mem_19 ;
 354
 355  {
 356  {
 357#line 33
 358  excep = (struct __UTAC__EXCEPTION *)exception;
 359#line 34
 360  tmp = malloc(24UL);
 361#line 34
 362  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
 363#line 36
 364  mem_15 = (int (**)(int  , int  ))cf;
 365#line 36
 366  *mem_15 = cflow_func;
 367#line 37
 368  __cil_tmp7 = (unsigned long )cf;
 369#line 37
 370  __cil_tmp8 = __cil_tmp7 + 8;
 371#line 37
 372  mem_16 = (int *)__cil_tmp8;
 373#line 37
 374  *mem_16 = val;
 375#line 38
 376  __cil_tmp9 = (unsigned long )cf;
 377#line 38
 378  __cil_tmp10 = __cil_tmp9 + 16;
 379#line 38
 380  __cil_tmp11 = (unsigned long )excep;
 381#line 38
 382  __cil_tmp12 = __cil_tmp11 + 24;
 383#line 38
 384  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
 385#line 38
 386  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
 387#line 38
 388  *mem_17 = *mem_18;
 389#line 39
 390  __cil_tmp13 = (unsigned long )excep;
 391#line 39
 392  __cil_tmp14 = __cil_tmp13 + 24;
 393#line 39
 394  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
 395#line 39
 396  *mem_19 = cf;
 397  }
 398#line 654 "libacc.c"
 399  return;
 400}
 401}
 402#line 44 "libacc.c"
 403void __utac__exception__cf_handler_free(void *exception ) 
 404{ struct __UTAC__EXCEPTION *excep ;
 405  struct __UTAC__CFLOW_FUNC *cf ;
 406  struct __UTAC__CFLOW_FUNC *tmp ;
 407  unsigned long __cil_tmp5 ;
 408  unsigned long __cil_tmp6 ;
 409  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
 410  unsigned long __cil_tmp8 ;
 411  unsigned long __cil_tmp9 ;
 412  unsigned long __cil_tmp10 ;
 413  unsigned long __cil_tmp11 ;
 414  void *__cil_tmp12 ;
 415  unsigned long __cil_tmp13 ;
 416  unsigned long __cil_tmp14 ;
 417  struct __UTAC__CFLOW_FUNC **mem_15 ;
 418  struct __UTAC__CFLOW_FUNC **mem_16 ;
 419  struct __UTAC__CFLOW_FUNC **mem_17 ;
 420
 421  {
 422#line 45
 423  excep = (struct __UTAC__EXCEPTION *)exception;
 424#line 46
 425  __cil_tmp5 = (unsigned long )excep;
 426#line 46
 427  __cil_tmp6 = __cil_tmp5 + 24;
 428#line 46
 429  mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
 430#line 46
 431  cf = *mem_15;
 432  {
 433#line 49
 434  while (1) {
 435    while_0_continue: /* CIL Label */ ;
 436    {
 437#line 49
 438    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
 439#line 49
 440    __cil_tmp8 = (unsigned long )__cil_tmp7;
 441#line 49
 442    __cil_tmp9 = (unsigned long )cf;
 443#line 49
 444    if (__cil_tmp9 != __cil_tmp8) {
 445
 446    } else {
 447      goto while_0_break;
 448    }
 449    }
 450    {
 451#line 50
 452    tmp = cf;
 453#line 51
 454    __cil_tmp10 = (unsigned long )cf;
 455#line 51
 456    __cil_tmp11 = __cil_tmp10 + 16;
 457#line 51
 458    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
 459#line 51
 460    cf = *mem_16;
 461#line 52
 462    __cil_tmp12 = (void *)tmp;
 463#line 52
 464    free(__cil_tmp12);
 465    }
 466  }
 467  while_0_break: /* CIL Label */ ;
 468  }
 469#line 55
 470  __cil_tmp13 = (unsigned long )excep;
 471#line 55
 472  __cil_tmp14 = __cil_tmp13 + 24;
 473#line 55
 474  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
 475#line 55
 476  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
 477#line 694 "libacc.c"
 478  return;
 479}
 480}
 481#line 59 "libacc.c"
 482void __utac__exception__cf_handler_reset(void *exception ) 
 483{ struct __UTAC__EXCEPTION *excep ;
 484  struct __UTAC__CFLOW_FUNC *cf ;
 485  unsigned long __cil_tmp5 ;
 486  unsigned long __cil_tmp6 ;
 487  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
 488  unsigned long __cil_tmp8 ;
 489  unsigned long __cil_tmp9 ;
 490  int (*__cil_tmp10)(int  , int  ) ;
 491  unsigned long __cil_tmp11 ;
 492  unsigned long __cil_tmp12 ;
 493  int __cil_tmp13 ;
 494  unsigned long __cil_tmp14 ;
 495  unsigned long __cil_tmp15 ;
 496  struct __UTAC__CFLOW_FUNC **mem_16 ;
 497  int (**mem_17)(int  , int  ) ;
 498  int *mem_18 ;
 499  struct __UTAC__CFLOW_FUNC **mem_19 ;
 500
 501  {
 502#line 60
 503  excep = (struct __UTAC__EXCEPTION *)exception;
 504#line 61
 505  __cil_tmp5 = (unsigned long )excep;
 506#line 61
 507  __cil_tmp6 = __cil_tmp5 + 24;
 508#line 61
 509  mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
 510#line 61
 511  cf = *mem_16;
 512  {
 513#line 64
 514  while (1) {
 515    while_1_continue: /* CIL Label */ ;
 516    {
 517#line 64
 518    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
 519#line 64
 520    __cil_tmp8 = (unsigned long )__cil_tmp7;
 521#line 64
 522    __cil_tmp9 = (unsigned long )cf;
 523#line 64
 524    if (__cil_tmp9 != __cil_tmp8) {
 525
 526    } else {
 527      goto while_1_break;
 528    }
 529    }
 530    {
 531#line 65
 532    mem_17 = (int (**)(int  , int  ))cf;
 533#line 65
 534    __cil_tmp10 = *mem_17;
 535#line 65
 536    __cil_tmp11 = (unsigned long )cf;
 537#line 65
 538    __cil_tmp12 = __cil_tmp11 + 8;
 539#line 65
 540    mem_18 = (int *)__cil_tmp12;
 541#line 65
 542    __cil_tmp13 = *mem_18;
 543#line 65
 544    (*__cil_tmp10)(4, __cil_tmp13);
 545#line 66
 546    __cil_tmp14 = (unsigned long )cf;
 547#line 66
 548    __cil_tmp15 = __cil_tmp14 + 16;
 549#line 66
 550    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
 551#line 66
 552    cf = *mem_19;
 553    }
 554  }
 555  while_1_break: /* CIL Label */ ;
 556  }
 557  {
 558#line 69
 559  __utac__exception__cf_handler_free(exception);
 560  }
 561#line 732 "libacc.c"
 562  return;
 563}
 564}
 565#line 80 "libacc.c"
 566void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
 567#line 80 "libacc.c"
 568static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
 569#line 79 "libacc.c"
 570void *__utac__error_stack_mgt(void *env , int mode , int count ) 
 571{ void *retValue_acc ;
 572  struct __ACC__ERR *new ;
 573  void *tmp ;
 574  struct __ACC__ERR *temp ;
 575  struct __ACC__ERR *next ;
 576  void *excep ;
 577  unsigned long __cil_tmp10 ;
 578  unsigned long __cil_tmp11 ;
 579  unsigned long __cil_tmp12 ;
 580  unsigned long __cil_tmp13 ;
 581  void *__cil_tmp14 ;
 582  unsigned long __cil_tmp15 ;
 583  unsigned long __cil_tmp16 ;
 584  void *__cil_tmp17 ;
 585  void **mem_18 ;
 586  struct __ACC__ERR **mem_19 ;
 587  struct __ACC__ERR **mem_20 ;
 588  void **mem_21 ;
 589  struct __ACC__ERR **mem_22 ;
 590  void **mem_23 ;
 591  void **mem_24 ;
 592
 593  {
 594#line 82 "libacc.c"
 595  if (count == 0) {
 596#line 758 "libacc.c"
 597    return (retValue_acc);
 598  } else {
 599
 600  }
 601#line 86 "libacc.c"
 602  if (mode == 0) {
 603    {
 604#line 87
 605    tmp = malloc(16UL);
 606#line 87
 607    new = (struct __ACC__ERR *)tmp;
 608#line 88
 609    mem_18 = (void **)new;
 610#line 88
 611    *mem_18 = env;
 612#line 89
 613    __cil_tmp10 = (unsigned long )new;
 614#line 89
 615    __cil_tmp11 = __cil_tmp10 + 8;
 616#line 89
 617    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
 618#line 89
 619    *mem_19 = head;
 620#line 90
 621    head = new;
 622#line 776 "libacc.c"
 623    retValue_acc = (void *)new;
 624    }
 625#line 778
 626    return (retValue_acc);
 627  } else {
 628
 629  }
 630#line 94 "libacc.c"
 631  if (mode == 1) {
 632#line 95
 633    temp = head;
 634    {
 635#line 98
 636    while (1) {
 637      while_2_continue: /* CIL Label */ ;
 638#line 98
 639      if (count > 1) {
 640
 641      } else {
 642        goto while_2_break;
 643      }
 644      {
 645#line 99
 646      __cil_tmp12 = (unsigned long )temp;
 647#line 99
 648      __cil_tmp13 = __cil_tmp12 + 8;
 649#line 99
 650      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
 651#line 99
 652      next = *mem_20;
 653#line 100
 654      mem_21 = (void **)temp;
 655#line 100
 656      excep = *mem_21;
 657#line 101
 658      __cil_tmp14 = (void *)temp;
 659#line 101
 660      free(__cil_tmp14);
 661#line 102
 662      __utac__exception__cf_handler_reset(excep);
 663#line 103
 664      temp = next;
 665#line 104
 666      count = count - 1;
 667      }
 668    }
 669    while_2_break: /* CIL Label */ ;
 670    }
 671    {
 672#line 107
 673    __cil_tmp15 = (unsigned long )temp;
 674#line 107
 675    __cil_tmp16 = __cil_tmp15 + 8;
 676#line 107
 677    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
 678#line 107
 679    head = *mem_22;
 680#line 108
 681    mem_23 = (void **)temp;
 682#line 108
 683    excep = *mem_23;
 684#line 109
 685    __cil_tmp17 = (void *)temp;
 686#line 109
 687    free(__cil_tmp17);
 688#line 110
 689    __utac__exception__cf_handler_reset(excep);
 690#line 820 "libacc.c"
 691    retValue_acc = excep;
 692    }
 693#line 822
 694    return (retValue_acc);
 695  } else {
 696
 697  }
 698#line 114
 699  if (mode == 2) {
 700#line 118 "libacc.c"
 701    if (head) {
 702#line 831
 703      mem_24 = (void **)head;
 704#line 831
 705      retValue_acc = *mem_24;
 706#line 833
 707      return (retValue_acc);
 708    } else {
 709#line 837 "libacc.c"
 710      retValue_acc = (void *)0;
 711#line 839
 712      return (retValue_acc);
 713    }
 714  } else {
 715
 716  }
 717#line 846 "libacc.c"
 718  return (retValue_acc);
 719}
 720}
 721#line 122 "libacc.c"
 722void *__utac__get_this_arg(int i , struct JoinPoint *this ) 
 723{ void *retValue_acc ;
 724  unsigned long __cil_tmp4 ;
 725  unsigned long __cil_tmp5 ;
 726  int __cil_tmp6 ;
 727  int __cil_tmp7 ;
 728  unsigned long __cil_tmp8 ;
 729  unsigned long __cil_tmp9 ;
 730  void **__cil_tmp10 ;
 731  void **__cil_tmp11 ;
 732  int *mem_12 ;
 733  void ***mem_13 ;
 734
 735  {
 736#line 123
 737  if (i > 0) {
 738    {
 739#line 123
 740    __cil_tmp4 = (unsigned long )this;
 741#line 123
 742    __cil_tmp5 = __cil_tmp4 + 16;
 743#line 123
 744    mem_12 = (int *)__cil_tmp5;
 745#line 123
 746    __cil_tmp6 = *mem_12;
 747#line 123
 748    if (i <= __cil_tmp6) {
 749
 750    } else {
 751      {
 752#line 123
 753      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
 754                    123U, "__utac__get_this_arg");
 755      }
 756    }
 757    }
 758  } else {
 759    {
 760#line 123
 761    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
 762                  123U, "__utac__get_this_arg");
 763    }
 764  }
 765#line 870 "libacc.c"
 766  __cil_tmp7 = i - 1;
 767#line 870
 768  __cil_tmp8 = (unsigned long )this;
 769#line 870
 770  __cil_tmp9 = __cil_tmp8 + 8;
 771#line 870
 772  mem_13 = (void ***)__cil_tmp9;
 773#line 870
 774  __cil_tmp10 = *mem_13;
 775#line 870
 776  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
 777#line 870
 778  retValue_acc = *__cil_tmp11;
 779#line 872
 780  return (retValue_acc);
 781#line 879
 782  return (retValue_acc);
 783}
 784}
 785#line 129 "libacc.c"
 786char const   *__utac__get_this_argtype(int i , struct JoinPoint *this ) 
 787{ char const   *retValue_acc ;
 788  unsigned long __cil_tmp4 ;
 789  unsigned long __cil_tmp5 ;
 790  int __cil_tmp6 ;
 791  int __cil_tmp7 ;
 792  unsigned long __cil_tmp8 ;
 793  unsigned long __cil_tmp9 ;
 794  char const   **__cil_tmp10 ;
 795  char const   **__cil_tmp11 ;
 796  int *mem_12 ;
 797  char const   ***mem_13 ;
 798
 799  {
 800#line 131
 801  if (i > 0) {
 802    {
 803#line 131
 804    __cil_tmp4 = (unsigned long )this;
 805#line 131
 806    __cil_tmp5 = __cil_tmp4 + 16;
 807#line 131
 808    mem_12 = (int *)__cil_tmp5;
 809#line 131
 810    __cil_tmp6 = *mem_12;
 811#line 131
 812    if (i <= __cil_tmp6) {
 813
 814    } else {
 815      {
 816#line 131
 817      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
 818                    131U, "__utac__get_this_argtype");
 819      }
 820    }
 821    }
 822  } else {
 823    {
 824#line 131
 825    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
 826                  131U, "__utac__get_this_argtype");
 827    }
 828  }
 829#line 903 "libacc.c"
 830  __cil_tmp7 = i - 1;
 831#line 903
 832  __cil_tmp8 = (unsigned long )this;
 833#line 903
 834  __cil_tmp9 = __cil_tmp8 + 24;
 835#line 903
 836  mem_13 = (char const   ***)__cil_tmp9;
 837#line 903
 838  __cil_tmp10 = *mem_13;
 839#line 903
 840  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
 841#line 903
 842  retValue_acc = *__cil_tmp11;
 843#line 905
 844  return (retValue_acc);
 845#line 912
 846  return (retValue_acc);
 847}
 848}
 849#line 1 "EmailLib.o"
 850#pragma merger(0,"EmailLib.i","")
 851#line 4 "EmailLib.h"
 852int initEmail(void) ;
 853#line 8
 854void setEmailId(int handle , int value ) ;
 855#line 18
 856char *getEmailSubject(int handle ) ;
 857#line 20
 858void setEmailSubject(int handle , char *value ) ;
 859#line 22
 860char *getEmailBody(int handle ) ;
 861#line 24
 862void setEmailBody(int handle , char *value ) ;
 863#line 28
 864void setEmailIsEncrypted(int handle , int value ) ;
 865#line 32
 866void setEmailEncryptionKey(int handle , int value ) ;
 867#line 34
 868int isSigned(int handle ) ;
 869#line 36
 870void setEmailIsSigned(int handle , int value ) ;
 871#line 38
 872int getEmailSignKey(int handle ) ;
 873#line 40
 874void setEmailSignKey(int handle , int value ) ;
 875#line 42
 876int isVerified(int handle ) ;
 877#line 44
 878void setEmailIsSignatureVerified(int handle , int value ) ;
 879#line 5 "EmailLib.c"
 880int __ste_Email_counter  =    0;
 881#line 7 "EmailLib.c"
 882int initEmail(void) 
 883{ int retValue_acc ;
 884
 885  {
 886#line 12 "EmailLib.c"
 887  if (__ste_Email_counter < 2) {
 888#line 670
 889    __ste_Email_counter = __ste_Email_counter + 1;
 890#line 670
 891    retValue_acc = __ste_Email_counter;
 892#line 672
 893    return (retValue_acc);
 894  } else {
 895#line 678 "EmailLib.c"
 896    retValue_acc = -1;
 897#line 680
 898    return (retValue_acc);
 899  }
 900#line 687 "EmailLib.c"
 901  return (retValue_acc);
 902}
 903}
 904#line 15 "EmailLib.c"
 905int __ste_email_id0  =    0;
 906#line 17 "EmailLib.c"
 907int __ste_email_id1  =    0;
 908#line 19 "EmailLib.c"
 909int getEmailId(int handle ) 
 910{ int retValue_acc ;
 911
 912  {
 913#line 26 "EmailLib.c"
 914  if (handle == 1) {
 915#line 716
 916    retValue_acc = __ste_email_id0;
 917#line 718
 918    return (retValue_acc);
 919  } else {
 920#line 720
 921    if (handle == 2) {
 922#line 725
 923      retValue_acc = __ste_email_id1;
 924#line 727
 925      return (retValue_acc);
 926    } else {
 927#line 733 "EmailLib.c"
 928      retValue_acc = 0;
 929#line 735
 930      return (retValue_acc);
 931    }
 932  }
 933#line 742 "EmailLib.c"
 934  return (retValue_acc);
 935}
 936}
 937#line 29 "EmailLib.c"
 938void setEmailId(int handle , int value ) 
 939{ 
 940
 941  {
 942#line 35
 943  if (handle == 1) {
 944#line 31
 945    __ste_email_id0 = value;
 946  } else {
 947#line 32
 948    if (handle == 2) {
 949#line 33
 950      __ste_email_id1 = value;
 951    } else {
 952
 953    }
 954  }
 955#line 773 "EmailLib.c"
 956  return;
 957}
 958}
 959#line 37 "EmailLib.c"
 960int __ste_email_from0  =    0;
 961#line 39 "EmailLib.c"
 962int __ste_email_from1  =    0;
 963#line 41 "EmailLib.c"
 964int getEmailFrom(int handle ) 
 965{ int retValue_acc ;
 966
 967  {
 968#line 48 "EmailLib.c"
 969  if (handle == 1) {
 970#line 798
 971    retValue_acc = __ste_email_from0;
 972#line 800
 973    return (retValue_acc);
 974  } else {
 975#line 802
 976    if (handle == 2) {
 977#line 807
 978      retValue_acc = __ste_email_from1;
 979#line 809
 980      return (retValue_acc);
 981    } else {
 982#line 815 "EmailLib.c"
 983      retValue_acc = 0;
 984#line 817
 985      return (retValue_acc);
 986    }
 987  }
 988#line 824 "EmailLib.c"
 989  return (retValue_acc);
 990}
 991}
 992#line 51 "EmailLib.c"
 993void setEmailFrom(int handle , int value ) 
 994{ 
 995
 996  {
 997#line 57
 998  if (handle == 1) {
 999#line 53
1000    __ste_email_from0 = value;
1001  } else {
1002#line 54
1003    if (handle == 2) {
1004#line 55
1005      __ste_email_from1 = value;
1006    } else {
1007
1008    }
1009  }
1010#line 855 "EmailLib.c"
1011  return;
1012}
1013}
1014#line 59 "EmailLib.c"
1015int __ste_email_to0  =    0;
1016#line 61 "EmailLib.c"
1017int __ste_email_to1  =    0;
1018#line 63 "EmailLib.c"
1019int getEmailTo(int handle ) 
1020{ int retValue_acc ;
1021
1022  {
1023#line 70 "EmailLib.c"
1024  if (handle == 1) {
1025#line 880
1026    retValue_acc = __ste_email_to0;
1027#line 882
1028    return (retValue_acc);
1029  } else {
1030#line 884
1031    if (handle == 2) {
1032#line 889
1033      retValue_acc = __ste_email_to1;
1034#line 891
1035      return (retValue_acc);
1036    } else {
1037#line 897 "EmailLib.c"
1038      retValue_acc = 0;
1039#line 899
1040      return (retValue_acc);
1041    }
1042  }
1043#line 906 "EmailLib.c"
1044  return (retValue_acc);
1045}
1046}
1047#line 73 "EmailLib.c"
1048void setEmailTo(int handle , int value ) 
1049{ 
1050
1051  {
1052#line 79
1053  if (handle == 1) {
1054#line 75
1055    __ste_email_to0 = value;
1056  } else {
1057#line 76
1058    if (handle == 2) {
1059#line 77
1060      __ste_email_to1 = value;
1061    } else {
1062
1063    }
1064  }
1065#line 937 "EmailLib.c"
1066  return;
1067}
1068}
1069#line 81 "EmailLib.c"
1070char *__ste_email_subject0  ;
1071#line 83 "EmailLib.c"
1072char *__ste_email_subject1  ;
1073#line 85 "EmailLib.c"
1074char *getEmailSubject(int handle ) 
1075{ char *retValue_acc ;
1076  void *__cil_tmp3 ;
1077
1078  {
1079#line 92 "EmailLib.c"
1080  if (handle == 1) {
1081#line 962
1082    retValue_acc = __ste_email_subject0;
1083#line 964
1084    return (retValue_acc);
1085  } else {
1086#line 966
1087    if (handle == 2) {
1088#line 971
1089      retValue_acc = __ste_email_subject1;
1090#line 973
1091      return (retValue_acc);
1092    } else {
1093#line 979 "EmailLib.c"
1094      __cil_tmp3 = (void *)0;
1095#line 979
1096      retValue_acc = (char *)__cil_tmp3;
1097#line 981
1098      return (retValue_acc);
1099    }
1100  }
1101#line 988 "EmailLib.c"
1102  return (retValue_acc);
1103}
1104}
1105#line 95 "EmailLib.c"
1106void setEmailSubject(int handle , char *value ) 
1107{ 
1108
1109  {
1110#line 101
1111  if (handle == 1) {
1112#line 97
1113    __ste_email_subject0 = value;
1114  } else {
1115#line 98
1116    if (handle == 2) {
1117#line 99
1118      __ste_email_subject1 = value;
1119    } else {
1120
1121    }
1122  }
1123#line 1019 "EmailLib.c"
1124  return;
1125}
1126}
1127#line 103 "EmailLib.c"
1128char *__ste_email_body0  =    (char *)0;
1129#line 105 "EmailLib.c"
1130char *__ste_email_body1  =    (char *)0;
1131#line 107 "EmailLib.c"
1132char *getEmailBody(int handle ) 
1133{ char *retValue_acc ;
1134  void *__cil_tmp3 ;
1135
1136  {
1137#line 114 "EmailLib.c"
1138  if (handle == 1) {
1139#line 1044
1140    retValue_acc = __ste_email_body0;
1141#line 1046
1142    return (retValue_acc);
1143  } else {
1144#line 1048
1145    if (handle == 2) {
1146#line 1053
1147      retValue_acc = __ste_email_body1;
1148#line 1055
1149      return (retValue_acc);
1150    } else {
1151#line 1061 "EmailLib.c"
1152      __cil_tmp3 = (void *)0;
1153#line 1061
1154      retValue_acc = (char *)__cil_tmp3;
1155#line 1063
1156      return (retValue_acc);
1157    }
1158  }
1159#line 1070 "EmailLib.c"
1160  return (retValue_acc);
1161}
1162}
1163#line 117 "EmailLib.c"
1164void setEmailBody(int handle , char *value ) 
1165{ 
1166
1167  {
1168#line 123
1169  if (handle == 1) {
1170#line 119
1171    __ste_email_body0 = value;
1172  } else {
1173#line 120
1174    if (handle == 2) {
1175#line 121
1176      __ste_email_body1 = value;
1177    } else {
1178
1179    }
1180  }
1181#line 1101 "EmailLib.c"
1182  return;
1183}
1184}
1185#line 125 "EmailLib.c"
1186int __ste_email_isEncrypted0  =    0;
1187#line 127 "EmailLib.c"
1188int __ste_email_isEncrypted1  =    0;
1189#line 129 "EmailLib.c"
1190int isEncrypted(int handle ) 
1191{ int retValue_acc ;
1192
1193  {
1194#line 136 "EmailLib.c"
1195  if (handle == 1) {
1196#line 1126
1197    retValue_acc = __ste_email_isEncrypted0;
1198#line 1128
1199    return (retValue_acc);
1200  } else {
1201#line 1130
1202    if (handle == 2) {
1203#line 1135
1204      retValue_acc = __ste_email_isEncrypted1;
1205#line 1137
1206      return (retValue_acc);
1207    } else {
1208#line 1143 "EmailLib.c"
1209      retValue_acc = 0;
1210#line 1145
1211      return (retValue_acc);
1212    }
1213  }
1214#line 1152 "EmailLib.c"
1215  return (retValue_acc);
1216}
1217}
1218#line 139 "EmailLib.c"
1219void setEmailIsEncrypted(int handle , int value ) 
1220{ 
1221
1222  {
1223#line 145
1224  if (handle == 1) {
1225#line 141
1226    __ste_email_isEncrypted0 = value;
1227  } else {
1228#line 142
1229    if (handle == 2) {
1230#line 143
1231      __ste_email_isEncrypted1 = value;
1232    } else {
1233
1234    }
1235  }
1236#line 1183 "EmailLib.c"
1237  return;
1238}
1239}
1240#line 147 "EmailLib.c"
1241int __ste_email_encryptionKey0  =    0;
1242#line 149 "EmailLib.c"
1243int __ste_email_encryptionKey1  =    0;
1244#line 151 "EmailLib.c"
1245int getEmailEncryptionKey(int handle ) 
1246{ int retValue_acc ;
1247
1248  {
1249#line 158 "EmailLib.c"
1250  if (handle == 1) {
1251#line 1208
1252    retValue_acc = __ste_email_encryptionKey0;
1253#line 1210
1254    return (retValue_acc);
1255  } else {
1256#line 1212
1257    if (handle == 2) {
1258#line 1217
1259      retValue_acc = __ste_email_encryptionKey1;
1260#line 1219
1261      return (retValue_acc);
1262    } else {
1263#line 1225 "EmailLib.c"
1264      retValue_acc = 0;
1265#line 1227
1266      return (retValue_acc);
1267    }
1268  }
1269#line 1234 "EmailLib.c"
1270  return (retValue_acc);
1271}
1272}
1273#line 161 "EmailLib.c"
1274void setEmailEncryptionKey(int handle , int value ) 
1275{ 
1276
1277  {
1278#line 167
1279  if (handle == 1) {
1280#line 163
1281    __ste_email_encryptionKey0 = value;
1282  } else {
1283#line 164
1284    if (handle == 2) {
1285#line 165
1286      __ste_email_encryptionKey1 = value;
1287    } else {
1288
1289    }
1290  }
1291#line 1265 "EmailLib.c"
1292  return;
1293}
1294}
1295#line 169 "EmailLib.c"
1296int __ste_email_isSigned0  =    0;
1297#line 171 "EmailLib.c"
1298int __ste_email_isSigned1  =    0;
1299#line 173 "EmailLib.c"
1300int isSigned(int handle ) 
1301{ int retValue_acc ;
1302
1303  {
1304#line 180 "EmailLib.c"
1305  if (handle == 1) {
1306#line 1290
1307    retValue_acc = __ste_email_isSigned0;
1308#line 1292
1309    return (retValue_acc);
1310  } else {
1311#line 1294
1312    if (handle == 2) {
1313#line 1299
1314      retValue_acc = __ste_email_isSigned1;
1315#line 1301
1316      return (retValue_acc);
1317    } else {
1318#line 1307 "EmailLib.c"
1319      retValue_acc = 0;
1320#line 1309
1321      return (retValue_acc);
1322    }
1323  }
1324#line 1316 "EmailLib.c"
1325  return (retValue_acc);
1326}
1327}
1328#line 183 "EmailLib.c"
1329void setEmailIsSigned(int handle , int value ) 
1330{ 
1331
1332  {
1333#line 189
1334  if (handle == 1) {
1335#line 185
1336    __ste_email_isSigned0 = value;
1337  } else {
1338#line 186
1339    if (handle == 2) {
1340#line 187
1341      __ste_email_isSigned1 = value;
1342    } else {
1343
1344    }
1345  }
1346#line 1347 "EmailLib.c"
1347  return;
1348}
1349}
1350#line 191 "EmailLib.c"
1351int __ste_email_signKey0  =    0;
1352#line 193 "EmailLib.c"
1353int __ste_email_signKey1  =    0;
1354#line 195 "EmailLib.c"
1355int getEmailSignKey(int handle ) 
1356{ int retValue_acc ;
1357
1358  {
1359#line 202 "EmailLib.c"
1360  if (handle == 1) {
1361#line 1372
1362    retValue_acc = __ste_email_signKey0;
1363#line 1374
1364    return (retValue_acc);
1365  } else {
1366#line 1376
1367    if (handle == 2) {
1368#line 1381
1369      retValue_acc = __ste_email_signKey1;
1370#line 1383
1371      return (retValue_acc);
1372    } else {
1373#line 1389 "EmailLib.c"
1374      retValue_acc = 0;
1375#line 1391
1376      return (retValue_acc);
1377    }
1378  }
1379#line 1398 "EmailLib.c"
1380  return (retValue_acc);
1381}
1382}
1383#line 205 "EmailLib.c"
1384void setEmailSignKey(int handle , int value ) 
1385{ 
1386
1387  {
1388#line 211
1389  if (handle == 1) {
1390#line 207
1391    __ste_email_signKey0 = value;
1392  } else {
1393#line 208
1394    if (handle == 2) {
1395#line 209
1396      __ste_email_signKey1 = value;
1397    } else {
1398
1399    }
1400  }
1401#line 1429 "EmailLib.c"
1402  return;
1403}
1404}
1405#line 213 "EmailLib.c"
1406int __ste_email_isSignatureVerified0  ;
1407#line 215 "EmailLib.c"
1408int __ste_email_isSignatureVerified1  ;
1409#line 217 "EmailLib.c"
1410int isVerified(int handle ) 
1411{ int retValue_acc ;
1412
1413  {
1414#line 224 "EmailLib.c"
1415  if (handle == 1) {
1416#line 1454
1417    retValue_acc = __ste_email_isSignatureVerified0;
1418#line 1456
1419    return (retValue_acc);
1420  } else {
1421#line 1458
1422    if (handle == 2) {
1423#line 1463
1424      retValue_acc = __ste_email_isSignatureVerified1;
1425#line 1465
1426      return (retValue_acc);
1427    } else {
1428#line 1471 "EmailLib.c"
1429      retValue_acc = 0;
1430#line 1473
1431      return (retValue_acc);
1432    }
1433  }
1434#line 1480 "EmailLib.c"
1435  return (retValue_acc);
1436}
1437}
1438#line 227 "EmailLib.c"
1439void setEmailIsSignatureVerified(int handle , int value ) 
1440{ 
1441
1442  {
1443#line 233
1444  if (handle == 1) {
1445#line 229
1446    __ste_email_isSignatureVerified0 = value;
1447  } else {
1448#line 230
1449    if (handle == 2) {
1450#line 231
1451      __ste_email_isSignatureVerified1 = value;
1452    } else {
1453
1454    }
1455  }
1456#line 1511 "EmailLib.c"
1457  return;
1458}
1459}
1460#line 1 "Client.o"
1461#pragma merger(0,"Client.i","")
1462#line 4 "ClientLib.h"
1463int initClient(void) ;
1464#line 33
1465int getClientPrivateKey(int handle ) ;
1466#line 35
1467void setClientPrivateKey(int handle , int value ) ;
1468#line 49
1469int getClientForwardReceiver(int handle ) ;
1470#line 53
1471int getClientId(int handle ) ;
1472#line 57
1473int findPublicKey(int handle , int userid ) ;
1474#line 14 "Client.h"
1475void queue(int client , int msg ) ;
1476#line 17
1477int is_queue_empty(void) ;
1478#line 19
1479int get_queued_client(void) ;
1480#line 21
1481int get_queued_email(void) ;
1482#line 24
1483void mail(int client , int msg ) ;
1484#line 26
1485void outgoing(int client , int msg ) ;
1486#line 28
1487void deliver(int client , int msg ) ;
1488#line 30
1489void incoming(int client , int msg ) ;
1490#line 32
1491int createClient(char *name ) ;
1492#line 35
1493void sendEmail(int sender , int receiver ) ;
1494#line 40
1495int isKeyPairValid(int publicKey , int privateKey ) ;
1496#line 44
1497void generateKeyPair(int client , int seed ) ;
1498#line 46
1499void forward(int client , int msg ) ;
1500#line 6 "Client.c"
1501int queue_empty  =    1;
1502#line 9 "Client.c"
1503int queued_message  ;
1504#line 12 "Client.c"
1505int queued_client  ;
1506#line 18 "Client.c"
1507void mail(int client , int msg ) 
1508{ int __utac__ad__arg1 ;
1509  int tmp ;
1510
1511  {
1512  {
1513#line 722 "Client.c"
1514  __utac__ad__arg1 = msg;
1515#line 723
1516  __utac_acc__EncryptForward_spec__2(__utac__ad__arg1);
1517#line 19 "Client.c"
1518  puts("mail sent");
1519#line 20
1520  tmp = getEmailTo(msg);
1521#line 20
1522  incoming(tmp, msg);
1523  }
1524#line 740 "Client.c"
1525  return;
1526}
1527}
1528#line 27 "Client.c"
1529void outgoing__wrappee__Keys(int client , int msg ) 
1530{ int tmp ;
1531
1532  {
1533  {
1534#line 28
1535  tmp = getClientId(client);
1536#line 28
1537  setEmailFrom(msg, tmp);
1538#line 29
1539  mail(client, msg);
1540  }
1541#line 762 "Client.c"
1542  return;
1543}
1544}
1545#line 33 "Client.c"
1546void outgoing(int client , int msg ) 
1547{ int receiver ;
1548  int tmp ;
1549  int pubkey ;
1550  int tmp___0 ;
1551
1552  {
1553  {
1554#line 36
1555  tmp = getEmailTo(msg);
1556#line 36
1557  receiver = tmp;
1558#line 37
1559  tmp___0 = findPublicKey(client, receiver);
1560#line 37
1561  pubkey = tmp___0;
1562  }
1563#line 38
1564  if (pubkey) {
1565    {
1566#line 39
1567    setEmailEncryptionKey(msg, pubkey);
1568#line 40
1569    setEmailIsEncrypted(msg, 1);
1570    }
1571  } else {
1572
1573  }
1574  {
1575#line 45
1576  outgoing__wrappee__Keys(client, msg);
1577  }
1578#line 797 "Client.c"
1579  return;
1580}
1581}
1582#line 52 "Client.c"
1583void deliver(int client , int msg ) 
1584{ 
1585
1586  {
1587  {
1588#line 53
1589  puts("mail delivered\n");
1590  }
1591#line 817 "Client.c"
1592  return;
1593}
1594}
1595#line 60 "Client.c"
1596void incoming__wrappee__Encrypt(int client , int msg ) 
1597{ 
1598
1599  {
1600  {
1601#line 61
1602  deliver(client, msg);
1603  }
1604#line 837 "Client.c"
1605  return;
1606}
1607}
1608#line 67 "Client.c"
1609void incoming__wrappee__Forward(int client , int msg ) 
1610{ int fwreceiver ;
1611  int tmp ;
1612
1613  {
1614  {
1615#line 68
1616  incoming__wrappee__Encrypt(client, msg);
1617#line 69
1618  tmp = getClientForwardReceiver(client);
1619#line 69
1620  fwreceiver = tmp;
1621  }
1622#line 70
1623  if (fwreceiver) {
1624    {
1625#line 72
1626    setEmailTo(msg, fwreceiver);
1627#line 73
1628    forward(client, msg);
1629    }
1630  } else {
1631
1632  }
1633#line 868 "Client.c"
1634  return;
1635}
1636}
1637#line 80 "Client.c"
1638void incoming(int client , int msg ) 
1639{ int __utac__ad__arg1 ;
1640  int privkey ;
1641  int tmp ;
1642  int tmp___0 ;
1643  int tmp___1 ;
1644  int tmp___2 ;
1645
1646  {
1647  {
1648#line 881 "Client.c"
1649  __utac__ad__arg1 = msg;
1650#line 882
1651  __utac_acc__EncryptForward_spec__1(__utac__ad__arg1);
1652#line 83 "Client.c"
1653  tmp = getClientPrivateKey(client);
1654#line 83
1655  privkey = tmp;
1656  }
1657#line 84
1658  if (privkey) {
1659    {
1660#line 92
1661    tmp___0 = isEncrypted(msg);
1662    }
1663#line 92
1664    if (tmp___0) {
1665      {
1666#line 92
1667      tmp___1 = getEmailEncryptionKey(msg);
1668#line 92
1669      tmp___2 = isKeyPairValid(tmp___1, privkey);
1670      }
1671#line 92
1672      if (tmp___2) {
1673        {
1674#line 89
1675        setEmailIsEncrypted(msg, 0);
1676#line 90
1677        setEmailEncryptionKey(msg, 0);
1678        }
1679      } else {
1680
1681      }
1682    } else {
1683
1684    }
1685  } else {
1686
1687  }
1688  {
1689#line 95
1690  incoming__wrappee__Forward(client, msg);
1691  }
1692#line 911 "Client.c"
1693  return;
1694}
1695}
1696#line 99 "Client.c"
1697int createClient(char *name ) 
1698{ int retValue_acc ;
1699  int client ;
1700  int tmp ;
1701
1702  {
1703  {
1704#line 100
1705  tmp = initClient();
1706#line 100
1707  client = tmp;
1708#line 933 "Client.c"
1709  retValue_acc = client;
1710  }
1711#line 935
1712  return (retValue_acc);
1713#line 942
1714  return (retValue_acc);
1715}
1716}
1717#line 107 "Client.c"
1718void sendEmail(int sender , int receiver ) 
1719{ int email ;
1720  int tmp ;
1721
1722  {
1723  {
1724#line 108
1725  tmp = createEmail(0, receiver);
1726#line 108
1727  email = tmp;
1728#line 109
1729  outgoing(sender, email);
1730  }
1731#line 970 "Client.c"
1732  return;
1733}
1734}
1735#line 117 "Client.c"
1736void queue(int client , int msg ) 
1737{ 
1738
1739  {
1740#line 118
1741  queue_empty = 0;
1742#line 119
1743  queued_message = msg;
1744#line 120
1745  queued_client = client;
1746#line 994 "Client.c"
1747  return;
1748}
1749}
1750#line 126 "Client.c"
1751int is_queue_empty(void) 
1752{ int retValue_acc ;
1753
1754  {
1755#line 1012 "Client.c"
1756  retValue_acc = queue_empty;
1757#line 1014
1758  return (retValue_acc);
1759#line 1021
1760  return (retValue_acc);
1761}
1762}
1763#line 133 "Client.c"
1764int get_queued_client(void) 
1765{ int retValue_acc ;
1766
1767  {
1768#line 1043 "Client.c"
1769  retValue_acc = queued_client;
1770#line 1045
1771  return (retValue_acc);
1772#line 1052
1773  return (retValue_acc);
1774}
1775}
1776#line 140 "Client.c"
1777int get_queued_email(void) 
1778{ int retValue_acc ;
1779
1780  {
1781#line 1074 "Client.c"
1782  retValue_acc = queued_message;
1783#line 1076
1784  return (retValue_acc);
1785#line 1083
1786  return (retValue_acc);
1787}
1788}
1789#line 146 "Client.c"
1790int isKeyPairValid(int publicKey , int privateKey ) 
1791{ int retValue_acc ;
1792  char const   * __restrict  __cil_tmp4 ;
1793
1794  {
1795  {
1796#line 147
1797  __cil_tmp4 = (char const   * __restrict  )"keypair valid %d %d";
1798#line 147
1799  printf(__cil_tmp4, publicKey, privateKey);
1800  }
1801#line 148 "Client.c"
1802  if (! publicKey) {
1803#line 1108 "Client.c"
1804    retValue_acc = 0;
1805#line 1110
1806    return (retValue_acc);
1807  } else {
1808#line 148 "Client.c"
1809    if (! privateKey) {
1810#line 1108 "Client.c"
1811      retValue_acc = 0;
1812#line 1110
1813      return (retValue_acc);
1814    } else {
1815
1816    }
1817  }
1818#line 1115 "Client.c"
1819  retValue_acc = privateKey == publicKey;
1820#line 1117
1821  return (retValue_acc);
1822#line 1124
1823  return (retValue_acc);
1824}
1825}
1826#line 156 "Client.c"
1827void generateKeyPair(int client , int seed ) 
1828{ 
1829
1830  {
1831  {
1832#line 157
1833  setClientPrivateKey(client, seed);
1834  }
1835#line 1148 "Client.c"
1836  return;
1837}
1838}
1839#line 162 "Client.c"
1840void forward(int client , int msg ) 
1841{ 
1842
1843  {
1844  {
1845#line 163
1846  puts("Forwarding message.\n");
1847#line 164
1848  printMail(msg);
1849#line 165
1850  queue(client, msg);
1851  }
1852#line 1172 "Client.c"
1853  return;
1854}
1855}
1856#line 1 "featureselect.o"
1857#pragma merger(0,"featureselect.i","")
1858#line 41 "featureselect.h"
1859int select_one(void) ;
1860#line 43
1861void select_features(void) ;
1862#line 45
1863void select_helpers(void) ;
1864#line 47
1865int valid_product(void) ;
1866#line 8 "featureselect.c"
1867int select_one(void) 
1868{ int retValue_acc ;
1869  int choice = __VERIFIER_nondet_int();
1870
1871  {
1872#line 84 "featureselect.c"
1873  retValue_acc = choice;
1874#line 86
1875  return (retValue_acc);
1876#line 93
1877  return (retValue_acc);
1878}
1879}
1880#line 14 "featureselect.c"
1881void select_features(void) 
1882{ 
1883
1884  {
1885#line 115 "featureselect.c"
1886  return;
1887}
1888}
1889#line 20 "featureselect.c"
1890void select_helpers(void) 
1891{ 
1892
1893  {
1894#line 133 "featureselect.c"
1895  return;
1896}
1897}
1898#line 25 "featureselect.c"
1899int valid_product(void) 
1900{ int retValue_acc ;
1901
1902  {
1903#line 151 "featureselect.c"
1904  retValue_acc = 1;
1905#line 153
1906  return (retValue_acc);
1907#line 160
1908  return (retValue_acc);
1909}
1910}
1911#line 1 "scenario.o"
1912#pragma merger(0,"scenario.i","")
1913#line 17 "scenario.c"
1914void bobKeyAdd(void) ;
1915#line 24
1916void rjhDeletePrivateKey(void) ;
1917#line 28
1918void rjhKeyAdd(void) ;
1919#line 32
1920void chuckKeyAddRjh(void) ;
1921#line 36
1922void rjhEnableForwarding(void) ;
1923#line 40
1924void rjhKeyChange(void) ;
1925#line 47
1926void chuckKeyAdd(void) ;
1927#line 51
1928void bobKeyChange(void) ;
1929#line 53
1930#line 60
1931void bobToRjh(void) ;
1932#line 1 "scenario.c"
1933void test(void) 
1934{ int op1 ;
1935  int op2 ;
1936  int op3 ;
1937  int op4 ;
1938  int op5 ;
1939  int op6 ;
1940  int op7 ;
1941  int op8 ;
1942  int op9 ;
1943  int op10 ;
1944  int op11 ;
1945  int splverifierCounter ;
1946  int tmp ;
1947  int tmp___0 ;
1948  int tmp___1 ;
1949  int tmp___2 ;
1950  int tmp___3 ;
1951  int tmp___4 ;
1952  int tmp___5 ;
1953  int tmp___6 ;
1954  int tmp___7 ;
1955  int tmp___8 ;
1956  int tmp___9 ;
1957
1958  {
1959#line 2
1960  op1 = 0;
1961#line 3
1962  op2 = 0;
1963#line 4
1964  op3 = 0;
1965#line 5
1966  op4 = 0;
1967#line 6
1968  op5 = 0;
1969#line 7
1970  op6 = 0;
1971#line 8
1972  op7 = 0;
1973#line 9
1974  op8 = 0;
1975#line 10
1976  op9 = 0;
1977#line 11
1978  op10 = 0;
1979#line 12
1980  op11 = 0;
1981#line 13
1982  splverifierCounter = 0;
1983  {
1984#line 14
1985  while (1) {
1986    while_3_continue: /* CIL Label */ ;
1987#line 14
1988    if (splverifierCounter < 4) {
1989
1990    } else {
1991      goto while_3_break;
1992    }
1993#line 15
1994    splverifierCounter = splverifierCounter + 1;
1995#line 16
1996    if (! op1) {
1997      {
1998#line 16
1999      tmp___9 = __VERIFIER_nondet_int();
2000      }
2001#line 16
2002      if (tmp___9) {
2003        {
2004#line 17
2005        bobKeyAdd();
2006#line 18
2007        op1 = 1;
2008        }
2009      } else {
2010        goto _L___8;
2011      }
2012    } else {
2013      _L___8: /* CIL Label */ 
2014#line 19
2015      if (! op2) {
2016        {
2017#line 19
2018        tmp___8 = __VERIFIER_nondet_int();
2019        }
2020#line 19
2021        if (tmp___8) {
2022#line 21
2023          op2 = 1;
2024        } else {
2025          goto _L___7;
2026        }
2027      } else {
2028        _L___7: /* CIL Label */ 
2029#line 22
2030        if (! op3) {
2031          {
2032#line 22
2033          tmp___7 = __VERIFIER_nondet_int();
2034          }
2035#line 22
2036          if (tmp___7) {
2037            {
2038#line 24
2039            rjhDeletePrivateKey();
2040#line 25
2041            op3 = 1;
2042            }
2043          } else {
2044            goto _L___6;
2045          }
2046        } else {
2047          _L___6: /* CIL Label */ 
2048#line 26
2049          if (! op4) {
2050            {
2051#line 26
2052            tmp___6 = __VERIFIER_nondet_int();
2053            }
2054#line 26
2055            if (tmp___6) {
2056              {
2057#line 28
2058              rjhKeyAdd();
2059#line 29
2060              op4 = 1;
2061              }
2062            } else {
2063              goto _L___5;
2064            }
2065          } else {
2066            _L___5: /* CIL Label */ 
2067#line 30
2068            if (! op5) {
2069              {
2070#line 30
2071              tmp___5 = __VERIFIER_nondet_int();
2072              }
2073#line 30
2074              if (tmp___5) {
2075                {
2076#line 32
2077                chuckKeyAddRjh();
2078#line 33
2079                op5 = 1;
2080                }
2081              } else {
2082                goto _L___4;
2083              }
2084            } else {
2085              _L___4: /* CIL Label */ 
2086#line 34
2087              if (! op6) {
2088                {
2089#line 34
2090                tmp___4 = __VERIFIER_nondet_int();
2091                }
2092#line 34
2093                if (tmp___4) {
2094                  {
2095#line 36
2096                  rjhEnableForwarding();
2097#line 37
2098                  op6 = 1;
2099                  }
2100                } else {
2101                  goto _L___3;
2102                }
2103              } else {
2104                _L___3: /* CIL Label */ 
2105#line 38
2106                if (! op7) {
2107                  {
2108#line 38
2109                  tmp___3 = __VERIFIER_nondet_int();
2110                  }
2111#line 38
2112                  if (tmp___3) {
2113                    {
2114#line 40
2115                    rjhKeyChange();
2116#line 41
2117                    op7 = 1;
2118                    }
2119                  } else {
2120                    goto _L___2;
2121                  }
2122                } else {
2123                  _L___2: /* CIL Label */ 
2124#line 42
2125                  if (! op8) {
2126                    {
2127#line 42
2128                    tmp___2 = __VERIFIER_nondet_int();
2129                    }
2130#line 42
2131                    if (tmp___2) {
2132#line 44
2133                      op8 = 1;
2134                    } else {
2135                      goto _L___1;
2136                    }
2137                  } else {
2138                    _L___1: /* CIL Label */ 
2139#line 45
2140                    if (! op9) {
2141                      {
2142#line 45
2143                      tmp___1 = __VERIFIER_nondet_int();
2144                      }
2145#line 45
2146                      if (tmp___1) {
2147                        {
2148#line 47
2149                        chuckKeyAdd();
2150#line 48
2151                        op9 = 1;
2152                        }
2153                      } else {
2154                        goto _L___0;
2155                      }
2156                    } else {
2157                      _L___0: /* CIL Label */ 
2158#line 49
2159                      if (! op10) {
2160                        {
2161#line 49
2162                        tmp___0 = __VERIFIER_nondet_int();
2163                        }
2164#line 49
2165                        if (tmp___0) {
2166                          {
2167#line 51
2168                          bobKeyChange();
2169#line 52
2170                          op10 = 1;
2171                          }
2172                        } else {
2173                          goto _L;
2174                        }
2175                      } else {
2176                        _L: /* CIL Label */ 
2177#line 53
2178                        if (! op11) {
2179                          {
2180#line 53
2181                          tmp = __VERIFIER_nondet_int();
2182                          }
2183#line 53
2184                          if (tmp) {
2185                            {
2186#line 55
2187                            chuckKeyAdd();
2188#line 56
2189                            op11 = 1;
2190                            }
2191                          } else {
2192                            goto while_3_break;
2193                          }
2194                        } else {
2195                          goto while_3_break;
2196                        }
2197                      }
2198                    }
2199                  }
2200                }
2201              }
2202            }
2203          }
2204        }
2205      }
2206    }
2207  }
2208  while_3_break: /* CIL Label */ ;
2209  }
2210  {
2211#line 60
2212  bobToRjh();
2213  }
2214#line 167 "scenario.c"
2215  return;
2216}
2217}
2218#line 1 "wsllib_check.o"
2219#pragma merger(0,"wsllib_check.i","")
2220#line 3 "wsllib_check.c"
2221void __automaton_fail(void) 
2222{ 
2223
2224  {
2225  goto ERROR;
2226  ERROR: ;
2227#line 53 "wsllib_check.c"
2228  return;
2229}
2230}
2231#line 1 "Test.o"
2232#pragma merger(0,"Test.i","")
2233#line 39 "ClientLib.h"
2234int createClientKeyringEntry(int handle ) ;
2235#line 41
2236int getClientKeyringUser(int handle , int index ) ;
2237#line 43
2238void setClientKeyringUser(int handle , int index , int value ) ;
2239#line 45
2240int getClientKeyringPublicKey(int handle , int index ) ;
2241#line 47
2242void setClientKeyringPublicKey(int handle , int index , int value ) ;
2243#line 51
2244void setClientForwardReceiver(int handle , int value ) ;
2245#line 55
2246void setClientId(int handle , int value ) ;
2247#line 2 "Test.h"
2248int bob  ;
2249#line 5 "Test.h"
2250int rjh  ;
2251#line 8 "Test.h"
2252int chuck  ;
2253#line 11
2254void setup_bob(int bob___0 ) ;
2255#line 14
2256void setup_rjh(int rjh___0 ) ;
2257#line 17
2258void setup_chuck(int chuck___0 ) ;
2259#line 26
2260void rjhToBob(void) ;
2261#line 32
2262void setup(void) ;
2263#line 35
2264int main(void) ;
2265#line 39
2266void bobKeyAddChuck(void) ;
2267#line 45
2268void rjhKeyAddChuck(void) ;
2269#line 18 "Test.c"
2270void setup_bob__wrappee__Base(int bob___0 ) 
2271{ 
2272
2273  {
2274  {
2275#line 19
2276  setClientId(bob___0, bob___0);
2277  }
2278#line 1326 "Test.c"
2279  return;
2280}
2281}
2282#line 23 "Test.c"
2283void setup_bob(int bob___0 ) 
2284{ 
2285
2286  {
2287  {
2288#line 24
2289  setup_bob__wrappee__Base(bob___0);
2290#line 25
2291  setClientPrivateKey(bob___0, 123);
2292  }
2293#line 1348 "Test.c"
2294  return;
2295}
2296}
2297#line 33 "Test.c"
2298void setup_rjh__wrappee__Base(int rjh___0 ) 
2299{ 
2300
2301  {
2302  {
2303#line 34
2304  setClientId(rjh___0, rjh___0);
2305  }
2306#line 1368 "Test.c"
2307  return;
2308}
2309}
2310#line 40 "Test.c"
2311void setup_rjh(int rjh___0 ) 
2312{ 
2313
2314  {
2315  {
2316#line 42
2317  setup_rjh__wrappee__Base(rjh___0);
2318#line 43
2319  setClientPrivateKey(rjh___0, 456);
2320  }
2321#line 1390 "Test.c"
2322  return;
2323}
2324}
2325#line 50 "Test.c"
2326void setup_chuck__wrappee__Base(int chuck___0 ) 
2327{ 
2328
2329  {
2330  {
2331#line 51
2332  setClientId(chuck___0, chuck___0);
2333  }
2334#line 1410 "Test.c"
2335  return;
2336}
2337}
2338#line 57 "Test.c"
2339void setup_chuck(int chuck___0 ) 
2340{ 
2341
2342  {
2343  {
2344#line 58
2345  setup_chuck__wrappee__Base(chuck___0);
2346#line 59
2347  setClientPrivateKey(chuck___0, 789);
2348  }
2349#line 1432 "Test.c"
2350  return;
2351}
2352}
2353#line 69 "Test.c"
2354void bobToRjh(void) 
2355{ int tmp ;
2356  int tmp___0 ;
2357  int tmp___1 ;
2358
2359  {
2360  {
2361#line 71
2362  puts("Please enter a subject and a message body.\n");
2363#line 72
2364  sendEmail(bob, rjh);
2365#line 73
2366  tmp___1 = is_queue_empty();
2367  }
2368#line 73
2369  if (tmp___1) {
2370
2371  } else {
2372    {
2373#line 74
2374    tmp = get_queued_email();
2375#line 74
2376    tmp___0 = get_queued_client();
2377#line 74
2378    outgoing(tmp___0, tmp);
2379    }
2380  }
2381#line 1459 "Test.c"
2382  return;
2383}
2384}
2385#line 81 "Test.c"
2386void rjhToBob(void) 
2387{ 
2388
2389  {
2390  {
2391#line 83
2392  puts("Please enter a subject and a message body.\n");
2393#line 84
2394  sendEmail(rjh, bob);
2395  }
2396#line 1481 "Test.c"
2397  return;
2398}
2399}
2400#line 88 "Test.c"
2401#line 95 "Test.c"
2402void setup(void) 
2403{ char const   * __restrict  __cil_tmp1 ;
2404  char const   * __restrict  __cil_tmp2 ;
2405  char const   * __restrict  __cil_tmp3 ;
2406
2407  {
2408  {
2409#line 96
2410  bob = 1;
2411#line 97
2412  setup_bob(bob);
2413#line 98
2414  __cil_tmp1 = (char const   * __restrict  )"bob: %d\n";
2415#line 98
2416  printf(__cil_tmp1, bob);
2417#line 100
2418  rjh = 2;
2419#line 101
2420  setup_rjh(rjh);
2421#line 102
2422  __cil_tmp2 = (char const   * __restrict  )"rjh: %d\n";
2423#line 102
2424  printf(__cil_tmp2, rjh);
2425#line 104
2426  chuck = 3;
2427#line 105
2428  setup_chuck(chuck);
2429#line 106
2430  __cil_tmp3 = (char const   * __restrict  )"chuck: %d\n";
2431#line 106
2432  printf(__cil_tmp3, chuck);
2433  }
2434#line 1552 "Test.c"
2435  return;
2436}
2437}
2438#line 112 "Test.c"
2439int main(void) 
2440{ int retValue_acc ;
2441  int tmp ;
2442
2443  {
2444  {
2445#line 113
2446  select_helpers();
2447#line 114
2448  select_features();
2449#line 115
2450  tmp = valid_product();
2451  }
2452#line 115
2453  if (tmp) {
2454    {
2455#line 116
2456    setup();
2457#line 117
2458    test();
2459    }
2460  } else {
2461
2462  }
2463#line 1583 "Test.c"
2464  return (retValue_acc);
2465}
2466}
2467#line 125 "Test.c"
2468void bobKeyAdd(void) 
2469{ int tmp ;
2470  int tmp___0 ;
2471  char const   * __restrict  __cil_tmp3 ;
2472  char const   * __restrict  __cil_tmp4 ;
2473
2474  {
2475  {
2476#line 126
2477  createClientKeyringEntry(bob);
2478#line 127
2479  setClientKeyringUser(bob, 0, 2);
2480#line 128
2481  setClientKeyringPublicKey(bob, 0, 456);
2482#line 129
2483  puts("bob added rjhs key");
2484#line 130
2485  tmp = getClientKeyringUser(bob, 0);
2486#line 130
2487  __cil_tmp3 = (char const   * __restrict  )"%d\n";
2488#line 130
2489  printf(__cil_tmp3, tmp);
2490#line 131
2491  tmp___0 = getClientKeyringPublicKey(bob, 0);
2492#line 131
2493  __cil_tmp4 = (char const   * __restrict  )"%d\n";
2494#line 131
2495  printf(__cil_tmp4, tmp___0);
2496  }
2497#line 1617 "Test.c"
2498  return;
2499}
2500}
2501#line 137 "Test.c"
2502void rjhKeyAdd(void) 
2503{ 
2504
2505  {
2506  {
2507#line 138
2508  createClientKeyringEntry(rjh);
2509#line 139
2510  setClientKeyringUser(rjh, 0, 1);
2511#line 140
2512  setClientKeyringPublicKey(rjh, 0, 123);
2513  }
2514#line 1641 "Test.c"
2515  return;
2516}
2517}
2518#line 146 "Test.c"
2519void rjhKeyAddChuck(void) 
2520{ 
2521
2522  {
2523  {
2524#line 147
2525  createClientKeyringEntry(rjh);
2526#line 148
2527  setClientKeyringUser(rjh, 0, 3);
2528#line 149
2529  setClientKeyringPublicKey(rjh, 0, 789);
2530  }
2531#line 1665 "Test.c"
2532  return;
2533}
2534}
2535#line 156 "Test.c"
2536void bobKeyAddChuck(void) 
2537{ 
2538
2539  {
2540  {
2541#line 157
2542  createClientKeyringEntry(bob);
2543#line 158
2544  setClientKeyringUser(bob, 1, 3);
2545#line 159
2546  setClientKeyringPublicKey(bob, 1, 789);
2547  }
2548#line 1689 "Test.c"
2549  return;
2550}
2551}
2552#line 165 "Test.c"
2553void chuckKeyAdd(void) 
2554{ 
2555
2556  {
2557  {
2558#line 166
2559  createClientKeyringEntry(chuck);
2560#line 167
2561  setClientKeyringUser(chuck, 0, 1);
2562#line 168
2563  setClientKeyringPublicKey(chuck, 0, 123);
2564  }
2565#line 1713 "Test.c"
2566  return;
2567}
2568}
2569#line 174 "Test.c"
2570void chuckKeyAddRjh(void) 
2571{ 
2572
2573  {
2574  {
2575#line 175
2576  createClientKeyringEntry(chuck);
2577#line 176
2578  setClientKeyringUser(chuck, 0, 2);
2579#line 177
2580  setClientKeyringPublicKey(chuck, 0, 456);
2581  }
2582#line 1737 "Test.c"
2583  return;
2584}
2585}
2586#line 183 "Test.c"
2587void rjhDeletePrivateKey(void) 
2588{ 
2589
2590  {
2591  {
2592#line 184
2593  setClientPrivateKey(rjh, 0);
2594  }
2595#line 1757 "Test.c"
2596  return;
2597}
2598}
2599#line 190 "Test.c"
2600void bobKeyChange(void) 
2601{ 
2602
2603  {
2604  {
2605#line 191
2606  generateKeyPair(bob, 777);
2607  }
2608#line 1777 "Test.c"
2609  return;
2610}
2611}
2612#line 197 "Test.c"
2613void rjhKeyChange(void) 
2614{ 
2615
2616  {
2617  {
2618#line 198
2619  generateKeyPair(rjh, 666);
2620  }
2621#line 1797 "Test.c"
2622  return;
2623}
2624}
2625#line 204 "Test.c"
2626void rjhEnableForwarding(void) 
2627{ 
2628
2629  {
2630  {
2631#line 205
2632  setClientForwardReceiver(rjh, chuck);
2633  }
2634#line 1817 "Test.c"
2635  return;
2636}
2637}
2638#line 1 "ClientLib.o"
2639#pragma merger(0,"ClientLib.i","")
2640#line 6 "ClientLib.h"
2641char *getClientName(int handle ) ;
2642#line 8
2643void setClientName(int handle , char *value ) ;
2644#line 10
2645int getClientOutbuffer(int handle ) ;
2646#line 12
2647void setClientOutbuffer(int handle , int value ) ;
2648#line 14
2649int getClientAddressBookSize(int handle ) ;
2650#line 16
2651void setClientAddressBookSize(int handle , int value ) ;
2652#line 18
2653int createClientAddressBookEntry(int handle ) ;
2654#line 20
2655int getClientAddressBookAlias(int handle , int index ) ;
2656#line 22
2657void setClientAddressBookAlias(int handle , int index , int value ) ;
2658#line 24
2659int getClientAddressBookAddress(int handle , int index ) ;
2660#line 26
2661void setClientAddressBookAddress(int handle , int index , int value ) ;
2662#line 29
2663int getClientAutoResponse(int handle ) ;
2664#line 31
2665void setClientAutoResponse(int handle , int value ) ;
2666#line 37
2667int getClientKeyringSize(int handle ) ;
2668#line 59
2669int findClientAddressBookAlias(int handle , int userid ) ;
2670#line 5 "ClientLib.c"
2671int __ste_Client_counter  =    0;
2672#line 7 "ClientLib.c"
2673int initClient(void) 
2674{ int retValue_acc ;
2675
2676  {
2677#line 12 "ClientLib.c"
2678  if (__ste_Client_counter < 3) {
2679#line 684
2680    __ste_Client_counter = __ste_Client_counter + 1;
2681#line 684
2682    retValue_acc = __ste_Client_counter;
2683#line 686
2684    return (retValue_acc);
2685  } else {
2686#line 692 "ClientLib.c"
2687    retValue_acc = -1;
2688#line 694
2689    return (retValue_acc);
2690  }
2691#line 701 "ClientLib.c"
2692  return (retValue_acc);
2693}
2694}
2695#line 15 "ClientLib.c"
2696char *__ste_client_name0  =    (char *)0;
2697#line 17 "ClientLib.c"
2698char *__ste_client_name1  =    (char *)0;
2699#line 19 "ClientLib.c"
2700char *__ste_client_name2  =    (char *)0;
2701#line 22 "ClientLib.c"
2702char *getClientName(int handle ) 
2703{ char *retValue_acc ;
2704  void *__cil_tmp3 ;
2705
2706  {
2707#line 31 "ClientLib.c"
2708  if (handle == 1) {
2709#line 732
2710    retValue_acc = __ste_client_name0;
2711#line 734
2712    return (retValue_acc);
2713  } else {
2714#line 736
2715    if (handle == 2) {
2716#line 741
2717      retValue_acc = __ste_client_name1;
2718#line 743
2719      return (retValue_acc);
2720    } else {
2721#line 745
2722      if (handle == 3) {
2723#line 750
2724        retValue_acc = __ste_client_name2;
2725#line 752
2726        return (retValue_acc);
2727      } else {
2728#line 758 "ClientLib.c"
2729        __cil_tmp3 = (void *)0;
2730#line 758
2731        retValue_acc = (char *)__cil_tmp3;
2732#line 760
2733        return (retValue_acc);
2734      }
2735    }
2736  }
2737#line 767 "ClientLib.c"
2738  return (retValue_acc);
2739}
2740}
2741#line 34 "ClientLib.c"
2742void setClientName(int handle , char *value ) 
2743{ 
2744
2745  {
2746#line 42
2747  if (handle == 1) {
2748#line 36
2749    __ste_client_name0 = value;
2750  } else {
2751#line 37
2752    if (handle == 2) {
2753#line 38
2754      __ste_client_name1 = value;
2755    } else {
2756#line 39
2757      if (handle == 3) {
2758#line 40
2759        __ste_client_name2 = value;
2760      } else {
2761
2762      }
2763    }
2764  }
2765#line 802 "ClientLib.c"
2766  return;
2767}
2768}
2769#line 44 "ClientLib.c"
2770int __ste_client_outbuffer0  =    0;
2771#line 46 "ClientLib.c"
2772int __ste_client_outbuffer1  =    0;
2773#line 48 "ClientLib.c"
2774int __ste_client_outbuffer2  =    0;
2775#line 50 "ClientLib.c"
2776int __ste_client_outbuffer3  =    0;
2777#line 53 "ClientLib.c"
2778int getClientOutbuffer(int handle ) 
2779{ int retValue_acc ;
2780
2781  {
2782#line 62 "ClientLib.c"
2783  if (handle == 1) {
2784#line 831
2785    retValue_acc = __ste_client_outbuffer0;
2786#line 833
2787    return (retValue_acc);
2788  } else {
2789#line 835
2790    if (handle == 2) {
2791#line 840
2792      retValue_acc = __ste_client_outbuffer1;
2793#line 842
2794      return (retValue_acc);
2795    } else {
2796#line 844
2797      if (handle == 3) {
2798#line 849
2799        retValue_acc = __ste_client_outbuffer2;
2800#line 851
2801        return (retValue_acc);
2802      } else {
2803#line 857 "ClientLib.c"
2804        retValue_acc = 0;
2805#line 859
2806        return (retValue_acc);
2807      }
2808    }
2809  }
2810#line 866 "ClientLib.c"
2811  return (retValue_acc);
2812}
2813}
2814#line 65 "ClientLib.c"
2815void setClientOutbuffer(int handle , int value ) 
2816{ 
2817
2818  {
2819#line 73
2820  if (handle == 1) {
2821#line 67
2822    __ste_client_outbuffer0 = value;
2823  } else {
2824#line 68
2825    if (handle == 2) {
2826#line 69
2827      __ste_client_outbuffer1 = value;
2828    } else {
2829#line 70
2830      if (handle == 3) {
2831#line 71
2832        __ste_client_outbuffer2 = value;
2833      } else {
2834
2835      }
2836    }
2837  }
2838#line 901 "ClientLib.c"
2839  return;
2840}
2841}
2842#line 77 "ClientLib.c"
2843int __ste_ClientAddressBook_size0  =    0;
2844#line 79 "ClientLib.c"
2845int __ste_ClientAddressBook_size1  =    0;
2846#line 81 "ClientLib.c"
2847int __ste_ClientAddressBook_size2  =    0;
2848#line 84 "ClientLib.c"
2849int getClientAddressBookSize(int handle ) 
2850{ int retValue_acc ;
2851
2852  {
2853#line 93 "ClientLib.c"
2854  if (handle == 1) {
2855#line 928
2856    retValue_acc = __ste_ClientAddressBook_size0;
2857#line 930
2858    return (retValue_acc);
2859  } else {
2860#line 932
2861    if (handle == 2) {
2862#line 937
2863      retValue_acc = __ste_ClientAddressBook_size1;
2864#line 939
2865      return (retValue_acc);
2866    } else {
2867#line 941
2868      if (handle == 3) {
2869#line 946
2870        retValue_acc = __ste_ClientAddressBook_size2;
2871#line 948
2872        return (retValue_acc);
2873      } else {
2874#line 954 "ClientLib.c"
2875        retValue_acc = 0;
2876#line 956
2877        return (retValue_acc);
2878      }
2879    }
2880  }
2881#line 963 "ClientLib.c"
2882  return (retValue_acc);
2883}
2884}
2885#line 96 "ClientLib.c"
2886void setClientAddressBookSize(int handle , int value ) 
2887{ 
2888
2889  {
2890#line 104
2891  if (handle == 1) {
2892#line 98
2893    __ste_ClientAddressBook_size0 = value;
2894  } else {
2895#line 99
2896    if (handle == 2) {
2897#line 100
2898      __ste_ClientAddressBook_size1 = value;
2899    } else {
2900#line 101
2901      if (handle == 3) {
2902#line 102
2903        __ste_ClientAddressBook_size2 = value;
2904      } else {
2905
2906      }
2907    }
2908  }
2909#line 998 "ClientLib.c"
2910  return;
2911}
2912}
2913#line 106 "ClientLib.c"
2914int createClientAddressBookEntry(int handle ) 
2915{ int retValue_acc ;
2916  int size ;
2917  int tmp ;
2918  int __cil_tmp5 ;
2919
2920  {
2921  {
2922#line 107
2923  tmp = getClientAddressBookSize(handle);
2924#line 107
2925  size = tmp;
2926  }
2927#line 108 "ClientLib.c"
2928  if (size < 3) {
2929    {
2930#line 109 "ClientLib.c"
2931    __cil_tmp5 = size + 1;
2932#line 109
2933    setClientAddressBookSize(handle, __cil_tmp5);
2934#line 1025 "ClientLib.c"
2935    retValue_acc = size + 1;
2936    }
2937#line 1027
2938    return (retValue_acc);
2939  } else {
2940#line 1031 "ClientLib.c"
2941    retValue_acc = -1;
2942#line 1033
2943    return (retValue_acc);
2944  }
2945#line 1040 "ClientLib.c"
2946  return (retValue_acc);
2947}
2948}
2949#line 115 "ClientLib.c"
2950int __ste_Client_AddressBook0_Alias0  =    0;
2951#line 117 "ClientLib.c"
2952int __ste_Client_AddressBook0_Alias1  =    0;
2953#line 119 "ClientLib.c"
2954int __ste_Client_AddressBook0_Alias2  =    0;
2955#line 121 "ClientLib.c"
2956int __ste_Client_AddressBook1_Alias0  =    0;
2957#line 123 "ClientLib.c"
2958int __ste_Client_AddressBook1_Alias1  =    0;
2959#line 125 "ClientLib.c"
2960int __ste_Client_AddressBook1_Alias2  =    0;
2961#line 127 "ClientLib.c"
2962int __ste_Client_AddressBook2_Alias0  =    0;
2963#line 129 "ClientLib.c"
2964int __ste_Client_AddressBook2_Alias1  =    0;
2965#line 131 "ClientLib.c"
2966int __ste_Client_AddressBook2_Alias2  =    0;
2967#line 134 "ClientLib.c"
2968int getClientAddressBookAlias(int handle , int index ) 
2969{ int retValue_acc ;
2970
2971  {
2972#line 167
2973  if (handle == 1) {
2974#line 144 "ClientLib.c"
2975    if (index == 0) {
2976#line 1086
2977      retValue_acc = __ste_Client_AddressBook0_Alias0;
2978#line 1088
2979      return (retValue_acc);
2980    } else {
2981#line 1090
2982      if (index == 1) {
2983#line 1095
2984        retValue_acc = __ste_Client_AddressBook0_Alias1;
2985#line 1097
2986        return (retValue_acc);
2987      } else {
2988#line 1099
2989        if (index == 2) {
2990#line 1104
2991          retValue_acc = __ste_Client_AddressBook0_Alias2;
2992#line 1106
2993          return (retValue_acc);
2994        } else {
2995#line 1112
2996          retValue_acc = 0;
2997#line 1114
2998          return (retValue_acc);
2999        }
3000      }
3001    }
3002  } else {
3003#line 1116 "ClientLib.c"
3004    if (handle == 2) {
3005#line 154 "ClientLib.c"
3006      if (index == 0) {
3007#line 1124
3008        retValue_acc = __ste_Client_AddressBook1_Alias0;
3009#line 1126
3010        return (retValue_acc);
3011      } else {
3012#line 1128
3013        if (index == 1) {
3014#line 1133
3015          retValue_acc = __ste_Client_AddressBook1_Alias1;
3016#line 1135
3017          return (retValue_acc);
3018        } else {
3019#line 1137
3020          if (index == 2) {
3021#line 1142
3022            retValue_acc = __ste_Client_AddressBook1_Alias2;
3023#line 1144
3024            return (retValue_acc);
3025          } else {
3026#line 1150
3027            retValue_acc = 0;
3028#line 1152
3029            return (retValue_acc);
3030          }
3031        }
3032      }
3033    } else {
3034#line 1154 "ClientLib.c"
3035      if (handle == 3) {
3036#line 164 "ClientLib.c"
3037        if (index == 0) {
3038#line 1162
3039          retValue_acc = __ste_Client_AddressBook2_Alias0;
3040#line 1164
3041          return (retValue_acc);
3042        } else {
3043#line 1166
3044          if (index == 1) {
3045#line 1171
3046            retValue_acc = __ste_Client_AddressBook2_Alias1;
3047#line 1173
3048            return (retValue_acc);
3049          } else {
3050#line 1175
3051            if (index == 2) {
3052#line 1180
3053              retValue_acc = __ste_Client_AddressBook2_Alias2;
3054#line 1182
3055              return (retValue_acc);
3056            } else {
3057#line 1188
3058              retValue_acc = 0;
3059#line 1190
3060              return (retValue_acc);
3061            }
3062          }
3063        }
3064      } else {
3065#line 1196 "ClientLib.c"
3066        retValue_acc = 0;
3067#line 1198
3068        return (retValue_acc);
3069      }
3070    }
3071  }
3072#line 1205 "ClientLib.c"
3073  return (retValue_acc);
3074}
3075}
3076#line 171 "ClientLib.c"
3077int findClientAddressBookAlias(int handle , int userid ) 
3078{ int retValue_acc ;
3079
3080  {
3081#line 204
3082  if (handle == 1) {
3083#line 181 "ClientLib.c"
3084    if (userid == __ste_Client_AddressBook0_Alias0) {
3085#line 1233
3086      retValue_acc = 0;
3087#line 1235
3088      return (retValue_acc);
3089    } else {
3090#line 1237
3091      if (userid == __ste_Client_AddressBook0_Alias1) {
3092#line 1242
3093        retValue_acc = 1;
3094#line 1244
3095        return (retValue_acc);
3096      } else {
3097#line 1246
3098        if (userid == __ste_Client_AddressBook0_Alias2) {
3099#line 1251
3100          retValue_acc = 2;
3101#line 1253
3102          return (retValue_acc);
3103        } else {
3104#line 1259
3105          retValue_acc = -1;
3106#line 1261
3107          return (retValue_acc);
3108        }
3109      }
3110    }
3111  } else {
3112#line 1263 "ClientLib.c"
3113    if (handle == 2) {
3114#line 191 "ClientLib.c"
3115      if (userid == __ste_Client_AddressBook1_Alias0) {
3116#line 1271
3117        retValue_acc = 0;
3118#line 1273
3119        return (retValue_acc);
3120      } else {
3121#line 1275
3122        if (userid == __ste_Client_AddressBook1_Alias1) {
3123#line 1280
3124          retValue_acc = 1;
3125#line 1282
3126          return (retValue_acc);
3127        } else {
3128#line 1284
3129          if (userid == __ste_Client_AddressBook1_Alias2) {
3130#line 1289
3131            retValue_acc = 2;
3132#line 1291
3133            return (retValue_acc);
3134          } else {
3135#line 1297
3136            retValue_acc = -1;
3137#line 1299
3138            return (retValue_acc);
3139          }
3140        }
3141      }
3142    } else {
3143#line 1301 "ClientLib.c"
3144      if (handle == 3) {
3145#line 201 "ClientLib.c"
3146        if (userid == __ste_Client_AddressBook2_Alias0) {
3147#line 1309
3148          retValue_acc = 0;
3149#line 1311
3150          return (retValue_acc);
3151        } else {
3152#line 1313
3153          if (userid == __ste_Client_AddressBook2_Alias1) {
3154#line 1318
3155            retValue_acc = 1;
3156#line 1320
3157            return (retValue_acc);
3158          } else {
3159#line 1322
3160            if (userid == __ste_Client_AddressBook2_Alias2) {
3161#line 1327
3162              retValue_acc = 2;
3163#line 1329
3164              return (retValue_acc);
3165            } else {
3166#line 1335
3167              retValue_acc = -1;
3168#line 1337
3169              return (retValue_acc);
3170            }
3171          }
3172        }
3173      } else {
3174#line 1343 "ClientLib.c"
3175        retValue_acc = -1;
3176#line 1345
3177        return (retValue_acc);
3178      }
3179    }
3180  }
3181#line 1352 "ClientLib.c"
3182  return (retValue_acc);
3183}
3184}
3185#line 208 "ClientLib.c"
3186void setClientAddressBookAlias(int handle , int index , int value ) 
3187{ 
3188
3189  {
3190#line 234
3191  if (handle == 1) {
3192#line 217
3193    if (index == 0) {
3194#line 211
3195      __ste_Client_AddressBook0_Alias0 = value;
3196    } else {
3197#line 212
3198      if (index == 1) {
3199#line 213
3200        __ste_Client_AddressBook0_Alias1 = value;
3201      } else {
3202#line 214
3203        if (index == 2) {
3204#line 215
3205          __ste_Client_AddressBook0_Alias2 = value;
3206        } else {
3207
3208        }
3209      }
3210    }
3211  } else {
3212#line 216
3213    if (handle == 2) {
3214#line 225
3215      if (index == 0) {
3216#line 219
3217        __ste_Client_AddressBook1_Alias0 = value;
3218      } else {
3219#line 220
3220        if (index == 1) {
3221#line 221
3222          __ste_Client_AddressBook1_Alias1 = value;
3223        } else {
3224#line 222
3225          if (index == 2) {
3226#line 223
3227            __ste_Client_AddressBook1_Alias2 = value;
3228          } else {
3229
3230          }
3231        }
3232      }
3233    } else {
3234#line 224
3235      if (handle == 3) {
3236#line 233
3237        if (index == 0) {
3238#line 227
3239          __ste_Client_AddressBook2_Alias0 = value;
3240        } else {
3241#line 228
3242          if (index == 1) {
3243#line 229
3244            __ste_Client_AddressBook2_Alias1 = value;
3245          } else {
3246#line 230
3247            if (index == 2) {
3248#line 231
3249              __ste_Client_AddressBook2_Alias2 = value;
3250            } else {
3251
3252            }
3253          }
3254        }
3255      } else {
3256
3257      }
3258    }
3259  }
3260#line 1420 "ClientLib.c"
3261  return;
3262}
3263}
3264#line 236 "ClientLib.c"
3265int __ste_Client_AddressBook0_Address0  =    0;
3266#line 238 "ClientLib.c"
3267int __ste_Client_AddressBook0_Address1  =    0;
3268#line 240 "ClientLib.c"
3269int __ste_Client_AddressBook0_Address2  =    0;
3270#line 242 "ClientLib.c"
3271int __ste_Client_AddressBook1_Address0  =    0;
3272#line 244 "ClientLib.c"
3273int __ste_Client_AddressBook1_Address1  =    0;
3274#line 246 "ClientLib.c"
3275int __ste_Client_AddressBook1_Address2  =    0;
3276#line 248 "ClientLib.c"
3277int __ste_Client_AddressBook2_Address0  =    0;
3278#line 250 "ClientLib.c"
3279int __ste_Client_AddressBook2_Address1  =    0;
3280#line 252 "ClientLib.c"
3281int __ste_Client_AddressBook2_Address2  =    0;
3282#line 255 "ClientLib.c"
3283int getClientAddressBookAddress(int handle , int index ) 
3284{ int retValue_acc ;
3285
3286  {
3287#line 288
3288  if (handle == 1) {
3289#line 265 "ClientLib.c"
3290    if (index == 0) {
3291#line 1462
3292      retValue_acc = __ste_Client_AddressBook0_Address0;
3293#line 1464
3294      return (retValue_acc);
3295    } else {
3296#line 1466
3297      if (index == 1) {
3298#line 1471
3299        retValue_acc = __ste_Client_AddressBook0_Address1;
3300#line 1473
3301        return (retValue_acc);
3302      } else {
3303#line 1475
3304        if (index == 2) {
3305#line 1480
3306          retValue_acc = __ste_Client_AddressBook0_Address2;
3307#line 1482
3308          return (retValue_acc);
3309        } else {
3310#line 1488
3311          retValue_acc = 0;
3312#line 1490
3313          return (retValue_acc);
3314        }
3315      }
3316    }
3317  } else {
3318#line 1492 "ClientLib.c"
3319    if (handle == 2) {
3320#line 275 "ClientLib.c"
3321      if (index == 0) {
3322#line 1500
3323        retValue_acc = __ste_Client_AddressBook1_Address0;
3324#line 1502
3325        return (retValue_acc);
3326      } else {
3327#line 1504
3328        if (index == 1) {
3329#line 1509
3330          retValue_acc = __ste_Client_AddressBook1_Address1;
3331#line 1511
3332          return (retValue_acc);
3333        } else {
3334#line 1513
3335          if (index == 2) {
3336#line 1518
3337            retValue_acc = __ste_Client_AddressBook1_Address2;
3338#line 1520
3339            return (retValue_acc);
3340          } else {
3341#line 1526
3342            retValue_acc = 0;
3343#line 1528
3344            return (retValue_acc);
3345          }
3346        }
3347      }
3348    } else {
3349#line 1530 "ClientLib.c"
3350      if (handle == 3) {
3351#line 285 "ClientLib.c"
3352        if (index == 0) {
3353#line 1538
3354          retValue_acc = __ste_Client_AddressBook2_Address0;
3355#line 1540
3356          return (retValue_acc);
3357        } else {
3358#line 1542
3359          if (index == 1) {
3360#line 1547
3361            retValue_acc = __ste_Client_AddressBook2_Address1;
3362#line 1549
3363            return (retValue_acc);
3364          } else {
3365#line 1551
3366            if (index == 2) {
3367#line 1556
3368              retValue_acc = __ste_Client_AddressBook2_Address2;
3369#line 1558
3370              return (retValue_acc);
3371            } else {
3372#line 1564
3373              retValue_acc = 0;
3374#line 1566
3375              return (retValue_acc);
3376            }
3377          }
3378        }
3379      } else {
3380#line 1572 "ClientLib.c"
3381        retValue_acc = 0;
3382#line 1574
3383        return (retValue_acc);
3384      }
3385    }
3386  }
3387#line 1581 "ClientLib.c"
3388  return (retValue_acc);
3389}
3390}
3391#line 291 "ClientLib.c"
3392void setClientAddressBookAddress(int handle , int index , int value ) 
3393{ 
3394
3395  {
3396#line 317
3397  if (handle == 1) {
3398#line 300
3399    if (index == 0) {
3400#line 294
3401      __ste_Client_AddressBook0_Address0 = value;
3402    } else {
3403#line 295
3404      if (index == 1) {
3405#line 296
3406        __ste_Client_AddressBook0_Address1 = value;
3407      } else {
3408#line 297
3409        if (index == 2) {
3410#line 298
3411          __ste_Client_AddressBook0_Address2 = value;
3412        } else {
3413
3414        }
3415      }
3416    }
3417  } else {
3418#line 299
3419    if (handle == 2) {
3420#line 308
3421      if (index == 0) {
3422#line 302
3423        __ste_Client_AddressBook1_Address0 = value;
3424      } else {
3425#line 303
3426        if (index == 1) {
3427#line 304
3428          __ste_Client_AddressBook1_Address1 = value;
3429        } else {
3430#line 305
3431          if (index == 2) {
3432#line 306
3433            __ste_Client_AddressBook1_Address2 = value;
3434          } else {
3435
3436          }
3437        }
3438      }
3439    } else {
3440#line 307
3441      if (handle == 3) {
3442#line 316
3443        if (index == 0) {
3444#line 310
3445          __ste_Client_AddressBook2_Address0 = value;
3446        } else {
3447#line 311
3448          if (index == 1) {
3449#line 312
3450            __ste_Client_AddressBook2_Address1 = value;
3451          } else {
3452#line 313
3453            if (index == 2) {
3454#line 314
3455              __ste_Client_AddressBook2_Address2 = value;
3456            } else {
3457
3458            }
3459          }
3460        }
3461      } else {
3462
3463      }
3464    }
3465  }
3466#line 1649 "ClientLib.c"
3467  return;
3468}
3469}
3470#line 319 "ClientLib.c"
3471int __ste_client_autoResponse0  =    0;
3472#line 321 "ClientLib.c"
3473int __ste_client_autoResponse1  =    0;
3474#line 323 "ClientLib.c"
3475int __ste_client_autoResponse2  =    0;
3476#line 326 "ClientLib.c"
3477int getClientAutoResponse(int handle ) 
3478{ int retValue_acc ;
3479
3480  {
3481#line 335 "ClientLib.c"
3482  if (handle == 1) {
3483#line 1676
3484    retValue_acc = __ste_client_autoResponse0;
3485#line 1678
3486    return (retValue_acc);
3487  } else {
3488#line 1680
3489    if (handle == 2) {
3490#line 1685
3491      retValue_acc = __ste_client_autoResponse1;
3492#line 1687
3493      return (retValue_acc);
3494    } else {
3495#line 1689
3496      if (handle == 3) {
3497#line 1694
3498        retValue_acc = __ste_client_autoResponse2;
3499#line 1696
3500        return (retValue_acc);
3501      } else {
3502#line 1702 "ClientLib.c"
3503        retValue_acc = -1;
3504#line 1704
3505        return (retValue_acc);
3506      }
3507    }
3508  }
3509#line 1711 "ClientLib.c"
3510  return (retValue_acc);
3511}
3512}
3513#line 338 "ClientLib.c"
3514void setClientAutoResponse(int handle , int value ) 
3515{ 
3516
3517  {
3518#line 346
3519  if (handle == 1) {
3520#line 340
3521    __ste_client_autoResponse0 = value;
3522  } else {
3523#line 341
3524    if (handle == 2) {
3525#line 342
3526      __ste_client_autoResponse1 = value;
3527    } else {
3528#line 343
3529      if (handle == 3) {
3530#line 344
3531        __ste_client_autoResponse2 = value;
3532      } else {
3533
3534      }
3535    }
3536  }
3537#line 1746 "ClientLib.c"
3538  return;
3539}
3540}
3541#line 348 "ClientLib.c"
3542int __ste_client_privateKey0  =    0;
3543#line 350 "ClientLib.c"
3544int __ste_client_privateKey1  =    0;
3545#line 352 "ClientLib.c"
3546int __ste_client_privateKey2  =    0;
3547#line 355 "ClientLib.c"
3548int getClientPrivateKey(int handle ) 
3549{ int retValue_acc ;
3550
3551  {
3552#line 364 "ClientLib.c"
3553  if (handle == 1) {
3554#line 1773
3555    retValue_acc = __ste_client_privateKey0;
3556#line 1775
3557    return (retValue_acc);
3558  } else {
3559#line 1777
3560    if (handle == 2) {
3561#line 1782
3562      retValue_acc = __ste_client_privateKey1;
3563#line 1784
3564      return (retValue_acc);
3565    } else {
3566#line 1786
3567      if (handle == 3) {
3568#line 1791
3569        retValue_acc = __ste_client_privateKey2;
3570#line 1793
3571        return (retValue_acc);
3572      } else {
3573#line 1799 "ClientLib.c"
3574        retValue_acc = 0;
3575#line 1801
3576        return (retValue_acc);
3577      }
3578    }
3579  }
3580#line 1808 "ClientLib.c"
3581  return (retValue_acc);
3582}
3583}
3584#line 367 "ClientLib.c"
3585void setClientPrivateKey(int handle , int value ) 
3586{ 
3587
3588  {
3589#line 375
3590  if (handle == 1) {
3591#line 369
3592    __ste_client_privateKey0 = value;
3593  } else {
3594#line 370
3595    if (handle == 2) {
3596#line 371
3597      __ste_client_privateKey1 = value;
3598    } else {
3599#line 372
3600      if (handle == 3) {
3601#line 373
3602        __ste_client_privateKey2 = value;
3603      } else {
3604
3605      }
3606    }
3607  }
3608#line 1843 "ClientLib.c"
3609  return;
3610}
3611}
3612#line 377 "ClientLib.c"
3613int __ste_ClientKeyring_size0  =    0;
3614#line 379 "ClientLib.c"
3615int __ste_ClientKeyring_size1  =    0;
3616#line 381 "ClientLib.c"
3617int __ste_ClientKeyring_size2  =    0;
3618#line 384 "ClientLib.c"
3619int getClientKeyringSize(int handle ) 
3620{ int retValue_acc ;
3621
3622  {
3623#line 393 "ClientLib.c"
3624  if (handle == 1) {
3625#line 1870
3626    retValue_acc = __ste_ClientKeyring_size0;
3627#line 1872
3628    return (retValue_acc);
3629  } else {
3630#line 1874
3631    if (handle == 2) {
3632#line 1879
3633      retValue_acc = __ste_ClientKeyring_size1;
3634#line 1881
3635      return (retValue_acc);
3636    } else {
3637#line 1883
3638      if (handle == 3) {
3639#line 1888
3640        retValue_acc = __ste_ClientKeyring_size2;
3641#line 1890
3642        return (retValue_acc);
3643      } else {
3644#line 1896 "ClientLib.c"
3645        retValue_acc = 0;
3646#line 1898
3647        return (retValue_acc);
3648      }
3649    }
3650  }
3651#line 1905 "ClientLib.c"
3652  return (retValue_acc);
3653}
3654}
3655#line 396 "ClientLib.c"
3656void setClientKeyringSize(int handle , int value ) 
3657{ 
3658
3659  {
3660#line 404
3661  if (handle == 1) {
3662#line 398
3663    __ste_ClientKeyring_size0 = value;
3664  } else {
3665#line 399
3666    if (handle == 2) {
3667#line 400
3668      __ste_ClientKeyring_size1 = value;
3669    } else {
3670#line 401
3671      if (handle == 3) {
3672#line 402
3673        __ste_ClientKeyring_size2 = value;
3674      } else {
3675
3676      }
3677    }
3678  }
3679#line 1940 "ClientLib.c"
3680  return;
3681}
3682}
3683#line 406 "ClientLib.c"
3684int createClientKeyringEntry(int handle ) 
3685{ int retValue_acc ;
3686  int size ;
3687  int tmp ;
3688  int __cil_tmp5 ;
3689
3690  {
3691  {
3692#line 407
3693  tmp = getClientKeyringSize(handle);
3694#line 407
3695  size = tmp;
3696  }
3697#line 408 "ClientLib.c"
3698  if (size < 2) {
3699    {
3700#line 409 "ClientLib.c"
3701    __cil_tmp5 = size + 1;
3702#line 409
3703    setClientKeyringSize(handle, __cil_tmp5);
3704#line 1967 "ClientLib.c"
3705    retValue_acc = size + 1;
3706    }
3707#line 1969
3708    return (retValue_acc);
3709  } else {
3710#line 1973 "ClientLib.c"
3711    retValue_acc = -1;
3712#line 1975
3713    return (retValue_acc);
3714  }
3715#line 1982 "ClientLib.c"
3716  return (retValue_acc);
3717}
3718}
3719#line 414 "ClientLib.c"
3720int __ste_Client_Keyring0_User0  =    0;
3721#line 416 "ClientLib.c"
3722int __ste_Client_Keyring0_User1  =    0;
3723#line 418 "ClientLib.c"
3724int __ste_Client_Keyring0_User2  =    0;
3725#line 420 "ClientLib.c"
3726int __ste_Client_Keyring1_User0  =    0;
3727#line 422 "ClientLib.c"
3728int __ste_Client_Keyring1_User1  =    0;
3729#line 424 "ClientLib.c"
3730int __ste_Client_Keyring1_User2  =    0;
3731#line 426 "ClientLib.c"
3732int __ste_Client_Keyring2_User0  =    0;
3733#line 428 "ClientLib.c"
3734int __ste_Client_Keyring2_User1  =    0;
3735#line 430 "ClientLib.c"
3736int __ste_Client_Keyring2_User2  =    0;
3737#line 433 "ClientLib.c"
3738int getClientKeyringUser(int handle , int index ) 
3739{ int retValue_acc ;
3740
3741  {
3742#line 466
3743  if (handle == 1) {
3744#line 443 "ClientLib.c"
3745    if (index == 0) {
3746#line 2028
3747      retValue_acc = __ste_Client_Keyring0_User0;
3748#line 2030
3749      return (retValue_acc);
3750    } else {
3751#line 2032
3752      if (index == 1) {
3753#line 2037
3754        retValue_acc = __ste_Client_Keyring0_User1;
3755#line 2039
3756        return (retValue_acc);
3757      } else {
3758#line 2045
3759        retValue_acc = 0;
3760#line 2047
3761        return (retValue_acc);
3762      }
3763    }
3764  } else {
3765#line 2049 "ClientLib.c"
3766    if (handle == 2) {
3767#line 453 "ClientLib.c"
3768      if (index == 0) {
3769#line 2057
3770        retValue_acc = __ste_Client_Keyring1_User0;
3771#line 2059
3772        return (retValue_acc);
3773      } else {
3774#line 2061
3775        if (index == 1) {
3776#line 2066
3777          retValue_acc = __ste_Client_Keyring1_User1;
3778#line 2068
3779          return (retValue_acc);
3780        } else {
3781#line 2074
3782          retValue_acc = 0;
3783#line 2076
3784          return (retValue_acc);
3785        }
3786      }
3787    } else {
3788#line 2078 "ClientLib.c"
3789      if (handle == 3) {
3790#line 463 "ClientLib.c"
3791        if (index == 0) {
3792#line 2086
3793          retValue_acc = __ste_Client_Keyring2_User0;
3794#line 2088
3795          return (retValue_acc);
3796        } else {
3797#line 2090
3798          if (index == 1) {
3799#line 2095
3800            retValue_acc = __ste_Client_Keyring2_User1;
3801#line 2097
3802            return (retValue_acc);
3803          } else {
3804#line 2103
3805            retValue_acc = 0;
3806#line 2105
3807            return (retValue_acc);
3808          }
3809        }
3810      } else {
3811#line 2111 "ClientLib.c"
3812        retValue_acc = 0;
3813#line 2113
3814        return (retValue_acc);
3815      }
3816    }
3817  }
3818#line 2120 "ClientLib.c"
3819  return (retValue_acc);
3820}
3821}
3822#line 473 "ClientLib.c"
3823void setClientKeyringUser(int handle , int index , int value ) 
3824{ 
3825
3826  {
3827#line 499
3828  if (handle == 1) {
3829#line 482
3830    if (index == 0) {
3831#line 476
3832      __ste_Client_Keyring0_User0 = value;
3833    } else {
3834#line 477
3835      if (index == 1) {
3836#line 478
3837        __ste_Client_Keyring0_User1 = value;
3838      } else {
3839
3840      }
3841    }
3842  } else {
3843#line 479
3844    if (handle == 2) {
3845#line 490
3846      if (index == 0) {
3847#line 484
3848        __ste_Client_Keyring1_User0 = value;
3849      } else {
3850#line 485
3851        if (index == 1) {
3852#line 486
3853          __ste_Client_Keyring1_User1 = value;
3854        } else {
3855
3856        }
3857      }
3858    } else {
3859#line 487
3860      if (handle == 3) {
3861#line 498
3862        if (index == 0) {
3863#line 492
3864          __ste_Client_Keyring2_User0 = value;
3865        } else {
3866#line 493
3867          if (index == 1) {
3868#line 494
3869            __ste_Client_Keyring2_User1 = value;
3870          } else {
3871
3872          }
3873        }
3874      } else {
3875
3876      }
3877    }
3878  }
3879#line 2176 "ClientLib.c"
3880  return;
3881}
3882}
3883#line 501 "ClientLib.c"
3884int __ste_Client_Keyring0_PublicKey0  =    0;
3885#line 503 "ClientLib.c"
3886int __ste_Client_Keyring0_PublicKey1  =    0;
3887#line 505 "ClientLib.c"
3888int __ste_Client_Keyring0_PublicKey2  =    0;
3889#line 507 "ClientLib.c"
3890int __ste_Client_Keyring1_PublicKey0  =    0;
3891#line 509 "ClientLib.c"
3892int __ste_Client_Keyring1_PublicKey1  =    0;
3893#line 511 "ClientLib.c"
3894int __ste_Client_Keyring1_PublicKey2  =    0;
3895#line 513 "ClientLib.c"
3896int __ste_Client_Keyring2_PublicKey0  =    0;
3897#line 515 "ClientLib.c"
3898int __ste_Client_Keyring2_PublicKey1  =    0;
3899#line 517 "ClientLib.c"
3900int __ste_Client_Keyring2_PublicKey2  =    0;
3901#line 520 "ClientLib.c"
3902int getClientKeyringPublicKey(int handle , int index ) 
3903{ int retValue_acc ;
3904
3905  {
3906#line 553
3907  if (handle == 1) {
3908#line 530 "ClientLib.c"
3909    if (index == 0) {
3910#line 2218
3911      retValue_acc = __ste_Client_Keyring0_PublicKey0;
3912#line 2220
3913      return (retValue_acc);
3914    } else {
3915#line 2222
3916      if (index == 1) {
3917#line 2227
3918        retValue_acc = __ste_Client_Keyring0_PublicKey1;
3919#line 2229
3920        return (retValue_acc);
3921      } else {
3922#line 2235
3923        retValue_acc = 0;
3924#line 2237
3925        return (retValue_acc);
3926      }
3927    }
3928  } else {
3929#line 2239 "ClientLib.c"
3930    if (handle == 2) {
3931#line 540 "ClientLib.c"
3932      if (index == 0) {
3933#line 2247
3934        retValue_acc = __ste_Client_Keyring1_PublicKey0;
3935#line 2249
3936        return (retValue_acc);
3937      } else {
3938#line 2251
3939        if (index == 1) {
3940#line 2256
3941          retValue_acc = __ste_Client_Keyring1_PublicKey1;
3942#line 2258
3943          return (retValue_acc);
3944        } else {
3945#line 2264
3946          retValue_acc = 0;
3947#line 2266
3948          return (retValue_acc);
3949        }
3950      }
3951    } else {
3952#line 2268 "ClientLib.c"
3953      if (handle == 3) {
3954#line 550 "ClientLib.c"
3955        if (index == 0) {
3956#line 2276
3957          retValue_acc = __ste_Client_Keyring2_PublicKey0;
3958#line 2278
3959          return (retValue_acc);
3960        } else {
3961#line 2280
3962          if (index == 1) {
3963#line 2285
3964            retValue_acc = __ste_Client_Keyring2_PublicKey1;
3965#line 2287
3966            return (retValue_acc);
3967          } else {
3968#line 2293
3969            retValue_acc = 0;
3970#line 2295
3971            return (retValue_acc);
3972          }
3973        }
3974      } else {
3975#line 2301 "ClientLib.c"
3976        retValue_acc = 0;
3977#line 2303
3978        return (retValue_acc);
3979      }
3980    }
3981  }
3982#line 2310 "ClientLib.c"
3983  return (retValue_acc);
3984}
3985}
3986#line 557 "ClientLib.c"
3987int findPublicKey(int handle , int userid ) 
3988{ int retValue_acc ;
3989
3990  {
3991#line 591
3992  if (handle == 1) {
3993#line 568 "ClientLib.c"
3994    if (userid == __ste_Client_Keyring0_User0) {
3995#line 2338
3996      retValue_acc = __ste_Client_Keyring0_PublicKey0;
3997#line 2340
3998      return (retValue_acc);
3999    } else {
4000#line 2342
4001      if (userid == __ste_Client_Keyring0_User1) {
4002#line 2347
4003        retValue_acc = __ste_Client_Keyring0_PublicKey1;
4004#line 2349
4005        return (retValue_acc);
4006      } else {
4007#line 2355
4008        retValue_acc = 0;
4009#line 2357
4010        return (retValue_acc);
4011      }
4012    }
4013  } else {
4014#line 2359 "ClientLib.c"
4015    if (handle == 2) {
4016#line 578 "ClientLib.c"
4017      if (userid == __ste_Client_Keyring1_User0) {
4018#line 2367
4019        retValue_acc = __ste_Client_Keyring1_PublicKey0;
4020#line 2369
4021        return (retValue_acc);
4022      } else {
4023#line 2371
4024        if (userid == __ste_Client_Keyring1_User1) {
4025#line 2376
4026          retValue_acc = __ste_Client_Keyring1_PublicKey1;
4027#line 2378
4028          return (retValue_acc);
4029        } else {
4030#line 2384
4031          retValue_acc = 0;
4032#line 2386
4033          return (retValue_acc);
4034        }
4035      }
4036    } else {
4037#line 2388 "ClientLib.c"
4038      if (handle == 3) {
4039#line 588 "ClientLib.c"
4040        if (userid == __ste_Client_Keyring2_User0) {
4041#line 2396
4042          retValue_acc = __ste_Client_Keyring2_PublicKey0;
4043#line 2398
4044          return (retValue_acc);
4045        } else {
4046#line 2400
4047          if (userid == __ste_Client_Keyring2_User1) {
4048#line 2405
4049            retValue_acc = __ste_Client_Keyring2_PublicKey1;
4050#line 2407
4051            return (retValue_acc);
4052          } else {
4053#line 2413
4054            retValue_acc = 0;
4055#line 2415
4056            return (retValue_acc);
4057          }
4058        }
4059      } else {
4060#line 2421 "ClientLib.c"
4061        retValue_acc = 0;
4062#line 2423
4063        return (retValue_acc);
4064      }
4065    }
4066  }
4067#line 2430 "ClientLib.c"
4068  return (retValue_acc);
4069}
4070}
4071#line 595 "ClientLib.c"
4072void setClientKeyringPublicKey(int handle , int index , int value ) 
4073{ 
4074
4075  {
4076#line 621
4077  if (handle == 1) {
4078#line 604
4079    if (index == 0) {
4080#line 598
4081      __ste_Client_Keyring0_PublicKey0 = value;
4082    } else {
4083#line 599
4084      if (index == 1) {
4085#line 600
4086        __ste_Client_Keyring0_PublicKey1 = value;
4087      } else {
4088
4089      }
4090    }
4091  } else {
4092#line 601
4093    if (handle == 2) {
4094#line 612
4095      if (index == 0) {
4096#line 606
4097        __ste_Client_Keyring1_PublicKey0 = value;
4098      } else {
4099#line 607
4100        if (index == 1) {
4101#line 608
4102          __ste_Client_Keyring1_PublicKey1 = value;
4103        } else {
4104
4105        }
4106      }
4107    } else {
4108#line 609
4109      if (handle == 3) {
4110#line 620
4111        if (index == 0) {
4112#line 614
4113          __ste_Client_Keyring2_PublicKey0 = value;
4114        } else {
4115#line 615
4116          if (index == 1) {
4117#line 616
4118            __ste_Client_Keyring2_PublicKey1 = value;
4119          } else {
4120
4121          }
4122        }
4123      } else {
4124
4125      }
4126    }
4127  }
4128#line 2486 "ClientLib.c"
4129  return;
4130}
4131}
4132#line 623 "ClientLib.c"
4133int __ste_client_forwardReceiver0  =    0;
4134#line 625 "ClientLib.c"
4135int __ste_client_forwardReceiver1  =    0;
4136#line 627 "ClientLib.c"
4137int __ste_client_forwardReceiver2  =    0;
4138#line 629 "ClientLib.c"
4139int __ste_client_forwardReceiver3  =    0;
4140#line 631 "ClientLib.c"
4141int getClientForwardReceiver(int handle ) 
4142{ int retValue_acc ;
4143
4144  {
4145#line 640 "ClientLib.c"
4146  if (handle == 1) {
4147#line 2515
4148    retValue_acc = __ste_client_forwardReceiver0;
4149#line 2517
4150    return (retValue_acc);
4151  } else {
4152#line 2519
4153    if (handle == 2) {
4154#line 2524
4155      retValue_acc = __ste_client_forwardReceiver1;
4156#line 2526
4157      return (retValue_acc);
4158    } else {
4159#line 2528
4160      if (handle == 3) {
4161#line 2533
4162        retValue_acc = __ste_client_forwardReceiver2;
4163#line 2535
4164        return (retValue_acc);
4165      } else {
4166#line 2541 "ClientLib.c"
4167        retValue_acc = 0;
4168#line 2543
4169        return (retValue_acc);
4170      }
4171    }
4172  }
4173#line 2550 "ClientLib.c"
4174  return (retValue_acc);
4175}
4176}
4177#line 643 "ClientLib.c"
4178void setClientForwardReceiver(int handle , int value ) 
4179{ 
4180
4181  {
4182#line 651
4183  if (handle == 1) {
4184#line 645
4185    __ste_client_forwardReceiver0 = value;
4186  } else {
4187#line 646
4188    if (handle == 2) {
4189#line 647
4190      __ste_client_forwardReceiver1 = value;
4191    } else {
4192#line 648
4193      if (handle == 3) {
4194#line 649
4195        __ste_client_forwardReceiver2 = value;
4196      } else {
4197
4198      }
4199    }
4200  }
4201#line 2585 "ClientLib.c"
4202  return;
4203}
4204}
4205#line 653 "ClientLib.c"
4206int __ste_client_idCounter0  =    0;
4207#line 655 "ClientLib.c"
4208int __ste_client_idCounter1  =    0;
4209#line 657 "ClientLib.c"
4210int __ste_client_idCounter2  =    0;
4211#line 660 "ClientLib.c"
4212int getClientId(int handle ) 
4213{ int retValue_acc ;
4214
4215  {
4216#line 669 "ClientLib.c"
4217  if (handle == 1) {
4218#line 2612
4219    retValue_acc = __ste_client_idCounter0;
4220#line 2614
4221    return (retValue_acc);
4222  } else {
4223#line 2616
4224    if (handle == 2) {
4225#line 2621
4226      retValue_acc = __ste_client_idCounter1;
4227#line 2623
4228      return (retValue_acc);
4229    } else {
4230#line 2625
4231      if (handle == 3) {
4232#line 2630
4233        retValue_acc = __ste_client_idCounter2;
4234#line 2632
4235        return (retValue_acc);
4236      } else {
4237#line 2638 "ClientLib.c"
4238        retValue_acc = 0;
4239#line 2640
4240        return (retValue_acc);
4241      }
4242    }
4243  }
4244#line 2647 "ClientLib.c"
4245  return (retValue_acc);
4246}
4247}
4248#line 672 "ClientLib.c"
4249void setClientId(int handle , int value ) 
4250{ 
4251
4252  {
4253#line 680
4254  if (handle == 1) {
4255#line 674
4256    __ste_client_idCounter0 = value;
4257  } else {
4258#line 675
4259    if (handle == 2) {
4260#line 676
4261      __ste_client_idCounter1 = value;
4262    } else {
4263#line 677
4264      if (handle == 3) {
4265#line 678
4266        __ste_client_idCounter2 = value;
4267      } else {
4268
4269      }
4270    }
4271  }
4272#line 2682 "ClientLib.c"
4273  return;
4274}
4275}