Showing error 1803

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