ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1772

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