ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1722

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