Showing error 1695

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