Showing error 1665

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