Showing error 1746

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