email_spec11_product26_false-unreach-call_true-termination.cil.c

extern void __VERIFIER_error() __attribute__ ((__noreturn__));

extern int __VERIFIER_nondet_int(void);
/* Generated by CIL v. 1.3.7 */
/* print_CIL_Input is true */

struct JoinPoint {
   void **(*fp)(struct JoinPoint * ) ;
   void **args ;
   int argsCount ;
   char const   **argsType ;
   void *(*arg)(int  , struct JoinPoint * ) ;
   char const   *(*argType)(int  , struct JoinPoint * ) ;
   void **retValue ;
   char const   *retType ;
   char const   *funcName ;
   char const   *targetName ;
   char const   *fileName ;
   char const   *kind ;
   void *excep_return ;
};
struct __UTAC__CFLOW_FUNC {
   int (*func)(int  , int  ) ;
   int val ;
   struct __UTAC__CFLOW_FUNC *next ;
};
struct __UTAC__EXCEPTION {
   void *jumpbuf ;
   unsigned long long prtValue ;
   int pops ;
   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
};
typedef unsigned int size_t;
struct __ACC__ERR {
   void *v ;
   struct __ACC__ERR *next ;
};
#pragma merger(0,"EmailLib.i","")
int initEmail(void) ;
int getEmailId(int handle ) ;
void setEmailId(int handle , int value ) ;
int getEmailFrom(int handle ) ;
void setEmailFrom(int handle , int value ) ;
int getEmailTo(int handle ) ;
void setEmailTo(int handle , int value ) ;
char *getEmailSubject(int handle ) ;
void setEmailSubject(int handle , char *value ) ;
char *getEmailBody(int handle ) ;
void setEmailBody(int handle , char *value ) ;
int isEncrypted(int handle ) ;
void setEmailIsEncrypted(int handle , int value ) ;
int getEmailEncryptionKey(int handle ) ;
void setEmailEncryptionKey(int handle , int value ) ;
int isSigned(int handle ) ;
void setEmailIsSigned(int handle , int value ) ;
int getEmailSignKey(int handle ) ;
void setEmailSignKey(int handle , int value ) ;
int isVerified(int handle ) ;
void setEmailIsSignatureVerified(int handle , int value ) ;
int __ste_Email_counter  =    0;
int initEmail(void) 
{ int retValue_acc ;

  {
  if (__ste_Email_counter < 2) {
    __ste_Email_counter = __ste_Email_counter + 1;
    retValue_acc = __ste_Email_counter;
    return (retValue_acc);
  } else {
    retValue_acc = -1;
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
int __ste_email_id0  =    0;
int __ste_email_id1  =    0;
int getEmailId(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_id0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_id1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailId(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_id0 = value;
  } else {
    if (handle == 2) {
      __ste_email_id1 = value;
    } else {

    }
  }
  return;
}
}
int __ste_email_from0  =    0;
int __ste_email_from1  =    0;
int getEmailFrom(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_from0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_from1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailFrom(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_from0 = value;
  } else {
    if (handle == 2) {
      __ste_email_from1 = value;
    } else {

    }
  }
  return;
}
}
int __ste_email_to0  =    0;
int __ste_email_to1  =    0;
int getEmailTo(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_to0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_to1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailTo(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_to0 = value;
  } else {
    if (handle == 2) {
      __ste_email_to1 = value;
    } else {

    }
  }
  return;
}
}
char *__ste_email_subject0  ;
char *__ste_email_subject1  ;
char *getEmailSubject(int handle ) 
{ char *retValue_acc ;
  void *__cil_tmp3 ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_subject0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_subject1;
      return (retValue_acc);
    } else {
      __cil_tmp3 = (void *)0;
      retValue_acc = (char *)__cil_tmp3;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailSubject(int handle , char *value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_subject0 = value;
  } else {
    if (handle == 2) {
      __ste_email_subject1 = value;
    } else {

    }
  }
  return;
}
}
char *__ste_email_body0  =    (char *)0;
char *__ste_email_body1  =    (char *)0;
char *getEmailBody(int handle ) 
{ char *retValue_acc ;
  void *__cil_tmp3 ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_body0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_body1;
      return (retValue_acc);
    } else {
      __cil_tmp3 = (void *)0;
      retValue_acc = (char *)__cil_tmp3;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailBody(int handle , char *value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_body0 = value;
  } else {
    if (handle == 2) {
      __ste_email_body1 = value;
    } else {

    }
  }
  return;
}
}
int __ste_email_isEncrypted0  =    0;
int __ste_email_isEncrypted1  =    0;
int isEncrypted(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_isEncrypted0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_isEncrypted1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailIsEncrypted(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_isEncrypted0 = value;
  } else {
    if (handle == 2) {
      __ste_email_isEncrypted1 = value;
    } else {

    }
  }
  return;
}
}
int __ste_email_encryptionKey0  =    0;
int __ste_email_encryptionKey1  =    0;
int getEmailEncryptionKey(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_encryptionKey0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_encryptionKey1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailEncryptionKey(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_encryptionKey0 = value;
  } else {
    if (handle == 2) {
      __ste_email_encryptionKey1 = value;
    } else {

    }
  }
  return;
}
}
int __ste_email_isSigned0  =    0;
int __ste_email_isSigned1  =    0;
int isSigned(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_isSigned0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_isSigned1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailIsSigned(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_isSigned0 = value;
  } else {
    if (handle == 2) {
      __ste_email_isSigned1 = value;
    } else {

    }
  }
  return;
}
}
int __ste_email_signKey0  =    0;
int __ste_email_signKey1  =    0;
int getEmailSignKey(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_signKey0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_signKey1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailSignKey(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_signKey0 = value;
  } else {
    if (handle == 2) {
      __ste_email_signKey1 = value;
    } else {

    }
  }
  return;
}
}
int __ste_email_isSignatureVerified0  ;
int __ste_email_isSignatureVerified1  ;
int isVerified(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_email_isSignatureVerified0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_email_isSignatureVerified1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
void setEmailIsSignatureVerified(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_email_isSignatureVerified0 = value;
  } else {
    if (handle == 2) {
      __ste_email_isSignatureVerified1 = value;
    } else {

    }
  }
  return;
}
}
#pragma merger(0,"Email.i","")
extern int printf(char const   * __restrict  __format  , ...) ;
int __SELECTED_FEATURE_Base  ;
int __SELECTED_FEATURE_Keys  ;
int __SELECTED_FEATURE_Encrypt  ;
int __SELECTED_FEATURE_AutoResponder  ;
int __SELECTED_FEATURE_AddressBook  ;
int __SELECTED_FEATURE_Sign  ;
int __SELECTED_FEATURE_Forward  ;
int __SELECTED_FEATURE_Verify  ;
int __SELECTED_FEATURE_Decrypt  ;
int __GUIDSL_ROOT_PRODUCTION  ;
int __GUIDSL_NON_TERMINAL_main  ;
void printMail(int msg ) ;
int isReadable(int msg ) ;
int createEmail(int from , int to ) ;
int cloneEmail(int msg ) ;
void printMail__wrappee__Keys(int msg ) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  char const   * __restrict  __cil_tmp6 ;
  char const   * __restrict  __cil_tmp7 ;
  char const   * __restrict  __cil_tmp8 ;
  char const   * __restrict  __cil_tmp9 ;

  {
  {
  tmp = getEmailId(msg);
  __cil_tmp6 = (char const   * __restrict  )"ID:\n  %i\n";
  printf(__cil_tmp6, tmp);
  tmp___0 = getEmailFrom(msg);
  __cil_tmp7 = (char const   * __restrict  )"FROM:\n  %i\n";
  printf(__cil_tmp7, tmp___0);
  tmp___1 = getEmailTo(msg);
  __cil_tmp8 = (char const   * __restrict  )"TO:\n  %i\n";
  printf(__cil_tmp8, tmp___1);
  tmp___2 = isReadable(msg);
  __cil_tmp9 = (char const   * __restrict  )"IS_READABLE\n  %i\n";
  printf(__cil_tmp9, tmp___2);
  }
  return;
}
}
void printMail(int msg ) 
{ int tmp ;
  int tmp___0 ;
  char const   * __restrict  __cil_tmp4 ;
  char const   * __restrict  __cil_tmp5 ;

  {
  {
  printMail__wrappee__Keys(msg);
  tmp = isEncrypted(msg);
  __cil_tmp4 = (char const   * __restrict  )"ENCRYPTED\n  %d\n";
  printf(__cil_tmp4, tmp);
  tmp___0 = getEmailEncryptionKey(msg);
  __cil_tmp5 = (char const   * __restrict  )"ENCRYPTION KEY\n  %d\n";
  printf(__cil_tmp5, tmp___0);
  }
  return;
}
}
int isReadable__wrappee__Keys(int msg ) 
{ int retValue_acc ;

  {
  retValue_acc = 1;
  return (retValue_acc);
  return (retValue_acc);
}
}
int isReadable(int msg ) 
{ int retValue_acc ;
  int tmp ;

  {
  {
  tmp = isEncrypted(msg);
  }
  if (tmp) {
    retValue_acc = 0;
    return (retValue_acc);
  } else {
    {
    retValue_acc = isReadable__wrappee__Keys(msg);
    }
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
int cloneEmail(int msg ) 
{ int retValue_acc ;

  {
  retValue_acc = msg;
  return (retValue_acc);
  return (retValue_acc);
}
}
int createEmail(int from , int to ) 
{ int retValue_acc ;
  int msg ;

  {
  {
  msg = 1;
  setEmailFrom(msg, from);
  setEmailTo(msg, to);
  retValue_acc = msg;
  }
  return (retValue_acc);
  return (retValue_acc);
}
}
#pragma merger(0,"featureselect.i","")
int select_one(void) ;
void select_features(void) ;
void select_helpers(void) ;
int valid_product(void) ;
int select_one(void) 
{ int retValue_acc ;
  int choice = __VERIFIER_nondet_int();

  {
  retValue_acc = choice;
  return (retValue_acc);
  return (retValue_acc);
}
}
void select_features(void) 
{ 

  {
  return;
}
}
void select_helpers(void) 
{ 

  {
  return;
}
}
int valid_product(void) 
{ int retValue_acc ;

  {
  retValue_acc = 1;
  return (retValue_acc);
  return (retValue_acc);
}
}
#pragma merger(0,"DecryptAutoResponder_spec.i","")
void __automaton_fail(void) ;
extern int puts(char const   *__s ) ;
inline static void __utac_acc__DecryptAutoResponder_spec__1(int client , int msg ) 
{ int tmp ;

  {
  {
  puts("before autoRespond\n");
  tmp = isReadable(msg);
  }
  if (tmp) {

  } else {
    {
    __automaton_fail();
    }
  }
  return;
}
}
#pragma merger(0,"Test.i","")
void setClientAddressBookSize(int handle , int value ) ;
void setClientAddressBookAlias(int handle , int index , int value ) ;
void setClientAddressBookAddress(int handle , int index , int value ) ;
void setClientAutoResponse(int handle , int value ) ;
void setClientPrivateKey(int handle , int value ) ;
int createClientKeyringEntry(int handle ) ;
int getClientKeyringUser(int handle , int index ) ;
void setClientKeyringUser(int handle , int index , int value ) ;
int getClientKeyringPublicKey(int handle , int index ) ;
void setClientKeyringPublicKey(int handle , int index , int value ) ;
void setClientForwardReceiver(int handle , int value ) ;
void setClientId(int handle , int value ) ;
int is_queue_empty(void) ;
int get_queued_client(void) ;
int get_queued_email(void) ;
void outgoing(int client , int msg ) ;
void sendEmail(int sender , int receiver ) ;
void generateKeyPair(int client , int seed ) ;
int bob  ;
int rjh  ;
int chuck  ;
void setup_bob(int bob___0 ) ;
void setup_rjh(int rjh___0 ) ;
void setup_chuck(int chuck___0 ) ;
void bobToRjh(void) ;
void rjhToBob(void) ;
void test(void) ;
void setup(void) ;
int main(void) ;
void bobKeyAdd(void) ;
void bobKeyAddChuck(void) ;
void rjhKeyAdd(void) ;
void rjhKeyAddChuck(void) ;
void chuckKeyAdd(void) ;
void bobKeyChange(void) ;
void rjhKeyChange(void) ;
void rjhDeletePrivateKey(void) ;
void chuckKeyAddRjh(void) ;
void rjhSetAutoRespond(void) ;
void bobSetAddressBook(void) ;
void rjhEnableForwarding(void) ;
void setup_bob__wrappee__Base(int bob___0 ) 
{ 

  {
  {
  setClientId(bob___0, bob___0);
  }
  return;
}
}
void setup_bob(int bob___0 ) 
{ 

  {
  {
  setup_bob__wrappee__Base(bob___0);
  setClientPrivateKey(bob___0, 123);
  }
  return;
}
}
void setup_rjh__wrappee__Base(int rjh___0 ) 
{ 

  {
  {
  setClientId(rjh___0, rjh___0);
  }
  return;
}
}
void setup_rjh(int rjh___0 ) 
{ 

  {
  {
  setup_rjh__wrappee__Base(rjh___0);
  setClientPrivateKey(rjh___0, 456);
  }
  return;
}
}
void setup_chuck__wrappee__Base(int chuck___0 ) 
{ 

  {
  {
  setClientId(chuck___0, chuck___0);
  }
  return;
}
}
void setup_chuck(int chuck___0 ) 
{ 

  {
  {
  setup_chuck__wrappee__Base(chuck___0);
  setClientPrivateKey(chuck___0, 789);
  }
  return;
}
}
void bobToRjh(void) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
  puts("Please enter a subject and a message body.\n");
  sendEmail(bob, rjh);
  tmp___1 = is_queue_empty();
  }
  if (tmp___1) {

  } else {
    {
    tmp = get_queued_email();
    tmp___0 = get_queued_client();
    outgoing(tmp___0, tmp);
    }
  }
  return;
}
}
void rjhToBob(void) 
{ 

  {
  {
  puts("Please enter a subject and a message body.\n");
  sendEmail(rjh, bob);
  }
  return;
}
}
void setup(void) 
{ char const   * __restrict  __cil_tmp1 ;
  char const   * __restrict  __cil_tmp2 ;
  char const   * __restrict  __cil_tmp3 ;

  {
  {
  bob = 1;
  setup_bob(bob);
  __cil_tmp1 = (char const   * __restrict  )"bob: %d\n";
  printf(__cil_tmp1, bob);
  rjh = 2;
  setup_rjh(rjh);
  __cil_tmp2 = (char const   * __restrict  )"rjh: %d\n";
  printf(__cil_tmp2, rjh);
  chuck = 3;
  setup_chuck(chuck);
  __cil_tmp3 = (char const   * __restrict  )"chuck: %d\n";
  printf(__cil_tmp3, chuck);
  }
  return;
}
}
int main(void) 
{ int retValue_acc ;
  int tmp ;

  {
  {
  select_helpers();
  select_features();
  tmp = valid_product();
  }
  if (tmp) {
    {
    setup();
    test();
    }
  } else {

  }
  return (retValue_acc);
}
}
void bobKeyAdd(void) 
{ int tmp ;
  int tmp___0 ;
  char const   * __restrict  __cil_tmp3 ;
  char const   * __restrict  __cil_tmp4 ;

  {
  {
  createClientKeyringEntry(bob);
  setClientKeyringUser(bob, 0, 2);
  setClientKeyringPublicKey(bob, 0, 456);
  puts("bob added rjhs key");
  tmp = getClientKeyringUser(bob, 0);
  __cil_tmp3 = (char const   * __restrict  )"%d\n";
  printf(__cil_tmp3, tmp);
  tmp___0 = getClientKeyringPublicKey(bob, 0);
  __cil_tmp4 = (char const   * __restrict  )"%d\n";
  printf(__cil_tmp4, tmp___0);
  }
  return;
}
}
void rjhKeyAdd(void) 
{ 

  {
  {
  createClientKeyringEntry(rjh);
  setClientKeyringUser(rjh, 0, 1);
  setClientKeyringPublicKey(rjh, 0, 123);
  }
  return;
}
}
void rjhKeyAddChuck(void) 
{ 

  {
  {
  createClientKeyringEntry(rjh);
  setClientKeyringUser(rjh, 0, 3);
  setClientKeyringPublicKey(rjh, 0, 789);
  }
  return;
}
}
void bobKeyAddChuck(void) 
{ 

  {
  {
  createClientKeyringEntry(bob);
  setClientKeyringUser(bob, 1, 3);
  setClientKeyringPublicKey(bob, 1, 789);
  }
  return;
}
}
void chuckKeyAdd(void) 
{ 

  {
  {
  createClientKeyringEntry(chuck);
  setClientKeyringUser(chuck, 0, 1);
  setClientKeyringPublicKey(chuck, 0, 123);
  }
  return;
}
}
void chuckKeyAddRjh(void) 
{ 

  {
  {
  createClientKeyringEntry(chuck);
  setClientKeyringUser(chuck, 0, 2);
  setClientKeyringPublicKey(chuck, 0, 456);
  }
  return;
}
}
void rjhDeletePrivateKey(void) 
{ 

  {
  {
  setClientPrivateKey(rjh, 0);
  }
  return;
}
}
void bobKeyChange(void) 
{ 

  {
  {
  generateKeyPair(bob, 777);
  }
  return;
}
}
void rjhKeyChange(void) 
{ 

  {
  {
  generateKeyPair(rjh, 666);
  }
  return;
}
}
void rjhSetAutoRespond(void) 
{ 

  {
  {
  setClientAutoResponse(rjh, 1);
  }
  return;
}
}
void bobSetAddressBook(void) 
{ 

  {
  {
  setClientAddressBookSize(bob, 1);
  setClientAddressBookAlias(bob, 0, rjh);
  setClientAddressBookAddress(bob, 0, rjh);
  setClientAddressBookAddress(bob, 1, chuck);
  }
  return;
}
}
void rjhEnableForwarding(void) 
{ 

  {
  {
  setClientForwardReceiver(rjh, chuck);
  }
  return;
}
}
#pragma merger(0,"libacc.i","")
extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
                                                                      char const   *__file ,
                                                                      unsigned int __line ,
                                                                      char const   *__function ) ;
extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int  ,
                                                                           int  ) ,
                                       int val ) 
{ struct __UTAC__EXCEPTION *excep ;
  struct __UTAC__CFLOW_FUNC *cf ;
  void *tmp ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  int (**mem_15)(int  , int  ) ;
  int *mem_16 ;
  struct __UTAC__CFLOW_FUNC **mem_17 ;
  struct __UTAC__CFLOW_FUNC **mem_18 ;
  struct __UTAC__CFLOW_FUNC **mem_19 ;

  {
  {
  excep = (struct __UTAC__EXCEPTION *)exception;
  tmp = malloc(24UL);
  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
  mem_15 = (int (**)(int  , int  ))cf;
  *mem_15 = cflow_func;
  __cil_tmp7 = (unsigned long )cf;
  __cil_tmp8 = __cil_tmp7 + 8;
  mem_16 = (int *)__cil_tmp8;
  *mem_16 = val;
  __cil_tmp9 = (unsigned long )cf;
  __cil_tmp10 = __cil_tmp9 + 16;
  __cil_tmp11 = (unsigned long )excep;
  __cil_tmp12 = __cil_tmp11 + 24;
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
  *mem_17 = *mem_18;
  __cil_tmp13 = (unsigned long )excep;
  __cil_tmp14 = __cil_tmp13 + 24;
  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
  *mem_19 = cf;
  }
  return;
}
}
void __utac__exception__cf_handler_free(void *exception ) 
{ struct __UTAC__EXCEPTION *excep ;
  struct __UTAC__CFLOW_FUNC *cf ;
  struct __UTAC__CFLOW_FUNC *tmp ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  void *__cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  struct __UTAC__CFLOW_FUNC **mem_15 ;
  struct __UTAC__CFLOW_FUNC **mem_16 ;
  struct __UTAC__CFLOW_FUNC **mem_17 ;

  {
  excep = (struct __UTAC__EXCEPTION *)exception;
  __cil_tmp5 = (unsigned long )excep;
  __cil_tmp6 = __cil_tmp5 + 24;
  mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
  cf = *mem_15;
  {
  while (1) {
    while_0_continue: /* CIL Label */ ;
    {
    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
    __cil_tmp8 = (unsigned long )__cil_tmp7;
    __cil_tmp9 = (unsigned long )cf;
    if (__cil_tmp9 != __cil_tmp8) {

    } else {
      goto while_0_break;
    }
    }
    {
    tmp = cf;
    __cil_tmp10 = (unsigned long )cf;
    __cil_tmp11 = __cil_tmp10 + 16;
    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
    cf = *mem_16;
    __cil_tmp12 = (void *)tmp;
    free(__cil_tmp12);
    }
  }
  while_0_break: /* CIL Label */ ;
  }
  __cil_tmp13 = (unsigned long )excep;
  __cil_tmp14 = __cil_tmp13 + 24;
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
  return;
}
}
void __utac__exception__cf_handler_reset(void *exception ) 
{ struct __UTAC__EXCEPTION *excep ;
  struct __UTAC__CFLOW_FUNC *cf ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  int (*__cil_tmp10)(int  , int  ) ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  int __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  struct __UTAC__CFLOW_FUNC **mem_16 ;
  int (**mem_17)(int  , int  ) ;
  int *mem_18 ;
  struct __UTAC__CFLOW_FUNC **mem_19 ;

  {
  excep = (struct __UTAC__EXCEPTION *)exception;
  __cil_tmp5 = (unsigned long )excep;
  __cil_tmp6 = __cil_tmp5 + 24;
  mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
  cf = *mem_16;
  {
  while (1) {
    while_1_continue: /* CIL Label */ ;
    {
    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
    __cil_tmp8 = (unsigned long )__cil_tmp7;
    __cil_tmp9 = (unsigned long )cf;
    if (__cil_tmp9 != __cil_tmp8) {

    } else {
      goto while_1_break;
    }
    }
    {
    mem_17 = (int (**)(int  , int  ))cf;
    __cil_tmp10 = *mem_17;
    __cil_tmp11 = (unsigned long )cf;
    __cil_tmp12 = __cil_tmp11 + 8;
    mem_18 = (int *)__cil_tmp12;
    __cil_tmp13 = *mem_18;
    (*__cil_tmp10)(4, __cil_tmp13);
    __cil_tmp14 = (unsigned long )cf;
    __cil_tmp15 = __cil_tmp14 + 16;
    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
    cf = *mem_19;
    }
  }
  while_1_break: /* CIL Label */ ;
  }
  {
  __utac__exception__cf_handler_free(exception);
  }
  return;
}
}
void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
void *__utac__error_stack_mgt(void *env , int mode , int count ) 
{ void *retValue_acc ;
  struct __ACC__ERR *new ;
  void *tmp ;
  struct __ACC__ERR *temp ;
  struct __ACC__ERR *next ;
  void *excep ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  void *__cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  void *__cil_tmp17 ;
  void **mem_18 ;
  struct __ACC__ERR **mem_19 ;
  struct __ACC__ERR **mem_20 ;
  void **mem_21 ;
  struct __ACC__ERR **mem_22 ;
  void **mem_23 ;
  void **mem_24 ;

  {
  if (count == 0) {
    return (retValue_acc);
  } else {

  }
  if (mode == 0) {
    {
    tmp = malloc(16UL);
    new = (struct __ACC__ERR *)tmp;
    mem_18 = (void **)new;
    *mem_18 = env;
    __cil_tmp10 = (unsigned long )new;
    __cil_tmp11 = __cil_tmp10 + 8;
    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
    *mem_19 = head;
    head = new;
    retValue_acc = (void *)new;
    }
    return (retValue_acc);
  } else {

  }
  if (mode == 1) {
    temp = head;
    {
    while (1) {
      while_2_continue: /* CIL Label */ ;
      if (count > 1) {

      } else {
        goto while_2_break;
      }
      {
      __cil_tmp12 = (unsigned long )temp;
      __cil_tmp13 = __cil_tmp12 + 8;
      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
      next = *mem_20;
      mem_21 = (void **)temp;
      excep = *mem_21;
      __cil_tmp14 = (void *)temp;
      free(__cil_tmp14);
      __utac__exception__cf_handler_reset(excep);
      temp = next;
      count = count - 1;
      }
    }
    while_2_break: /* CIL Label */ ;
    }
    {
    __cil_tmp15 = (unsigned long )temp;
    __cil_tmp16 = __cil_tmp15 + 8;
    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
    head = *mem_22;
    mem_23 = (void **)temp;
    excep = *mem_23;
    __cil_tmp17 = (void *)temp;
    free(__cil_tmp17);
    __utac__exception__cf_handler_reset(excep);
    retValue_acc = excep;
    }
    return (retValue_acc);
  } else {

  }
  if (mode == 2) {
    if (head) {
      mem_24 = (void **)head;
      retValue_acc = *mem_24;
      return (retValue_acc);
    } else {
      retValue_acc = (void *)0;
      return (retValue_acc);
    }
  } else {

  }
  return (retValue_acc);
}
}
void *__utac__get_this_arg(int i , struct JoinPoint *this ) 
{ void *retValue_acc ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  int __cil_tmp6 ;
  int __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  void **__cil_tmp10 ;
  void **__cil_tmp11 ;
  int *mem_12 ;
  void ***mem_13 ;

  {
  if (i > 0) {
    {
    __cil_tmp4 = (unsigned long )this;
    __cil_tmp5 = __cil_tmp4 + 16;
    mem_12 = (int *)__cil_tmp5;
    __cil_tmp6 = *mem_12;
    if (i <= __cil_tmp6) {

    } else {
      {
      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                    123U, "__utac__get_this_arg");
      }
    }
    }
  } else {
    {
    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                  123U, "__utac__get_this_arg");
    }
  }
  __cil_tmp7 = i - 1;
  __cil_tmp8 = (unsigned long )this;
  __cil_tmp9 = __cil_tmp8 + 8;
  mem_13 = (void ***)__cil_tmp9;
  __cil_tmp10 = *mem_13;
  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
  retValue_acc = *__cil_tmp11;
  return (retValue_acc);
  return (retValue_acc);
}
}
char const   *__utac__get_this_argtype(int i , struct JoinPoint *this ) 
{ char const   *retValue_acc ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  int __cil_tmp6 ;
  int __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  char const   **__cil_tmp10 ;
  char const   **__cil_tmp11 ;
  int *mem_12 ;
  char const   ***mem_13 ;

  {
  if (i > 0) {
    {
    __cil_tmp4 = (unsigned long )this;
    __cil_tmp5 = __cil_tmp4 + 16;
    mem_12 = (int *)__cil_tmp5;
    __cil_tmp6 = *mem_12;
    if (i <= __cil_tmp6) {

    } else {
      {
      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                    131U, "__utac__get_this_argtype");
      }
    }
    }
  } else {
    {
    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                  131U, "__utac__get_this_argtype");
    }
  }
  __cil_tmp7 = i - 1;
  __cil_tmp8 = (unsigned long )this;
  __cil_tmp9 = __cil_tmp8 + 24;
  mem_13 = (char const   ***)__cil_tmp9;
  __cil_tmp10 = *mem_13;
  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
  retValue_acc = *__cil_tmp11;
  return (retValue_acc);
  return (retValue_acc);
}
}
#pragma merger(0,"scenario.i","")
void test(void) 
{ int op1 ;
  int op2 ;
  int op3 ;
  int op4 ;
  int op5 ;
  int op6 ;
  int op7 ;
  int op8 ;
  int op9 ;
  int op10 ;
  int op11 ;
  int splverifierCounter ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  int tmp___4 ;
  int tmp___5 ;
  int tmp___6 ;
  int tmp___7 ;
  int tmp___8 ;
  int tmp___9 ;

  {
  op1 = 0;
  op2 = 0;
  op3 = 0;
  op4 = 0;
  op5 = 0;
  op6 = 0;
  op7 = 0;
  op8 = 0;
  op9 = 0;
  op10 = 0;
  op11 = 0;
  splverifierCounter = 0;
  {
  while (1) {
    while_3_continue: /* CIL Label */ ;
    if (splverifierCounter < 4) {

    } else {
      goto while_3_break;
    }
    splverifierCounter = splverifierCounter + 1;
    if (! op1) {
      {
      tmp___9 = __VERIFIER_nondet_int();
      }
      if (tmp___9) {
        {
        bobKeyAdd();
        op1 = 1;
        }
      } else {
        goto _L___8;
      }
    } else {
      _L___8: /* CIL Label */ 
      if (! op2) {
        {
        tmp___8 = __VERIFIER_nondet_int();
        }
        if (tmp___8) {
          {
          rjhSetAutoRespond();
          op2 = 1;
          }
        } else {
          goto _L___7;
        }
      } else {
        _L___7: /* CIL Label */ 
        if (! op3) {
          {
          tmp___7 = __VERIFIER_nondet_int();
          }
          if (tmp___7) {
            {
            rjhDeletePrivateKey();
            op3 = 1;
            }
          } else {
            goto _L___6;
          }
        } else {
          _L___6: /* CIL Label */ 
          if (! op4) {
            {
            tmp___6 = __VERIFIER_nondet_int();
            }
            if (tmp___6) {
              {
              rjhKeyAdd();
              op4 = 1;
              }
            } else {
              goto _L___5;
            }
          } else {
            _L___5: /* CIL Label */ 
            if (! op5) {
              {
              tmp___5 = __VERIFIER_nondet_int();
              }
              if (tmp___5) {
                {
                chuckKeyAddRjh();
                op5 = 1;
                }
              } else {
                goto _L___4;
              }
            } else {
              _L___4: /* CIL Label */ 
              if (! op6) {
                {
                tmp___4 = __VERIFIER_nondet_int();
                }
                if (tmp___4) {
                  {
                  rjhEnableForwarding();
                  op6 = 1;
                  }
                } else {
                  goto _L___3;
                }
              } else {
                _L___3: /* CIL Label */ 
                if (! op7) {
                  {
                  tmp___3 = __VERIFIER_nondet_int();
                  }
                  if (tmp___3) {
                    {
                    rjhKeyChange();
                    op7 = 1;
                    }
                  } else {
                    goto _L___2;
                  }
                } else {
                  _L___2: /* CIL Label */ 
                  if (! op8) {
                    {
                    tmp___2 = __VERIFIER_nondet_int();
                    }
                    if (tmp___2) {
                      {
                      bobSetAddressBook();
                      op8 = 1;
                      }
                    } else {
                      goto _L___1;
                    }
                  } else {
                    _L___1: /* CIL Label */ 
                    if (! op9) {
                      {
                      tmp___1 = __VERIFIER_nondet_int();
                      }
                      if (tmp___1) {
                        {
                        chuckKeyAdd();
                        op9 = 1;
                        }
                      } else {
                        goto _L___0;
                      }
                    } else {
                      _L___0: /* CIL Label */ 
                      if (! op10) {
                        {
                        tmp___0 = __VERIFIER_nondet_int();
                        }
                        if (tmp___0) {
                          {
                          bobKeyChange();
                          op10 = 1;
                          }
                        } else {
                          goto _L;
                        }
                      } else {
                        _L: /* CIL Label */ 
                        if (! op11) {
                          {
                          tmp = __VERIFIER_nondet_int();
                          }
                          if (tmp) {
                            {
                            chuckKeyAdd();
                            op11 = 1;
                            }
                          } else {
                            goto while_3_break;
                          }
                        } else {
                          goto while_3_break;
                        }
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  while_3_break: /* CIL Label */ ;
  }
  {
  bobToRjh();
  }
  return;
}
}
#pragma merger(0,"ClientLib.i","")
int initClient(void) ;
char *getClientName(int handle ) ;
void setClientName(int handle , char *value ) ;
int getClientOutbuffer(int handle ) ;
void setClientOutbuffer(int handle , int value ) ;
int getClientAddressBookSize(int handle ) ;
int createClientAddressBookEntry(int handle ) ;
int getClientAddressBookAlias(int handle , int index ) ;
int getClientAddressBookAddress(int handle , int index ) ;
int getClientAutoResponse(int handle ) ;
int getClientPrivateKey(int handle ) ;
int getClientKeyringSize(int handle ) ;
int getClientForwardReceiver(int handle ) ;
int getClientId(int handle ) ;
int findPublicKey(int handle , int userid ) ;
int findClientAddressBookAlias(int handle , int userid ) ;
int __ste_Client_counter  =    0;
int initClient(void) 
{ int retValue_acc ;

  {
  if (__ste_Client_counter < 3) {
    __ste_Client_counter = __ste_Client_counter + 1;
    retValue_acc = __ste_Client_counter;
    return (retValue_acc);
  } else {
    retValue_acc = -1;
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
char *__ste_client_name0  =    (char *)0;
char *__ste_client_name1  =    (char *)0;
char *__ste_client_name2  =    (char *)0;
char *getClientName(int handle ) 
{ char *retValue_acc ;
  void *__cil_tmp3 ;

  {
  if (handle == 1) {
    retValue_acc = __ste_client_name0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_client_name1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_client_name2;
        return (retValue_acc);
      } else {
        __cil_tmp3 = (void *)0;
        retValue_acc = (char *)__cil_tmp3;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientName(int handle , char *value ) 
{ 

  {
  if (handle == 1) {
    __ste_client_name0 = value;
  } else {
    if (handle == 2) {
      __ste_client_name1 = value;
    } else {
      if (handle == 3) {
        __ste_client_name2 = value;
      } else {

      }
    }
  }
  return;
}
}
int __ste_client_outbuffer0  =    0;
int __ste_client_outbuffer1  =    0;
int __ste_client_outbuffer2  =    0;
int __ste_client_outbuffer3  =    0;
int getClientOutbuffer(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_client_outbuffer0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_client_outbuffer1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_client_outbuffer2;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientOutbuffer(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_client_outbuffer0 = value;
  } else {
    if (handle == 2) {
      __ste_client_outbuffer1 = value;
    } else {
      if (handle == 3) {
        __ste_client_outbuffer2 = value;
      } else {

      }
    }
  }
  return;
}
}
int __ste_ClientAddressBook_size0  =    0;
int __ste_ClientAddressBook_size1  =    0;
int __ste_ClientAddressBook_size2  =    0;
int getClientAddressBookSize(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_ClientAddressBook_size0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_ClientAddressBook_size1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_ClientAddressBook_size2;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientAddressBookSize(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_ClientAddressBook_size0 = value;
  } else {
    if (handle == 2) {
      __ste_ClientAddressBook_size1 = value;
    } else {
      if (handle == 3) {
        __ste_ClientAddressBook_size2 = value;
      } else {

      }
    }
  }
  return;
}
}
int createClientAddressBookEntry(int handle ) 
{ int retValue_acc ;
  int size ;
  int tmp ;
  int __cil_tmp5 ;

  {
  {
  tmp = getClientAddressBookSize(handle);
  size = tmp;
  }
  if (size < 3) {
    {
    __cil_tmp5 = size + 1;
    setClientAddressBookSize(handle, __cil_tmp5);
    retValue_acc = size + 1;
    }
    return (retValue_acc);
  } else {
    retValue_acc = -1;
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
int __ste_Client_AddressBook0_Alias0  =    0;
int __ste_Client_AddressBook0_Alias1  =    0;
int __ste_Client_AddressBook0_Alias2  =    0;
int __ste_Client_AddressBook1_Alias0  =    0;
int __ste_Client_AddressBook1_Alias1  =    0;
int __ste_Client_AddressBook1_Alias2  =    0;
int __ste_Client_AddressBook2_Alias0  =    0;
int __ste_Client_AddressBook2_Alias1  =    0;
int __ste_Client_AddressBook2_Alias2  =    0;
int getClientAddressBookAlias(int handle , int index ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    if (index == 0) {
      retValue_acc = __ste_Client_AddressBook0_Alias0;
      return (retValue_acc);
    } else {
      if (index == 1) {
        retValue_acc = __ste_Client_AddressBook0_Alias1;
        return (retValue_acc);
      } else {
        if (index == 2) {
          retValue_acc = __ste_Client_AddressBook0_Alias2;
          return (retValue_acc);
        } else {
          retValue_acc = 0;
          return (retValue_acc);
        }
      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        retValue_acc = __ste_Client_AddressBook1_Alias0;
        return (retValue_acc);
      } else {
        if (index == 1) {
          retValue_acc = __ste_Client_AddressBook1_Alias1;
          return (retValue_acc);
        } else {
          if (index == 2) {
            retValue_acc = __ste_Client_AddressBook1_Alias2;
            return (retValue_acc);
          } else {
            retValue_acc = 0;
            return (retValue_acc);
          }
        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          retValue_acc = __ste_Client_AddressBook2_Alias0;
          return (retValue_acc);
        } else {
          if (index == 1) {
            retValue_acc = __ste_Client_AddressBook2_Alias1;
            return (retValue_acc);
          } else {
            if (index == 2) {
              retValue_acc = __ste_Client_AddressBook2_Alias2;
              return (retValue_acc);
            } else {
              retValue_acc = 0;
              return (retValue_acc);
            }
          }
        }
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
int findClientAddressBookAlias(int handle , int userid ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    if (userid == __ste_Client_AddressBook0_Alias0) {
      retValue_acc = 0;
      return (retValue_acc);
    } else {
      if (userid == __ste_Client_AddressBook0_Alias1) {
        retValue_acc = 1;
        return (retValue_acc);
      } else {
        if (userid == __ste_Client_AddressBook0_Alias2) {
          retValue_acc = 2;
          return (retValue_acc);
        } else {
          retValue_acc = -1;
          return (retValue_acc);
        }
      }
    }
  } else {
    if (handle == 2) {
      if (userid == __ste_Client_AddressBook1_Alias0) {
        retValue_acc = 0;
        return (retValue_acc);
      } else {
        if (userid == __ste_Client_AddressBook1_Alias1) {
          retValue_acc = 1;
          return (retValue_acc);
        } else {
          if (userid == __ste_Client_AddressBook1_Alias2) {
            retValue_acc = 2;
            return (retValue_acc);
          } else {
            retValue_acc = -1;
            return (retValue_acc);
          }
        }
      }
    } else {
      if (handle == 3) {
        if (userid == __ste_Client_AddressBook2_Alias0) {
          retValue_acc = 0;
          return (retValue_acc);
        } else {
          if (userid == __ste_Client_AddressBook2_Alias1) {
            retValue_acc = 1;
            return (retValue_acc);
          } else {
            if (userid == __ste_Client_AddressBook2_Alias2) {
              retValue_acc = 2;
              return (retValue_acc);
            } else {
              retValue_acc = -1;
              return (retValue_acc);
            }
          }
        }
      } else {
        retValue_acc = -1;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientAddressBookAlias(int handle , int index , int value ) 
{ 

  {
  if (handle == 1) {
    if (index == 0) {
      __ste_Client_AddressBook0_Alias0 = value;
    } else {
      if (index == 1) {
        __ste_Client_AddressBook0_Alias1 = value;
      } else {
        if (index == 2) {
          __ste_Client_AddressBook0_Alias2 = value;
        } else {

        }
      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        __ste_Client_AddressBook1_Alias0 = value;
      } else {
        if (index == 1) {
          __ste_Client_AddressBook1_Alias1 = value;
        } else {
          if (index == 2) {
            __ste_Client_AddressBook1_Alias2 = value;
          } else {

          }
        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          __ste_Client_AddressBook2_Alias0 = value;
        } else {
          if (index == 1) {
            __ste_Client_AddressBook2_Alias1 = value;
          } else {
            if (index == 2) {
              __ste_Client_AddressBook2_Alias2 = value;
            } else {

            }
          }
        }
      } else {

      }
    }
  }
  return;
}
}
int __ste_Client_AddressBook0_Address0  =    0;
int __ste_Client_AddressBook0_Address1  =    0;
int __ste_Client_AddressBook0_Address2  =    0;
int __ste_Client_AddressBook1_Address0  =    0;
int __ste_Client_AddressBook1_Address1  =    0;
int __ste_Client_AddressBook1_Address2  =    0;
int __ste_Client_AddressBook2_Address0  =    0;
int __ste_Client_AddressBook2_Address1  =    0;
int __ste_Client_AddressBook2_Address2  =    0;
int getClientAddressBookAddress(int handle , int index ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    if (index == 0) {
      retValue_acc = __ste_Client_AddressBook0_Address0;
      return (retValue_acc);
    } else {
      if (index == 1) {
        retValue_acc = __ste_Client_AddressBook0_Address1;
        return (retValue_acc);
      } else {
        if (index == 2) {
          retValue_acc = __ste_Client_AddressBook0_Address2;
          return (retValue_acc);
        } else {
          retValue_acc = 0;
          return (retValue_acc);
        }
      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        retValue_acc = __ste_Client_AddressBook1_Address0;
        return (retValue_acc);
      } else {
        if (index == 1) {
          retValue_acc = __ste_Client_AddressBook1_Address1;
          return (retValue_acc);
        } else {
          if (index == 2) {
            retValue_acc = __ste_Client_AddressBook1_Address2;
            return (retValue_acc);
          } else {
            retValue_acc = 0;
            return (retValue_acc);
          }
        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          retValue_acc = __ste_Client_AddressBook2_Address0;
          return (retValue_acc);
        } else {
          if (index == 1) {
            retValue_acc = __ste_Client_AddressBook2_Address1;
            return (retValue_acc);
          } else {
            if (index == 2) {
              retValue_acc = __ste_Client_AddressBook2_Address2;
              return (retValue_acc);
            } else {
              retValue_acc = 0;
              return (retValue_acc);
            }
          }
        }
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientAddressBookAddress(int handle , int index , int value ) 
{ 

  {
  if (handle == 1) {
    if (index == 0) {
      __ste_Client_AddressBook0_Address0 = value;
    } else {
      if (index == 1) {
        __ste_Client_AddressBook0_Address1 = value;
      } else {
        if (index == 2) {
          __ste_Client_AddressBook0_Address2 = value;
        } else {

        }
      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        __ste_Client_AddressBook1_Address0 = value;
      } else {
        if (index == 1) {
          __ste_Client_AddressBook1_Address1 = value;
        } else {
          if (index == 2) {
            __ste_Client_AddressBook1_Address2 = value;
          } else {

          }
        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          __ste_Client_AddressBook2_Address0 = value;
        } else {
          if (index == 1) {
            __ste_Client_AddressBook2_Address1 = value;
          } else {
            if (index == 2) {
              __ste_Client_AddressBook2_Address2 = value;
            } else {

            }
          }
        }
      } else {

      }
    }
  }
  return;
}
}
int __ste_client_autoResponse0  =    0;
int __ste_client_autoResponse1  =    0;
int __ste_client_autoResponse2  =    0;
int getClientAutoResponse(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_client_autoResponse0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_client_autoResponse1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_client_autoResponse2;
        return (retValue_acc);
      } else {
        retValue_acc = -1;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientAutoResponse(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_client_autoResponse0 = value;
  } else {
    if (handle == 2) {
      __ste_client_autoResponse1 = value;
    } else {
      if (handle == 3) {
        __ste_client_autoResponse2 = value;
      } else {

      }
    }
  }
  return;
}
}
int __ste_client_privateKey0  =    0;
int __ste_client_privateKey1  =    0;
int __ste_client_privateKey2  =    0;
int getClientPrivateKey(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_client_privateKey0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_client_privateKey1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_client_privateKey2;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientPrivateKey(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_client_privateKey0 = value;
  } else {
    if (handle == 2) {
      __ste_client_privateKey1 = value;
    } else {
      if (handle == 3) {
        __ste_client_privateKey2 = value;
      } else {

      }
    }
  }
  return;
}
}
int __ste_ClientKeyring_size0  =    0;
int __ste_ClientKeyring_size1  =    0;
int __ste_ClientKeyring_size2  =    0;
int getClientKeyringSize(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_ClientKeyring_size0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_ClientKeyring_size1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_ClientKeyring_size2;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientKeyringSize(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_ClientKeyring_size0 = value;
  } else {
    if (handle == 2) {
      __ste_ClientKeyring_size1 = value;
    } else {
      if (handle == 3) {
        __ste_ClientKeyring_size2 = value;
      } else {

      }
    }
  }
  return;
}
}
int createClientKeyringEntry(int handle ) 
{ int retValue_acc ;
  int size ;
  int tmp ;
  int __cil_tmp5 ;

  {
  {
  tmp = getClientKeyringSize(handle);
  size = tmp;
  }
  if (size < 2) {
    {
    __cil_tmp5 = size + 1;
    setClientKeyringSize(handle, __cil_tmp5);
    retValue_acc = size + 1;
    }
    return (retValue_acc);
  } else {
    retValue_acc = -1;
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
int __ste_Client_Keyring0_User0  =    0;
int __ste_Client_Keyring0_User1  =    0;
int __ste_Client_Keyring0_User2  =    0;
int __ste_Client_Keyring1_User0  =    0;
int __ste_Client_Keyring1_User1  =    0;
int __ste_Client_Keyring1_User2  =    0;
int __ste_Client_Keyring2_User0  =    0;
int __ste_Client_Keyring2_User1  =    0;
int __ste_Client_Keyring2_User2  =    0;
int getClientKeyringUser(int handle , int index ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    if (index == 0) {
      retValue_acc = __ste_Client_Keyring0_User0;
      return (retValue_acc);
    } else {
      if (index == 1) {
        retValue_acc = __ste_Client_Keyring0_User1;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        retValue_acc = __ste_Client_Keyring1_User0;
        return (retValue_acc);
      } else {
        if (index == 1) {
          retValue_acc = __ste_Client_Keyring1_User1;
          return (retValue_acc);
        } else {
          retValue_acc = 0;
          return (retValue_acc);
        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          retValue_acc = __ste_Client_Keyring2_User0;
          return (retValue_acc);
        } else {
          if (index == 1) {
            retValue_acc = __ste_Client_Keyring2_User1;
            return (retValue_acc);
          } else {
            retValue_acc = 0;
            return (retValue_acc);
          }
        }
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientKeyringUser(int handle , int index , int value ) 
{ 

  {
  if (handle == 1) {
    if (index == 0) {
      __ste_Client_Keyring0_User0 = value;
    } else {
      if (index == 1) {
        __ste_Client_Keyring0_User1 = value;
      } else {

      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        __ste_Client_Keyring1_User0 = value;
      } else {
        if (index == 1) {
          __ste_Client_Keyring1_User1 = value;
        } else {

        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          __ste_Client_Keyring2_User0 = value;
        } else {
          if (index == 1) {
            __ste_Client_Keyring2_User1 = value;
          } else {

          }
        }
      } else {

      }
    }
  }
  return;
}
}
int __ste_Client_Keyring0_PublicKey0  =    0;
int __ste_Client_Keyring0_PublicKey1  =    0;
int __ste_Client_Keyring0_PublicKey2  =    0;
int __ste_Client_Keyring1_PublicKey0  =    0;
int __ste_Client_Keyring1_PublicKey1  =    0;
int __ste_Client_Keyring1_PublicKey2  =    0;
int __ste_Client_Keyring2_PublicKey0  =    0;
int __ste_Client_Keyring2_PublicKey1  =    0;
int __ste_Client_Keyring2_PublicKey2  =    0;
int getClientKeyringPublicKey(int handle , int index ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    if (index == 0) {
      retValue_acc = __ste_Client_Keyring0_PublicKey0;
      return (retValue_acc);
    } else {
      if (index == 1) {
        retValue_acc = __ste_Client_Keyring0_PublicKey1;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        retValue_acc = __ste_Client_Keyring1_PublicKey0;
        return (retValue_acc);
      } else {
        if (index == 1) {
          retValue_acc = __ste_Client_Keyring1_PublicKey1;
          return (retValue_acc);
        } else {
          retValue_acc = 0;
          return (retValue_acc);
        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          retValue_acc = __ste_Client_Keyring2_PublicKey0;
          return (retValue_acc);
        } else {
          if (index == 1) {
            retValue_acc = __ste_Client_Keyring2_PublicKey1;
            return (retValue_acc);
          } else {
            retValue_acc = 0;
            return (retValue_acc);
          }
        }
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
int findPublicKey(int handle , int userid ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    if (userid == __ste_Client_Keyring0_User0) {
      retValue_acc = __ste_Client_Keyring0_PublicKey0;
      return (retValue_acc);
    } else {
      if (userid == __ste_Client_Keyring0_User1) {
        retValue_acc = __ste_Client_Keyring0_PublicKey1;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  } else {
    if (handle == 2) {
      if (userid == __ste_Client_Keyring1_User0) {
        retValue_acc = __ste_Client_Keyring1_PublicKey0;
        return (retValue_acc);
      } else {
        if (userid == __ste_Client_Keyring1_User1) {
          retValue_acc = __ste_Client_Keyring1_PublicKey1;
          return (retValue_acc);
        } else {
          retValue_acc = 0;
          return (retValue_acc);
        }
      }
    } else {
      if (handle == 3) {
        if (userid == __ste_Client_Keyring2_User0) {
          retValue_acc = __ste_Client_Keyring2_PublicKey0;
          return (retValue_acc);
        } else {
          if (userid == __ste_Client_Keyring2_User1) {
            retValue_acc = __ste_Client_Keyring2_PublicKey1;
            return (retValue_acc);
          } else {
            retValue_acc = 0;
            return (retValue_acc);
          }
        }
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientKeyringPublicKey(int handle , int index , int value ) 
{ 

  {
  if (handle == 1) {
    if (index == 0) {
      __ste_Client_Keyring0_PublicKey0 = value;
    } else {
      if (index == 1) {
        __ste_Client_Keyring0_PublicKey1 = value;
      } else {

      }
    }
  } else {
    if (handle == 2) {
      if (index == 0) {
        __ste_Client_Keyring1_PublicKey0 = value;
      } else {
        if (index == 1) {
          __ste_Client_Keyring1_PublicKey1 = value;
        } else {

        }
      }
    } else {
      if (handle == 3) {
        if (index == 0) {
          __ste_Client_Keyring2_PublicKey0 = value;
        } else {
          if (index == 1) {
            __ste_Client_Keyring2_PublicKey1 = value;
          } else {

          }
        }
      } else {

      }
    }
  }
  return;
}
}
int __ste_client_forwardReceiver0  =    0;
int __ste_client_forwardReceiver1  =    0;
int __ste_client_forwardReceiver2  =    0;
int __ste_client_forwardReceiver3  =    0;
int getClientForwardReceiver(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_client_forwardReceiver0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_client_forwardReceiver1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_client_forwardReceiver2;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientForwardReceiver(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_client_forwardReceiver0 = value;
  } else {
    if (handle == 2) {
      __ste_client_forwardReceiver1 = value;
    } else {
      if (handle == 3) {
        __ste_client_forwardReceiver2 = value;
      } else {

      }
    }
  }
  return;
}
}
int __ste_client_idCounter0  =    0;
int __ste_client_idCounter1  =    0;
int __ste_client_idCounter2  =    0;
int getClientId(int handle ) 
{ int retValue_acc ;

  {
  if (handle == 1) {
    retValue_acc = __ste_client_idCounter0;
    return (retValue_acc);
  } else {
    if (handle == 2) {
      retValue_acc = __ste_client_idCounter1;
      return (retValue_acc);
    } else {
      if (handle == 3) {
        retValue_acc = __ste_client_idCounter2;
        return (retValue_acc);
      } else {
        retValue_acc = 0;
        return (retValue_acc);
      }
    }
  }
  return (retValue_acc);
}
}
void setClientId(int handle , int value ) 
{ 

  {
  if (handle == 1) {
    __ste_client_idCounter0 = value;
  } else {
    if (handle == 2) {
      __ste_client_idCounter1 = value;
    } else {
      if (handle == 3) {
        __ste_client_idCounter2 = value;
      } else {

      }
    }
  }
  return;
}
}
#pragma merger(0,"Client.i","")
void queue(int client , int msg ) ;
void mail(int client , int msg ) ;
void deliver(int client , int msg ) ;
void incoming(int client , int msg ) ;
int createClient(char *name ) ;
int isKeyPairValid(int publicKey , int privateKey ) ;
void autoRespond(int client , int msg ) ;
void sendToAddressBook(int client , int msg ) ;
void forward(int client , int msg ) ;
int queue_empty  =    1;
int queued_message  ;
int queued_client  ;
void mail(int client , int msg ) 
{ int tmp ;

  {
  {
  puts("mail sent");
  tmp = getEmailTo(msg);
  incoming(tmp, msg);
  }
  return;
}
}
void outgoing__wrappee__Keys(int client , int msg ) 
{ int tmp ;

  {
  {
  tmp = getClientId(client);
  setEmailFrom(msg, tmp);
  mail(client, msg);
  }
  return;
}
}
void outgoing__wrappee__AutoResponder(int client , int msg ) 
{ int receiver ;
  int tmp ;
  int pubkey ;
  int tmp___0 ;

  {
  {
  tmp = getEmailTo(msg);
  receiver = tmp;
  tmp___0 = findPublicKey(client, receiver);
  pubkey = tmp___0;
  }
  if (pubkey) {
    {
    setEmailEncryptionKey(msg, pubkey);
    setEmailIsEncrypted(msg, 1);
    }
  } else {

  }
  {
  outgoing__wrappee__Keys(client, msg);
  }
  return;
}
}
void outgoing(int client , int msg ) 
{ int size ;
  int tmp ;
  int receiver ;
  int tmp___0 ;
  int second ;
  int tmp___1 ;
  int tmp___2 ;

  {
  {
  tmp = getClientAddressBookSize(client);
  size = tmp;
  }
  if (size) {
    {
    sendToAddressBook(client, msg);
    puts("sending to alias in address book\n");
    tmp___0 = getEmailTo(msg);
    receiver = tmp___0;
    puts("sending to second receipient\n");
    tmp___1 = getClientAddressBookAddress(client, 1);
    second = tmp___1;
    setEmailTo(msg, second);
    outgoing__wrappee__AutoResponder(client, msg);
    tmp___2 = getClientAddressBookAddress(client, 0);
    setEmailTo(msg, tmp___2);
    outgoing__wrappee__AutoResponder(client, msg);
    }
  } else {
    {
    outgoing__wrappee__AutoResponder(client, msg);
    }
  }
  return;
}
}
void deliver(int client , int msg ) 
{ 

  {
  {
  puts("mail delivered\n");
  }
  return;
}
}
void incoming__wrappee__Encrypt(int client , int msg ) 
{ 

  {
  {
  deliver(client, msg);
  }
  return;
}
}
void incoming__wrappee__AddressBook(int client , int msg ) 
{ int tmp ;

  {
  {
  incoming__wrappee__Encrypt(client, msg);
  tmp = getClientAutoResponse(client);
  }
  if (tmp) {
    {
    autoRespond(client, msg);
    }
  } else {

  }
  return;
}
}
void incoming__wrappee__Forward(int client , int msg ) 
{ int fwreceiver ;
  int tmp ;

  {
  {
  incoming__wrappee__AddressBook(client, msg);
  tmp = getClientForwardReceiver(client);
  fwreceiver = tmp;
  }
  if (fwreceiver) {
    {
    setEmailTo(msg, fwreceiver);
    forward(client, msg);
    }
  } else {

  }
  return;
}
}
void incoming(int client , int msg ) 
{ int privkey ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;

  {
  {
  tmp = getClientPrivateKey(client);
  privkey = tmp;
  }
  if (privkey) {
    {
    tmp___0 = isEncrypted(msg);
    }
    if (tmp___0) {
      {
      tmp___1 = getEmailEncryptionKey(msg);
      tmp___2 = isKeyPairValid(tmp___1, privkey);
      }
      if (tmp___2) {
        {
        setEmailIsEncrypted(msg, 0);
        setEmailEncryptionKey(msg, 0);
        }
      } else {

      }
    } else {

    }
  } else {

  }
  {
  incoming__wrappee__Forward(client, msg);
  }
  return;
}
}
int createClient(char *name ) 
{ int retValue_acc ;
  int client ;
  int tmp ;

  {
  {
  tmp = initClient();
  client = tmp;
  retValue_acc = client;
  }
  return (retValue_acc);
  return (retValue_acc);
}
}
void sendEmail(int sender , int receiver ) 
{ int email ;
  int tmp ;

  {
  {
  tmp = createEmail(0, receiver);
  email = tmp;
  outgoing(sender, email);
  }
  return;
}
}
void queue(int client , int msg ) 
{ 

  {
  queue_empty = 0;
  queued_message = msg;
  queued_client = client;
  return;
}
}
int is_queue_empty(void) 
{ int retValue_acc ;

  {
  retValue_acc = queue_empty;
  return (retValue_acc);
  return (retValue_acc);
}
}
int get_queued_client(void) 
{ int retValue_acc ;

  {
  retValue_acc = queued_client;
  return (retValue_acc);
  return (retValue_acc);
}
}
int get_queued_email(void) 
{ int retValue_acc ;

  {
  retValue_acc = queued_message;
  return (retValue_acc);
  return (retValue_acc);
}
}
int isKeyPairValid(int publicKey , int privateKey ) 
{ int retValue_acc ;
  char const   * __restrict  __cil_tmp4 ;

  {
  {
  __cil_tmp4 = (char const   * __restrict  )"keypair valid %d %d";
  printf(__cil_tmp4, publicKey, privateKey);
  }
  if (! publicKey) {
    retValue_acc = 0;
    return (retValue_acc);
  } else {
    if (! privateKey) {
      retValue_acc = 0;
      return (retValue_acc);
    } else {

    }
  }
  retValue_acc = privateKey == publicKey;
  return (retValue_acc);
  return (retValue_acc);
}
}
void generateKeyPair(int client , int seed ) 
{ 

  {
  {
  setClientPrivateKey(client, seed);
  }
  return;
}
}
void autoRespond(int client , int msg ) 
{ int __utac__ad__arg1 ;
  int __utac__ad__arg2 ;
  int sender ;
  int tmp ;

  {
  {
  __utac__ad__arg1 = client;
  __utac__ad__arg2 = msg;
  __utac_acc__DecryptAutoResponder_spec__1(__utac__ad__arg1, __utac__ad__arg2);
  puts("sending autoresponse\n");
  tmp = getEmailFrom(msg);
  sender = tmp;
  setEmailTo(msg, sender);
  queue(client, msg);
  }
  return;
}
}
void sendToAddressBook(int client , int msg ) 
{ 

  {
  return;
}
}
void forward(int client , int msg ) 
{ 

  {
  {
  puts("Forwarding message.\n");
  printMail(msg);
  queue(client, msg);
  }
  return;
}
}
#pragma merger(0,"wsllib_check.i","")
void __automaton_fail(void) 
{ 

  {
  ERROR: __VERIFIER_error();
  return;
}
}
#pragma merger(0,"Util.i","")
int prompt(char *msg ) ;
int prompt(char *msg ) 
{ int retValue_acc ;
  int retval ;
  char const   * __restrict  __cil_tmp4 ;

  {
  {
  __cil_tmp4 = (char const   * __restrict  )"%s\n";
  printf(__cil_tmp4, msg);
  retValue_acc = retval;
  }
  return (retValue_acc);
  return (retValue_acc);
}
}