ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1831

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