Showing error 1747

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