Showing error 1678

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