ClabureDB: Classified Bug-Reports Database

   extern int __VERIFIER_nondet_int(void);
   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 2 "libacc.c"
   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 ;
  };
  #line 18 "libacc.c"
  struct __UTAC__CFLOW_FUNC {
     int (*func)(int  , int  ) ;
     int val ;
     struct __UTAC__CFLOW_FUNC *next ;
  };
  #line 18 "libacc.c"
  struct __UTAC__EXCEPTION {
     void *jumpbuf ;
     unsigned long long prtValue ;
     int pops ;
     struct __UTAC__CFLOW_FUNC *cflowfuncs ;
  };
  #line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
  typedef unsigned long size_t;
  #line 76 "libacc.c"
  struct __ACC__ERR {
     void *v ;
     struct __ACC__ERR *next ;
  };
  #line 1 "ClientLib.o"
  #pragma merger(0,"ClientLib.i","")
  #line 4 "ClientLib.h"
  int initClient(void) ;
  #line 6
  char *getClientName(int handle ) ;
  #line 8
  void setClientName(int handle , char *value ) ;
  #line 10
  int getClientOutbuffer(int handle ) ;
  #line 12
  void setClientOutbuffer(int handle , int value ) ;
  #line 14
  int getClientAddressBookSize(int handle ) ;
  #line 16
  void setClientAddressBookSize(int handle , int value ) ;
  #line 18
  int createClientAddressBookEntry(int handle ) ;
  #line 20
  int getClientAddressBookAlias(int handle , int index ) ;
  #line 22
  void setClientAddressBookAlias(int handle , int index , int value ) ;
  #line 24
  int getClientAddressBookAddress(int handle , int index ) ;
  #line 26
  void setClientAddressBookAddress(int handle , int index , int value ) ;
  #line 29
  int getClientAutoResponse(int handle ) ;
  #line 31
  void setClientAutoResponse(int handle , int value ) ;
  #line 33
  int getClientPrivateKey(int handle ) ;
  #line 35
  void setClientPrivateKey(int handle , int value ) ;
  #line 37
  int getClientKeyringSize(int handle ) ;
  #line 39
  int createClientKeyringEntry(int handle ) ;
  #line 41
  int getClientKeyringUser(int handle , int index ) ;
  #line 43
  void setClientKeyringUser(int handle , int index , int value ) ;
  #line 45
  int getClientKeyringPublicKey(int handle , int index ) ;
  #line 47
  void setClientKeyringPublicKey(int handle , int index , int value ) ;
  #line 49
  int getClientForwardReceiver(int handle ) ;
  #line 51
  void setClientForwardReceiver(int handle , int value ) ;
  #line 53
  int getClientId(int handle ) ;
  #line 55
  void setClientId(int handle , int value ) ;
  #line 57
  int findPublicKey(int handle , int userid ) ;
  #line 59
  int findClientAddressBookAlias(int handle , int userid ) ;
  #line 5 "ClientLib.c"
 int __ste_Client_counter  =    0;
 #line 7 "ClientLib.c"
 int initClient(void) 
 { int retValue_acc ;
 
   {
 #line 12 "ClientLib.c"
   if (__ste_Client_counter < 3) {
 #line 684
     __ste_Client_counter = __ste_Client_counter + 1;
 #line 684
     retValue_acc = __ste_Client_counter;
 #line 686
     return (retValue_acc);
   } else {
 #line 692 "ClientLib.c"
     retValue_acc = -1;
 #line 694
     return (retValue_acc);
   }
 #line 701 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 15 "ClientLib.c"
 char *__ste_client_name0  =    (char *)0;
 #line 17 "ClientLib.c"
 char *__ste_client_name1  =    (char *)0;
 #line 19 "ClientLib.c"
 char *__ste_client_name2  =    (char *)0;
 #line 22 "ClientLib.c"
 char *getClientName(int handle ) 
 { char *retValue_acc ;
   void *__cil_tmp3 ;
 
   {
 #line 31 "ClientLib.c"
   if (handle == 1) {
 #line 732
     retValue_acc = __ste_client_name0;
 #line 734
     return (retValue_acc);
   } else {
 #line 736
     if (handle == 2) {
 #line 741
       retValue_acc = __ste_client_name1;
 #line 743
       return (retValue_acc);
     } else {
 #line 745
       if (handle == 3) {
 #line 750
         retValue_acc = __ste_client_name2;
 #line 752
         return (retValue_acc);
       } else {
 #line 758 "ClientLib.c"
         __cil_tmp3 = (void *)0;
 #line 758
         retValue_acc = (char *)__cil_tmp3;
 #line 760
         return (retValue_acc);
       }
     }
   }
 #line 767 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 34 "ClientLib.c"
 void setClientName(int handle , char *value ) 
 { 
 
   {
 #line 42
   if (handle == 1) {
 #line 36
     __ste_client_name0 = value;
   } else {
 #line 37
     if (handle == 2) {
 #line 38
       __ste_client_name1 = value;
     } else {
 #line 39
       if (handle == 3) {
 #line 40
         __ste_client_name2 = value;
       } else {
 
       }
     }
   }
 #line 802 "ClientLib.c"
   return;
 }
 }
 #line 44 "ClientLib.c"
 int __ste_client_outbuffer0  =    0;
 #line 46 "ClientLib.c"
 int __ste_client_outbuffer1  =    0;
 #line 48 "ClientLib.c"
 int __ste_client_outbuffer2  =    0;
 #line 50 "ClientLib.c"
 int __ste_client_outbuffer3  =    0;
 #line 53 "ClientLib.c"
 int getClientOutbuffer(int handle ) 
 { int retValue_acc ;
 
   {
 #line 62 "ClientLib.c"
   if (handle == 1) {
 #line 831
     retValue_acc = __ste_client_outbuffer0;
 #line 833
     return (retValue_acc);
   } else {
 #line 835
     if (handle == 2) {
 #line 840
       retValue_acc = __ste_client_outbuffer1;
 #line 842
       return (retValue_acc);
     } else {
 #line 844
       if (handle == 3) {
 #line 849
         retValue_acc = __ste_client_outbuffer2;
 #line 851
         return (retValue_acc);
       } else {
 #line 857 "ClientLib.c"
         retValue_acc = 0;
 #line 859
         return (retValue_acc);
       }
     }
   }
 #line 866 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 65 "ClientLib.c"
 void setClientOutbuffer(int handle , int value ) 
 { 
 
   {
 #line 73
   if (handle == 1) {
 #line 67
     __ste_client_outbuffer0 = value;
   } else {
 #line 68
     if (handle == 2) {
 #line 69
       __ste_client_outbuffer1 = value;
     } else {
 #line 70
       if (handle == 3) {
 #line 71
         __ste_client_outbuffer2 = value;
       } else {
 
       }
     }
   }
 #line 901 "ClientLib.c"
   return;
 }
 }
 #line 77 "ClientLib.c"
 int __ste_ClientAddressBook_size0  =    0;
 #line 79 "ClientLib.c"
 int __ste_ClientAddressBook_size1  =    0;
 #line 81 "ClientLib.c"
 int __ste_ClientAddressBook_size2  =    0;
 #line 84 "ClientLib.c"
 int getClientAddressBookSize(int handle ) 
 { int retValue_acc ;
 
   {
 #line 93 "ClientLib.c"
   if (handle == 1) {
 #line 928
     retValue_acc = __ste_ClientAddressBook_size0;
 #line 930
     return (retValue_acc);
   } else {
 #line 932
     if (handle == 2) {
 #line 937
       retValue_acc = __ste_ClientAddressBook_size1;
 #line 939
       return (retValue_acc);
     } else {
 #line 941
       if (handle == 3) {
 #line 946
         retValue_acc = __ste_ClientAddressBook_size2;
 #line 948
         return (retValue_acc);
       } else {
 #line 954 "ClientLib.c"
         retValue_acc = 0;
 #line 956
         return (retValue_acc);
       }
     }
   }
 #line 963 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 96 "ClientLib.c"
 void setClientAddressBookSize(int handle , int value ) 
 { 
 
   {
 #line 104
   if (handle == 1) {
 #line 98
     __ste_ClientAddressBook_size0 = value;
   } else {
 #line 99
     if (handle == 2) {
 #line 100
       __ste_ClientAddressBook_size1 = value;
     } else {
 #line 101
       if (handle == 3) {
 #line 102
         __ste_ClientAddressBook_size2 = value;
       } else {
 
       }
     }
   }
 #line 998 "ClientLib.c"
   return;
 }
 }
 #line 106 "ClientLib.c"
 int createClientAddressBookEntry(int handle ) 
 { int retValue_acc ;
   int size ;
   int tmp ;
   int __cil_tmp5 ;
 
   {
   {
 #line 107
   tmp = getClientAddressBookSize(handle);
 #line 107
   size = tmp;
   }
 #line 108 "ClientLib.c"
   if (size < 3) {
     {
 #line 109 "ClientLib.c"
     __cil_tmp5 = size + 1;
 #line 109
     setClientAddressBookSize(handle, __cil_tmp5);
 #line 1025 "ClientLib.c"
     retValue_acc = size + 1;
     }
 #line 1027
     return (retValue_acc);
   } else {
 #line 1031 "ClientLib.c"
     retValue_acc = -1;
 #line 1033
     return (retValue_acc);
   }
 #line 1040 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 115 "ClientLib.c"
 int __ste_Client_AddressBook0_Alias0  =    0;
 #line 117 "ClientLib.c"
 int __ste_Client_AddressBook0_Alias1  =    0;
 #line 119 "ClientLib.c"
 int __ste_Client_AddressBook0_Alias2  =    0;
 #line 121 "ClientLib.c"
 int __ste_Client_AddressBook1_Alias0  =    0;
 #line 123 "ClientLib.c"
 int __ste_Client_AddressBook1_Alias1  =    0;
 #line 125 "ClientLib.c"
 int __ste_Client_AddressBook1_Alias2  =    0;
 #line 127 "ClientLib.c"
 int __ste_Client_AddressBook2_Alias0  =    0;
 #line 129 "ClientLib.c"
 int __ste_Client_AddressBook2_Alias1  =    0;
 #line 131 "ClientLib.c"
 int __ste_Client_AddressBook2_Alias2  =    0;
 #line 134 "ClientLib.c"
 int getClientAddressBookAlias(int handle , int index ) 
 { int retValue_acc ;
 
   {
 #line 167
   if (handle == 1) {
 #line 144 "ClientLib.c"
     if (index == 0) {
 #line 1086
       retValue_acc = __ste_Client_AddressBook0_Alias0;
 #line 1088
       return (retValue_acc);
     } else {
 #line 1090
       if (index == 1) {
 #line 1095
         retValue_acc = __ste_Client_AddressBook0_Alias1;
 #line 1097
         return (retValue_acc);
       } else {
 #line 1099
         if (index == 2) {
 #line 1104
           retValue_acc = __ste_Client_AddressBook0_Alias2;
 #line 1106
           return (retValue_acc);
         } else {
 #line 1112
           retValue_acc = 0;
 #line 1114
           return (retValue_acc);
         }
       }
     }
   } else {
 #line 1116 "ClientLib.c"
     if (handle == 2) {
 #line 154 "ClientLib.c"
       if (index == 0) {
 #line 1124
         retValue_acc = __ste_Client_AddressBook1_Alias0;
 #line 1126
         return (retValue_acc);
       } else {
 #line 1128
         if (index == 1) {
 #line 1133
           retValue_acc = __ste_Client_AddressBook1_Alias1;
 #line 1135
           return (retValue_acc);
         } else {
 #line 1137
           if (index == 2) {
 #line 1142
             retValue_acc = __ste_Client_AddressBook1_Alias2;
 #line 1144
             return (retValue_acc);
           } else {
 #line 1150
             retValue_acc = 0;
 #line 1152
             return (retValue_acc);
           }
         }
       }
     } else {
 #line 1154 "ClientLib.c"
       if (handle == 3) {
 #line 164 "ClientLib.c"
         if (index == 0) {
 #line 1162
           retValue_acc = __ste_Client_AddressBook2_Alias0;
 #line 1164
           return (retValue_acc);
         } else {
 #line 1166
           if (index == 1) {
 #line 1171
             retValue_acc = __ste_Client_AddressBook2_Alias1;
 #line 1173
             return (retValue_acc);
           } else {
 #line 1175
             if (index == 2) {
 #line 1180
               retValue_acc = __ste_Client_AddressBook2_Alias2;
 #line 1182
               return (retValue_acc);
             } else {
 #line 1188
               retValue_acc = 0;
 #line 1190
               return (retValue_acc);
             }
           }
         }
       } else {
 #line 1196 "ClientLib.c"
         retValue_acc = 0;
 #line 1198
         return (retValue_acc);
       }
     }
   }
 #line 1205 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 171 "ClientLib.c"
 int findClientAddressBookAlias(int handle , int userid ) 
 { int retValue_acc ;
 
   {
 #line 204
   if (handle == 1) {
 #line 181 "ClientLib.c"
     if (userid == __ste_Client_AddressBook0_Alias0) {
 #line 1233
       retValue_acc = 0;
 #line 1235
       return (retValue_acc);
     } else {
 #line 1237
       if (userid == __ste_Client_AddressBook0_Alias1) {
 #line 1242
         retValue_acc = 1;
 #line 1244
         return (retValue_acc);
       } else {
 #line 1246
         if (userid == __ste_Client_AddressBook0_Alias2) {
 #line 1251
           retValue_acc = 2;
 #line 1253
           return (retValue_acc);
         } else {
 #line 1259
           retValue_acc = -1;
 #line 1261
           return (retValue_acc);
         }
       }
     }
   } else {
 #line 1263 "ClientLib.c"
     if (handle == 2) {
 #line 191 "ClientLib.c"
       if (userid == __ste_Client_AddressBook1_Alias0) {
 #line 1271
         retValue_acc = 0;
 #line 1273
         return (retValue_acc);
       } else {
 #line 1275
         if (userid == __ste_Client_AddressBook1_Alias1) {
 #line 1280
           retValue_acc = 1;
 #line 1282
           return (retValue_acc);
         } else {
 #line 1284
           if (userid == __ste_Client_AddressBook1_Alias2) {
 #line 1289
             retValue_acc = 2;
 #line 1291
             return (retValue_acc);
           } else {
 #line 1297
             retValue_acc = -1;
 #line 1299
             return (retValue_acc);
           }
         }
       }
     } else {
 #line 1301 "ClientLib.c"
       if (handle == 3) {
 #line 201 "ClientLib.c"
         if (userid == __ste_Client_AddressBook2_Alias0) {
 #line 1309
           retValue_acc = 0;
 #line 1311
           return (retValue_acc);
         } else {
 #line 1313
           if (userid == __ste_Client_AddressBook2_Alias1) {
 #line 1318
             retValue_acc = 1;
 #line 1320
             return (retValue_acc);
           } else {
 #line 1322
             if (userid == __ste_Client_AddressBook2_Alias2) {
 #line 1327
               retValue_acc = 2;
 #line 1329
               return (retValue_acc);
             } else {
 #line 1335
               retValue_acc = -1;
 #line 1337
               return (retValue_acc);
             }
           }
         }
       } else {
 #line 1343 "ClientLib.c"
         retValue_acc = -1;
 #line 1345
         return (retValue_acc);
       }
     }
   }
 #line 1352 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 208 "ClientLib.c"
 void setClientAddressBookAlias(int handle , int index , int value ) 
 { 
 
   {
 #line 234
   if (handle == 1) {
 #line 217
     if (index == 0) {
 #line 211
       __ste_Client_AddressBook0_Alias0 = value;
     } else {
 #line 212
       if (index == 1) {
 #line 213
         __ste_Client_AddressBook0_Alias1 = value;
       } else {
 #line 214
         if (index == 2) {
 #line 215
           __ste_Client_AddressBook0_Alias2 = value;
         } else {
 
         }
       }
     }
   } else {
 #line 216
     if (handle == 2) {
 #line 225
       if (index == 0) {
 #line 219
         __ste_Client_AddressBook1_Alias0 = value;
       } else {
 #line 220
         if (index == 1) {
 #line 221
           __ste_Client_AddressBook1_Alias1 = value;
         } else {
 #line 222
           if (index == 2) {
 #line 223
             __ste_Client_AddressBook1_Alias2 = value;
           } else {
 
           }
         }
       }
     } else {
 #line 224
       if (handle == 3) {
 #line 233
         if (index == 0) {
 #line 227
           __ste_Client_AddressBook2_Alias0 = value;
         } else {
 #line 228
           if (index == 1) {
 #line 229
             __ste_Client_AddressBook2_Alias1 = value;
           } else {
 #line 230
             if (index == 2) {
 #line 231
               __ste_Client_AddressBook2_Alias2 = value;
             } else {
 
             }
           }
         }
       } else {
 
       }
     }
   }
 #line 1420 "ClientLib.c"
   return;
 }
 }
 #line 236 "ClientLib.c"
 int __ste_Client_AddressBook0_Address0  =    0;
 #line 238 "ClientLib.c"
 int __ste_Client_AddressBook0_Address1  =    0;
 #line 240 "ClientLib.c"
 int __ste_Client_AddressBook0_Address2  =    0;
 #line 242 "ClientLib.c"
 int __ste_Client_AddressBook1_Address0  =    0;
 #line 244 "ClientLib.c"
 int __ste_Client_AddressBook1_Address1  =    0;
 #line 246 "ClientLib.c"
 int __ste_Client_AddressBook1_Address2  =    0;
 #line 248 "ClientLib.c"
 int __ste_Client_AddressBook2_Address0  =    0;
 #line 250 "ClientLib.c"
 int __ste_Client_AddressBook2_Address1  =    0;
 #line 252 "ClientLib.c"
 int __ste_Client_AddressBook2_Address2  =    0;
 #line 255 "ClientLib.c"
 int getClientAddressBookAddress(int handle , int index ) 
 { int retValue_acc ;
 
   {
 #line 288
   if (handle == 1) {
 #line 265 "ClientLib.c"
     if (index == 0) {
 #line 1462
       retValue_acc = __ste_Client_AddressBook0_Address0;
 #line 1464
       return (retValue_acc);
     } else {
 #line 1466
       if (index == 1) {
 #line 1471
         retValue_acc = __ste_Client_AddressBook0_Address1;
 #line 1473
         return (retValue_acc);
       } else {
 #line 1475
         if (index == 2) {
 #line 1480
           retValue_acc = __ste_Client_AddressBook0_Address2;
 #line 1482
           return (retValue_acc);
         } else {
 #line 1488
           retValue_acc = 0;
 #line 1490
           return (retValue_acc);
         }
       }
     }
   } else {
 #line 1492 "ClientLib.c"
     if (handle == 2) {
 #line 275 "ClientLib.c"
       if (index == 0) {
 #line 1500
         retValue_acc = __ste_Client_AddressBook1_Address0;
 #line 1502
         return (retValue_acc);
       } else {
 #line 1504
         if (index == 1) {
 #line 1509
           retValue_acc = __ste_Client_AddressBook1_Address1;
 #line 1511
           return (retValue_acc);
         } else {
 #line 1513
           if (index == 2) {
 #line 1518
             retValue_acc = __ste_Client_AddressBook1_Address2;
 #line 1520
             return (retValue_acc);
           } else {
 #line 1526
             retValue_acc = 0;
 #line 1528
             return (retValue_acc);
           }
         }
       }
     } else {
 #line 1530 "ClientLib.c"
       if (handle == 3) {
 #line 285 "ClientLib.c"
         if (index == 0) {
 #line 1538
           retValue_acc = __ste_Client_AddressBook2_Address0;
 #line 1540
           return (retValue_acc);
         } else {
 #line 1542
           if (index == 1) {
 #line 1547
             retValue_acc = __ste_Client_AddressBook2_Address1;
 #line 1549
             return (retValue_acc);
           } else {
 #line 1551
             if (index == 2) {
 #line 1556
               retValue_acc = __ste_Client_AddressBook2_Address2;
 #line 1558
               return (retValue_acc);
             } else {
 #line 1564
               retValue_acc = 0;
 #line 1566
               return (retValue_acc);
             }
           }
         }
       } else {
 #line 1572 "ClientLib.c"
         retValue_acc = 0;
 #line 1574
         return (retValue_acc);
       }
     }
   }
 #line 1581 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 291 "ClientLib.c"
 void setClientAddressBookAddress(int handle , int index , int value ) 
 { 
 
   {
 #line 317
   if (handle == 1) {
 #line 300
     if (index == 0) {
 #line 294
       __ste_Client_AddressBook0_Address0 = value;
     } else {
 #line 295
       if (index == 1) {
 #line 296
         __ste_Client_AddressBook0_Address1 = value;
       } else {
 #line 297
         if (index == 2) {
 #line 298
           __ste_Client_AddressBook0_Address2 = value;
         } else {
 
         }
       }
     }
   } else {
 #line 299
     if (handle == 2) {
 #line 308
       if (index == 0) {
 #line 302
         __ste_Client_AddressBook1_Address0 = value;
       } else {
 #line 303
         if (index == 1) {
 #line 304
           __ste_Client_AddressBook1_Address1 = value;
         } else {
 #line 305
           if (index == 2) {
 #line 306
             __ste_Client_AddressBook1_Address2 = value;
           } else {
 
           }
         }
       }
     } else {
 #line 307
       if (handle == 3) {
 #line 316
         if (index == 0) {
 #line 310
           __ste_Client_AddressBook2_Address0 = value;
         } else {
 #line 311
           if (index == 1) {
 #line 312
             __ste_Client_AddressBook2_Address1 = value;
           } else {
 #line 313
             if (index == 2) {
 #line 314
               __ste_Client_AddressBook2_Address2 = value;
             } else {
 
             }
           }
         }
       } else {
 
       }
     }
   }
 #line 1649 "ClientLib.c"
   return;
 }
 }
 #line 319 "ClientLib.c"
 int __ste_client_autoResponse0  =    0;
 #line 321 "ClientLib.c"
 int __ste_client_autoResponse1  =    0;
 #line 323 "ClientLib.c"
 int __ste_client_autoResponse2  =    0;
 #line 326 "ClientLib.c"
 int getClientAutoResponse(int handle ) 
 { int retValue_acc ;
 
   {
 #line 335 "ClientLib.c"
   if (handle == 1) {
 #line 1676
     retValue_acc = __ste_client_autoResponse0;
 #line 1678
     return (retValue_acc);
   } else {
 #line 1680
     if (handle == 2) {
 #line 1685
       retValue_acc = __ste_client_autoResponse1;
 #line 1687
       return (retValue_acc);
     } else {
 #line 1689
       if (handle == 3) {
 #line 1694
         retValue_acc = __ste_client_autoResponse2;
 #line 1696
         return (retValue_acc);
       } else {
 #line 1702 "ClientLib.c"
         retValue_acc = -1;
 #line 1704
         return (retValue_acc);
       }
     }
   }
 #line 1711 "ClientLib.c"
   return (retValue_acc);
 }
 }
 #line 338 "ClientLib.c"
 void setClientAutoResponse(int handle , int value ) 
 { 
 
   {
 #line 346
   if (handle == 1) {
 #line 340
     __ste_client_autoResponse0 = value;
   } else {
 #line 341
     if (handle == 2) {
 #line 342
       __ste_client_autoResponse1 = value;
     } else {
 #line 343
       if (handle == 3) {
 #line 344
         __ste_client_autoResponse2 = value;
       } else {
 
       }
     }
   }
 #line 1746 "ClientLib.c"
   return;
 }
 }
 #line 348 "ClientLib.c"
 int __ste_client_privateKey0  =    0;
 #line 350 "ClientLib.c"
 int __ste_client_privateKey1  =    0;
 #line 352 "ClientLib.c"
 int __ste_client_privateKey2  =    0;
 #line 355 "ClientLib.c"
 int getClientPrivateKey(int handle ) 
 { int retValue_acc ;
 
   {
 #line 364 "ClientLib.c"
   if (handle == 1) {
 #line 1773
     retValue_acc = __ste_client_privateKey0;
 #line 1775
     return (retValue_acc);
   } else {
 #line 1777
     if (handle == 2) {
 #line 1782
       retValue_acc = __ste_client_privateKey1;
 #line 1784
       return (retValue_acc);
     } else {
 #line 1786
       if (handle == 3) {
 #line 1791
         retValue_acc = __ste_client_privateKey2;
 #line 1793
        return (retValue_acc);
      } else {
#line 1799 "ClientLib.c"
        retValue_acc = 0;
#line 1801
        return (retValue_acc);
      }
    }
  }
#line 1808 "ClientLib.c"
  return (retValue_acc);
}
}
#line 367 "ClientLib.c"
void setClientPrivateKey(int handle , int value ) 
{ 

  {
#line 375
  if (handle == 1) {
#line 369
    __ste_client_privateKey0 = value;
  } else {
#line 370
    if (handle == 2) {
#line 371
      __ste_client_privateKey1 = value;
    } else {
#line 372
      if (handle == 3) {
#line 373
        __ste_client_privateKey2 = value;
      } else {

      }
    }
  }
#line 1843 "ClientLib.c"
  return;
}
}
#line 377 "ClientLib.c"
int __ste_ClientKeyring_size0  =    0;
#line 379 "ClientLib.c"
int __ste_ClientKeyring_size1  =    0;
#line 381 "ClientLib.c"
int __ste_ClientKeyring_size2  =    0;
#line 384 "ClientLib.c"
int getClientKeyringSize(int handle ) 
{ int retValue_acc ;

  {
#line 393 "ClientLib.c"
  if (handle == 1) {
#line 1870
    retValue_acc = __ste_ClientKeyring_size0;
#line 1872
    return (retValue_acc);
  } else {
#line 1874
    if (handle == 2) {
#line 1879
      retValue_acc = __ste_ClientKeyring_size1;
#line 1881
      return (retValue_acc);
    } else {
#line 1883
      if (handle == 3) {
#line 1888
        retValue_acc = __ste_ClientKeyring_size2;
#line 1890
        return (retValue_acc);
      } else {
#line 1896 "ClientLib.c"
        retValue_acc = 0;
#line 1898
        return (retValue_acc);
      }
    }
  }
#line 1905 "ClientLib.c"
  return (retValue_acc);
}
}
#line 396 "ClientLib.c"
void setClientKeyringSize(int handle , int value ) 
{ 

  {
#line 404
  if (handle == 1) {
#line 398
    __ste_ClientKeyring_size0 = value;
  } else {
#line 399
    if (handle == 2) {
#line 400
      __ste_ClientKeyring_size1 = value;
    } else {
#line 401
      if (handle == 3) {
#line 402
        __ste_ClientKeyring_size2 = value;
      } else {

      }
    }
  }
#line 1940 "ClientLib.c"
  return;
}
}
#line 406 "ClientLib.c"
int createClientKeyringEntry(int handle ) 
{ int retValue_acc ;
  int size ;
  int tmp ;
  int __cil_tmp5 ;

  {
  {
#line 407
  tmp = getClientKeyringSize(handle);
#line 407
  size = tmp;
  }
#line 408 "ClientLib.c"
  if (size < 2) {
    {
#line 409 "ClientLib.c"
    __cil_tmp5 = size + 1;
#line 409
    setClientKeyringSize(handle, __cil_tmp5);
#line 1967 "ClientLib.c"
    retValue_acc = size + 1;
    }
#line 1969
    return (retValue_acc);
  } else {
#line 1973 "ClientLib.c"
    retValue_acc = -1;
#line 1975
    return (retValue_acc);
  }
#line 1982 "ClientLib.c"
  return (retValue_acc);
}
}
#line 414 "ClientLib.c"
int __ste_Client_Keyring0_User0  =    0;
#line 416 "ClientLib.c"
int __ste_Client_Keyring0_User1  =    0;
#line 418 "ClientLib.c"
int __ste_Client_Keyring0_User2  =    0;
#line 420 "ClientLib.c"
int __ste_Client_Keyring1_User0  =    0;
#line 422 "ClientLib.c"
int __ste_Client_Keyring1_User1  =    0;
#line 424 "ClientLib.c"
int __ste_Client_Keyring1_User2  =    0;
#line 426 "ClientLib.c"
int __ste_Client_Keyring2_User0  =    0;
#line 428 "ClientLib.c"
int __ste_Client_Keyring2_User1  =    0;
#line 430 "ClientLib.c"
int __ste_Client_Keyring2_User2  =    0;
#line 433 "ClientLib.c"
int getClientKeyringUser(int handle , int index ) 
{ int retValue_acc ;

  {
#line 466
  if (handle == 1) {
#line 443 "ClientLib.c"
    if (index == 0) {
#line 2028
      retValue_acc = __ste_Client_Keyring0_User0;
#line 2030
      return (retValue_acc);
    } else {
#line 2032
      if (index == 1) {
#line 2037
        retValue_acc = __ste_Client_Keyring0_User1;
#line 2039
        return (retValue_acc);
      } else {
#line 2045
        retValue_acc = 0;
#line 2047
        return (retValue_acc);
      }
    }
  } else {
#line 2049 "ClientLib.c"
    if (handle == 2) {
#line 453 "ClientLib.c"
      if (index == 0) {
#line 2057
        retValue_acc = __ste_Client_Keyring1_User0;
#line 2059
        return (retValue_acc);
      } else {
#line 2061
        if (index == 1) {
#line 2066
          retValue_acc = __ste_Client_Keyring1_User1;
#line 2068
          return (retValue_acc);
        } else {
#line 2074
          retValue_acc = 0;
#line 2076
          return (retValue_acc);
        }
      }
    } else {
#line 2078 "ClientLib.c"
      if (handle == 3) {
#line 463 "ClientLib.c"
        if (index == 0) {
#line 2086
          retValue_acc = __ste_Client_Keyring2_User0;
#line 2088
          return (retValue_acc);
        } else {
#line 2090
          if (index == 1) {
#line 2095
            retValue_acc = __ste_Client_Keyring2_User1;
#line 2097
            return (retValue_acc);
          } else {
#line 2103
            retValue_acc = 0;
#line 2105
            return (retValue_acc);
          }
        }
      } else {
#line 2111 "ClientLib.c"
        retValue_acc = 0;
#line 2113
        return (retValue_acc);
      }
    }
  }
#line 2120 "ClientLib.c"
  return (retValue_acc);
}
}
#line 473 "ClientLib.c"
void setClientKeyringUser(int handle , int index , int value ) 
{ 

  {
#line 499
  if (handle == 1) {
#line 482
    if (index == 0) {
#line 476
      __ste_Client_Keyring0_User0 = value;
    } else {
#line 477
      if (index == 1) {
#line 478
        __ste_Client_Keyring0_User1 = value;
      } else {

      }
    }
  } else {
#line 479
    if (handle == 2) {
#line 490
      if (index == 0) {
#line 484
        __ste_Client_Keyring1_User0 = value;
      } else {
#line 485
        if (index == 1) {
#line 486
          __ste_Client_Keyring1_User1 = value;
        } else {

        }
      }
    } else {
#line 487
      if (handle == 3) {
#line 498
        if (index == 0) {
#line 492
          __ste_Client_Keyring2_User0 = value;
        } else {
#line 493
          if (index == 1) {
#line 494
            __ste_Client_Keyring2_User1 = value;
          } else {

          }
        }
      } else {

      }
    }
  }
#line 2176 "ClientLib.c"
  return;
}
}
#line 501 "ClientLib.c"
int __ste_Client_Keyring0_PublicKey0  =    0;
#line 503 "ClientLib.c"
int __ste_Client_Keyring0_PublicKey1  =    0;
#line 505 "ClientLib.c"
int __ste_Client_Keyring0_PublicKey2  =    0;
#line 507 "ClientLib.c"
int __ste_Client_Keyring1_PublicKey0  =    0;
#line 509 "ClientLib.c"
int __ste_Client_Keyring1_PublicKey1  =    0;
#line 511 "ClientLib.c"
int __ste_Client_Keyring1_PublicKey2  =    0;
#line 513 "ClientLib.c"
int __ste_Client_Keyring2_PublicKey0  =    0;
#line 515 "ClientLib.c"
int __ste_Client_Keyring2_PublicKey1  =    0;
#line 517 "ClientLib.c"
int __ste_Client_Keyring2_PublicKey2  =    0;
#line 520 "ClientLib.c"
int getClientKeyringPublicKey(int handle , int index ) 
{ int retValue_acc ;

  {
#line 553
  if (handle == 1) {
#line 530 "ClientLib.c"
    if (index == 0) {
#line 2218
      retValue_acc = __ste_Client_Keyring0_PublicKey0;
#line 2220
      return (retValue_acc);
    } else {
#line 2222
      if (index == 1) {
#line 2227
        retValue_acc = __ste_Client_Keyring0_PublicKey1;
#line 2229
        return (retValue_acc);
      } else {
#line 2235
        retValue_acc = 0;
#line 2237
        return (retValue_acc);
      }
    }
  } else {
#line 2239 "ClientLib.c"
    if (handle == 2) {
#line 540 "ClientLib.c"
      if (index == 0) {
#line 2247
        retValue_acc = __ste_Client_Keyring1_PublicKey0;
#line 2249
        return (retValue_acc);
      } else {
#line 2251
        if (index == 1) {
#line 2256
          retValue_acc = __ste_Client_Keyring1_PublicKey1;
#line 2258
          return (retValue_acc);
        } else {
#line 2264
          retValue_acc = 0;
#line 2266
          return (retValue_acc);
        }
      }
    } else {
#line 2268 "ClientLib.c"
      if (handle == 3) {
#line 550 "ClientLib.c"
        if (index == 0) {
#line 2276
          retValue_acc = __ste_Client_Keyring2_PublicKey0;
#line 2278
          return (retValue_acc);
        } else {
#line 2280
          if (index == 1) {
#line 2285
            retValue_acc = __ste_Client_Keyring2_PublicKey1;
#line 2287
            return (retValue_acc);
          } else {
#line 2293
            retValue_acc = 0;
#line 2295
            return (retValue_acc);
          }
        }
      } else {
#line 2301 "ClientLib.c"
        retValue_acc = 0;
#line 2303
        return (retValue_acc);
      }
    }
  }
#line 2310 "ClientLib.c"
  return (retValue_acc);
}
}
#line 557 "ClientLib.c"
int findPublicKey(int handle , int userid ) 
{ int retValue_acc ;

  {
#line 591
  if (handle == 1) {
#line 568 "ClientLib.c"
    if (userid == __ste_Client_Keyring0_User0) {
#line 2338
      retValue_acc = __ste_Client_Keyring0_PublicKey0;
#line 2340
      return (retValue_acc);
    } else {
#line 2342
      if (userid == __ste_Client_Keyring0_User1) {
#line 2347
        retValue_acc = __ste_Client_Keyring0_PublicKey1;
#line 2349
        return (retValue_acc);
      } else {
#line 2355
        retValue_acc = 0;
#line 2357
        return (retValue_acc);
      }
    }
  } else {
#line 2359 "ClientLib.c"
    if (handle == 2) {
#line 578 "ClientLib.c"
      if (userid == __ste_Client_Keyring1_User0) {
#line 2367
        retValue_acc = __ste_Client_Keyring1_PublicKey0;
#line 2369
        return (retValue_acc);
      } else {
#line 2371
        if (userid == __ste_Client_Keyring1_User1) {
#line 2376
          retValue_acc = __ste_Client_Keyring1_PublicKey1;
#line 2378
          return (retValue_acc);
        } else {
#line 2384
          retValue_acc = 0;
#line 2386
          return (retValue_acc);
        }
      }
    } else {
#line 2388 "ClientLib.c"
      if (handle == 3) {
#line 588 "ClientLib.c"
        if (userid == __ste_Client_Keyring2_User0) {
#line 2396
          retValue_acc = __ste_Client_Keyring2_PublicKey0;
#line 2398
          return (retValue_acc);
        } else {
#line 2400
          if (userid == __ste_Client_Keyring2_User1) {
#line 2405
            retValue_acc = __ste_Client_Keyring2_PublicKey1;
#line 2407
            return (retValue_acc);
          } else {
#line 2413
            retValue_acc = 0;
#line 2415
            return (retValue_acc);
          }
        }
      } else {
#line 2421 "ClientLib.c"
        retValue_acc = 0;
#line 2423
        return (retValue_acc);
      }
    }
  }
#line 2430 "ClientLib.c"
  return (retValue_acc);
}
}
#line 595 "ClientLib.c"
void setClientKeyringPublicKey(int handle , int index , int value ) 
{ 

  {
#line 621
  if (handle == 1) {
#line 604
    if (index == 0) {
#line 598
      __ste_Client_Keyring0_PublicKey0 = value;
    } else {
#line 599
      if (index == 1) {
#line 600
        __ste_Client_Keyring0_PublicKey1 = value;
      } else {

      }
    }
  } else {
#line 601
    if (handle == 2) {
#line 612
      if (index == 0) {
#line 606
        __ste_Client_Keyring1_PublicKey0 = value;
      } else {
#line 607
        if (index == 1) {
#line 608
          __ste_Client_Keyring1_PublicKey1 = value;
        } else {

        }
      }
    } else {
#line 609
      if (handle == 3) {
#line 620
        if (index == 0) {
#line 614
          __ste_Client_Keyring2_PublicKey0 = value;
        } else {
#line 615
          if (index == 1) {
#line 616
            __ste_Client_Keyring2_PublicKey1 = value;
          } else {

          }
        }
      } else {

      }
    }
  }
#line 2486 "ClientLib.c"
  return;
}
}
#line 623 "ClientLib.c"
int __ste_client_forwardReceiver0  =    0;
#line 625 "ClientLib.c"
int __ste_client_forwardReceiver1  =    0;
#line 627 "ClientLib.c"
int __ste_client_forwardReceiver2  =    0;
#line 629 "ClientLib.c"
int __ste_client_forwardReceiver3  =    0;
#line 631 "ClientLib.c"
int getClientForwardReceiver(int handle ) 
{ int retValue_acc ;

  {
#line 640 "ClientLib.c"
  if (handle == 1) {
#line 2515
    retValue_acc = __ste_client_forwardReceiver0;
#line 2517
    return (retValue_acc);
  } else {
#line 2519
    if (handle == 2) {
#line 2524
      retValue_acc = __ste_client_forwardReceiver1;
#line 2526
      return (retValue_acc);
    } else {
#line 2528
      if (handle == 3) {
#line 2533
        retValue_acc = __ste_client_forwardReceiver2;
#line 2535
        return (retValue_acc);
      } else {
#line 2541 "ClientLib.c"
        retValue_acc = 0;
#line 2543
        return (retValue_acc);
      }
    }
  }
#line 2550 "ClientLib.c"
  return (retValue_acc);
}
}
#line 643 "ClientLib.c"
void setClientForwardReceiver(int handle , int value ) 
{ 

  {
#line 651
  if (handle == 1) {
#line 645
    __ste_client_forwardReceiver0 = value;
  } else {
#line 646
    if (handle == 2) {
#line 647
      __ste_client_forwardReceiver1 = value;
    } else {
#line 648
      if (handle == 3) {
#line 649
        __ste_client_forwardReceiver2 = value;
      } else {

      }
    }
  }
#line 2585 "ClientLib.c"
  return;
}
}
#line 653 "ClientLib.c"
int __ste_client_idCounter0  =    0;
#line 655 "ClientLib.c"
int __ste_client_idCounter1  =    0;
#line 657 "ClientLib.c"
int __ste_client_idCounter2  =    0;
#line 660 "ClientLib.c"
int getClientId(int handle ) 
{ int retValue_acc ;

  {
#line 669 "ClientLib.c"
  if (handle == 1) {
#line 2612
    retValue_acc = __ste_client_idCounter0;
#line 2614
    return (retValue_acc);
  } else {
#line 2616
    if (handle == 2) {
#line 2621
      retValue_acc = __ste_client_idCounter1;
#line 2623
      return (retValue_acc);
    } else {
#line 2625
      if (handle == 3) {
#line 2630
        retValue_acc = __ste_client_idCounter2;
#line 2632
        return (retValue_acc);
      } else {
#line 2638 "ClientLib.c"
        retValue_acc = 0;
#line 2640
        return (retValue_acc);
      }
    }
  }
#line 2647 "ClientLib.c"
  return (retValue_acc);
}
}
#line 672 "ClientLib.c"
void setClientId(int handle , int value ) 
{ 

  {
#line 680
  if (handle == 1) {
#line 674
    __ste_client_idCounter0 = value;
  } else {
#line 675
    if (handle == 2) {
#line 676
      __ste_client_idCounter1 = value;
    } else {
#line 677
      if (handle == 3) {
#line 678
        __ste_client_idCounter2 = value;
      } else {

      }
    }
  }
#line 2682 "ClientLib.c"
  return;
}
}
#line 1 "Email.o"
#pragma merger(0,"Email.i","")
#line 359 "/usr/include/stdio.h"
extern int printf(char const   * __restrict  __format  , ...) ;
#line 8 "featureselect.h"
int __SELECTED_FEATURE_Base  ;
#line 11 "featureselect.h"
int __SELECTED_FEATURE_Keys  ;
#line 14 "featureselect.h"
int __SELECTED_FEATURE_Encrypt  ;
#line 17 "featureselect.h"
int __SELECTED_FEATURE_AutoResponder  ;
#line 20 "featureselect.h"
int __SELECTED_FEATURE_AddressBook  ;
#line 23 "featureselect.h"
int __SELECTED_FEATURE_Sign  ;
#line 26 "featureselect.h"
int __SELECTED_FEATURE_Forward  ;
#line 29 "featureselect.h"
int __SELECTED_FEATURE_Verify  ;
#line 32 "featureselect.h"
int __SELECTED_FEATURE_Decrypt  ;
#line 35 "featureselect.h"
int __GUIDSL_ROOT_PRODUCTION  ;
#line 37 "featureselect.h"
int __GUIDSL_NON_TERMINAL_main  ;
#line 6 "EmailLib.h"
int getEmailId(int handle ) ;
#line 10
int getEmailFrom(int handle ) ;
#line 12
void setEmailFrom(int handle , int value ) ;
#line 14
int getEmailTo(int handle ) ;
#line 16
void setEmailTo(int handle , int value ) ;
#line 26
int isEncrypted(int handle ) ;
#line 30
int getEmailEncryptionKey(int handle ) ;
#line 34
int isSigned(int handle ) ;
#line 38
int getEmailSignKey(int handle ) ;
#line 42
int isVerified(int handle ) ;
#line 6 "Email.h"
void printMail(int msg ) ;
#line 9
int isReadable(int msg ) ;
#line 12
int createEmail(int from , int to ) ;
#line 15
int cloneEmail(int msg ) ;
#line 9 "Email.c"
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 ;

  {
  {
#line 10
  tmp = getEmailId(msg);
#line 10
  __cil_tmp6 = (char const   * __restrict  )"ID:\n  %i\n";
#line 10
  printf(__cil_tmp6, tmp);
#line 11
  tmp___0 = getEmailFrom(msg);
#line 11
  __cil_tmp7 = (char const   * __restrict  )"FROM:\n  %i\n";
#line 11
  printf(__cil_tmp7, tmp___0);
#line 12
  tmp___1 = getEmailTo(msg);
#line 12
  __cil_tmp8 = (char const   * __restrict  )"TO:\n  %i\n";
#line 12
  printf(__cil_tmp8, tmp___1);
#line 13
  tmp___2 = isReadable(msg);
#line 13
  __cil_tmp9 = (char const   * __restrict  )"IS_READABLE\n  %i\n";
#line 13
  printf(__cil_tmp9, tmp___2);
  }
#line 601 "Email.c"
  return;
}
}
#line 17 "Email.c"
void printMail__wrappee__AddressBook(int msg ) 
{ int tmp ;
  int tmp___0 ;
  char const   * __restrict  __cil_tmp4 ;
  char const   * __restrict  __cil_tmp5 ;

  {
  {
#line 18
  printMail__wrappee__Keys(msg);
#line 19
  tmp = isEncrypted(msg);
#line 19
  __cil_tmp4 = (char const   * __restrict  )"ENCRYPTED\n  %d\n";
#line 19
  printf(__cil_tmp4, tmp);
#line 20
  tmp___0 = getEmailEncryptionKey(msg);
#line 20
  __cil_tmp5 = (char const   * __restrict  )"ENCRYPTION KEY\n  %d\n";
#line 20
  printf(__cil_tmp5, tmp___0);
  }
#line 625 "Email.c"
  return;
}
}
#line 26 "Email.c"
void printMail__wrappee__Forward(int msg ) 
{ int tmp ;
  int tmp___0 ;
  char const   * __restrict  __cil_tmp4 ;
  char const   * __restrict  __cil_tmp5 ;

  {
  {
#line 27
  printMail__wrappee__AddressBook(msg);
#line 28
  tmp = isSigned(msg);
#line 28
  __cil_tmp4 = (char const   * __restrict  )"SIGNED\n  %i\n";
#line 28
  printf(__cil_tmp4, tmp);
#line 29
  tmp___0 = getEmailSignKey(msg);
#line 29
  __cil_tmp5 = (char const   * __restrict  )"SIGNATURE\n  %i\n";
#line 29
  printf(__cil_tmp5, tmp___0);
  }
#line 649 "Email.c"
  return;
}
}
#line 33 "Email.c"
void printMail(int msg ) 
{ int tmp ;
  char const   * __restrict  __cil_tmp3 ;

  {
  {
#line 34
  printMail__wrappee__Forward(msg);
#line 35
  tmp = isVerified(msg);
#line 35
  __cil_tmp3 = (char const   * __restrict  )"SIGNATURE VERIFIED\n  %d\n";
#line 35
  printf(__cil_tmp3, tmp);
  }
#line 671 "Email.c"
  return;
}
}
#line 41 "Email.c"
int isReadable__wrappee__Keys(int msg ) 
{ int retValue_acc ;

  {
#line 689 "Email.c"
  retValue_acc = 1;
#line 691
  return (retValue_acc);
#line 698
  return (retValue_acc);
}
}
#line 49 "Email.c"
int isReadable(int msg ) 
{ int retValue_acc ;
  int tmp ;

  {
  {
#line 53
  tmp = isEncrypted(msg);
  }
#line 53 "Email.c"
  if (tmp) {
#line 727
    retValue_acc = 0;
#line 729
    return (retValue_acc);
  } else {
    {
#line 721 "Email.c"
    retValue_acc = isReadable__wrappee__Keys(msg);
    }
#line 723
    return (retValue_acc);
  }
#line 736 "Email.c"
  return (retValue_acc);
}
}
#line 57 "Email.c"
int cloneEmail(int msg ) 
{ int retValue_acc ;

  {
#line 758 "Email.c"
  retValue_acc = msg;
#line 760
  return (retValue_acc);
#line 767
  return (retValue_acc);
}
}
#line 62 "Email.c"
int createEmail(int from , int to ) 
{ int retValue_acc ;
  int msg ;

  {
  {
#line 63
  msg = 1;
#line 64
  setEmailFrom(msg, from);
#line 65
  setEmailTo(msg, to);
#line 797 "Email.c"
  retValue_acc = msg;
  }
#line 799
  return (retValue_acc);
#line 806
  return (retValue_acc);
}
}
#line 1 "scenario.o"
#pragma merger(0,"scenario.i","")
#line 17 "scenario.c"
void bobKeyAdd(void) ;
#line 24
void rjhDeletePrivateKey(void) ;
#line 28
void rjhKeyAdd(void) ;
#line 32
void chuckKeyAddRjh(void) ;
#line 36
void rjhEnableForwarding(void) ;
#line 40
void rjhKeyChange(void) ;
#line 44
void bobSetAddressBook(void) ;
#line 48
void chuckKeyAdd(void) ;
#line 52
void bobKeyChange(void) ;
#line 54
#line 61
void bobToRjh(void) ;
#line 1 "scenario.c"
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 ;

  {
#line 2
  op1 = 0;
#line 3
  op2 = 0;
#line 4
  op3 = 0;
#line 5
  op4 = 0;
#line 6
  op5 = 0;
#line 7
  op6 = 0;
#line 8
  op7 = 0;
#line 9
  op8 = 0;
#line 10
  op9 = 0;
#line 11
  op10 = 0;
#line 12
  op11 = 0;
#line 13
  splverifierCounter = 0;
  {
#line 14
  while (1) {
    while_0_continue: /* CIL Label */ ;
#line 14
    if (splverifierCounter < 4) {

    } else {
      goto while_0_break;
    }
#line 15
    splverifierCounter = splverifierCounter + 1;
#line 16
    if (! op1) {
      {
#line 16
      tmp___9 = __VERIFIER_nondet_int();
      }
#line 16
      if (tmp___9) {
        {
#line 17
        bobKeyAdd();
#line 18
        op1 = 1;
        }
      } else {
        goto _L___8;
      }
    } else {
      _L___8: /* CIL Label */ 
#line 19
      if (! op2) {
        {
#line 19
        tmp___8 = __VERIFIER_nondet_int();
        }
#line 19
        if (tmp___8) {
#line 21
          op2 = 1;
        } else {
          goto _L___7;
        }
      } else {
        _L___7: /* CIL Label */ 
#line 22
        if (! op3) {
          {
#line 22
          tmp___7 = __VERIFIER_nondet_int();
          }
#line 22
          if (tmp___7) {
            {
#line 24
            rjhDeletePrivateKey();
#line 25
            op3 = 1;
            }
          } else {
            goto _L___6;
          }
        } else {
          _L___6: /* CIL Label */ 
#line 26
          if (! op4) {
            {
#line 26
            tmp___6 = __VERIFIER_nondet_int();
            }
#line 26
            if (tmp___6) {
              {
#line 28
              rjhKeyAdd();
#line 29
              op4 = 1;
              }
            } else {
              goto _L___5;
            }
          } else {
            _L___5: /* CIL Label */ 
#line 30
            if (! op5) {
              {
#line 30
              tmp___5 = __VERIFIER_nondet_int();
              }
#line 30
              if (tmp___5) {
                {
#line 32
                chuckKeyAddRjh();
#line 33
                op5 = 1;
                }
              } else {
                goto _L___4;
              }
            } else {
              _L___4: /* CIL Label */ 
#line 34
              if (! op6) {
                {
#line 34
                tmp___4 = __VERIFIER_nondet_int();
                }
#line 34
                if (tmp___4) {
                  {
#line 36
                  rjhEnableForwarding();
#line 37
                  op6 = 1;
                  }
                } else {
                  goto _L___3;
                }
              } else {
                _L___3: /* CIL Label */ 
#line 38
                if (! op7) {
                  {
#line 38
                  tmp___3 = __VERIFIER_nondet_int();
                  }
#line 38
                  if (tmp___3) {
                    {
#line 40
                    rjhKeyChange();
#line 41
                    op7 = 1;
                    }
                  } else {
                    goto _L___2;
                  }
                } else {
                  _L___2: /* CIL Label */ 
#line 42
                  if (! op8) {
                    {
#line 42
                    tmp___2 = __VERIFIER_nondet_int();
                    }
#line 42
                    if (tmp___2) {
                      {
#line 44
                      bobSetAddressBook();
#line 45
                      op8 = 1;
                      }
                    } else {
                      goto _L___1;
                    }
                  } else {
                    _L___1: /* CIL Label */ 
#line 46
                    if (! op9) {
                      {
#line 46
                      tmp___1 = __VERIFIER_nondet_int();
                      }
#line 46
                      if (tmp___1) {
                        {
#line 48
                        chuckKeyAdd();
#line 49
                        op9 = 1;
                        }
                      } else {
                        goto _L___0;
                      }
                    } else {
                      _L___0: /* CIL Label */ 
#line 50
                      if (! op10) {
                        {
#line 50
                        tmp___0 = __VERIFIER_nondet_int();
                        }
#line 50
                        if (tmp___0) {
                          {
#line 52
                          bobKeyChange();
#line 53
                          op10 = 1;
                          }
                        } else {
                          goto _L;
                        }
                      } else {
                        _L: /* CIL Label */ 
#line 54
                        if (! op11) {
                          {
#line 54
                          tmp = __VERIFIER_nondet_int();
                          }
#line 54
                          if (tmp) {
                            {
#line 56
                            chuckKeyAdd();
#line 57
                            op11 = 1;
                            }
                          } else {
                            goto while_0_break;
                          }
                        } else {
                          goto while_0_break;
                        }
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  while_0_break: /* CIL Label */ ;
  }
  {
#line 61
  bobToRjh();
  }
#line 169 "scenario.c"
  return;
}
}
#line 1 "Util.o"
#pragma merger(0,"Util.i","")
#line 1 "Util.h"
int prompt(char *msg ) ;
#line 9 "Util.c"
int prompt(char *msg ) 
{ int retValue_acc ;
  int retval ;
  char const   * __restrict  __cil_tmp4 ;

  {
  {
#line 10
  __cil_tmp4 = (char const   * __restrict  )"%s\n";
#line 10
  printf(__cil_tmp4, msg);
#line 518 "Util.c"
  retValue_acc = retval;
  }
#line 520
  return (retValue_acc);
#line 527
  return (retValue_acc);
}
}
#line 1 "EmailLib.o"
#pragma merger(0,"EmailLib.i","")
#line 4 "EmailLib.h"
int initEmail(void) ;
#line 8
void setEmailId(int handle , int value ) ;
#line 18
char *getEmailSubject(int handle ) ;
#line 20
void setEmailSubject(int handle , char *value ) ;
#line 22
char *getEmailBody(int handle ) ;
#line 24
void setEmailBody(int handle , char *value ) ;
#line 28
void setEmailIsEncrypted(int handle , int value ) ;
#line 32
void setEmailEncryptionKey(int handle , int value ) ;
#line 36
void setEmailIsSigned(int handle , int value ) ;
#line 40
void setEmailSignKey(int handle , int value ) ;
#line 44
void setEmailIsSignatureVerified(int handle , int value ) ;
#line 5 "EmailLib.c"
int __ste_Email_counter  =    0;
#line 7 "EmailLib.c"
int initEmail(void) 
{ int retValue_acc ;

  {
#line 12 "EmailLib.c"
  if (__ste_Email_counter < 2) {
#line 670
    __ste_Email_counter = __ste_Email_counter + 1;
#line 670
    retValue_acc = __ste_Email_counter;
#line 672
    return (retValue_acc);
  } else {
#line 678 "EmailLib.c"
    retValue_acc = -1;
#line 680
    return (retValue_acc);
  }
#line 687 "EmailLib.c"
  return (retValue_acc);
}
}
#line 15 "EmailLib.c"
int __ste_email_id0  =    0;
#line 17 "EmailLib.c"
int __ste_email_id1  =    0;
#line 19 "EmailLib.c"
int getEmailId(int handle ) 
{ int retValue_acc ;

  {
#line 26 "EmailLib.c"
  if (handle == 1) {
#line 716
    retValue_acc = __ste_email_id0;
#line 718
    return (retValue_acc);
  } else {
#line 720
    if (handle == 2) {
#line 725
      retValue_acc = __ste_email_id1;
#line 727
      return (retValue_acc);
    } else {
#line 733 "EmailLib.c"
      retValue_acc = 0;
#line 735
      return (retValue_acc);
    }
  }
#line 742 "EmailLib.c"
  return (retValue_acc);
}
}
#line 29 "EmailLib.c"
void setEmailId(int handle , int value ) 
{ 

  {
#line 35
  if (handle == 1) {
#line 31
    __ste_email_id0 = value;
  } else {
#line 32
    if (handle == 2) {
#line 33
      __ste_email_id1 = value;
    } else {

    }
  }
#line 773 "EmailLib.c"
  return;
}
}
#line 37 "EmailLib.c"
int __ste_email_from0  =    0;
#line 39 "EmailLib.c"
int __ste_email_from1  =    0;
#line 41 "EmailLib.c"
int getEmailFrom(int handle ) 
{ int retValue_acc ;

  {
#line 48 "EmailLib.c"
  if (handle == 1) {
#line 798
    retValue_acc = __ste_email_from0;
#line 800
    return (retValue_acc);
  } else {
#line 802
    if (handle == 2) {
#line 807
      retValue_acc = __ste_email_from1;
#line 809
      return (retValue_acc);
    } else {
#line 815 "EmailLib.c"
      retValue_acc = 0;
#line 817
      return (retValue_acc);
    }
  }
#line 824 "EmailLib.c"
  return (retValue_acc);
}
}
#line 51 "EmailLib.c"
void setEmailFrom(int handle , int value ) 
{ 

  {
#line 57
  if (handle == 1) {
#line 53
    __ste_email_from0 = value;
  } else {
#line 54
    if (handle == 2) {
#line 55
      __ste_email_from1 = value;
    } else {

    }
  }
#line 855 "EmailLib.c"
  return;
}
}
#line 59 "EmailLib.c"
int __ste_email_to0  =    0;
#line 61 "EmailLib.c"
int __ste_email_to1  =    0;
#line 63 "EmailLib.c"
int getEmailTo(int handle ) 
{ int retValue_acc ;

  {
#line 70 "EmailLib.c"
  if (handle == 1) {
#line 880
    retValue_acc = __ste_email_to0;
#line 882
    return (retValue_acc);
  } else {
#line 884
    if (handle == 2) {
#line 889
      retValue_acc = __ste_email_to1;
#line 891
      return (retValue_acc);
    } else {
#line 897 "EmailLib.c"
      retValue_acc = 0;
#line 899
      return (retValue_acc);
    }
  }
#line 906 "EmailLib.c"
  return (retValue_acc);
}
}
#line 73 "EmailLib.c"
void setEmailTo(int handle , int value ) 
{ 

  {
#line 79
  if (handle == 1) {
#line 75
    __ste_email_to0 = value;
  } else {
#line 76
    if (handle == 2) {
#line 77
      __ste_email_to1 = value;
    } else {

    }
  }
#line 937 "EmailLib.c"
  return;
}
}
#line 81 "EmailLib.c"
char *__ste_email_subject0  ;
#line 83 "EmailLib.c"
char *__ste_email_subject1  ;
#line 85 "EmailLib.c"
char *getEmailSubject(int handle ) 
{ char *retValue_acc ;
  void *__cil_tmp3 ;

  {
#line 92 "EmailLib.c"
  if (handle == 1) {
#line 962
    retValue_acc = __ste_email_subject0;
#line 964
    return (retValue_acc);
  } else {
#line 966
    if (handle == 2) {
#line 971
      retValue_acc = __ste_email_subject1;
#line 973
      return (retValue_acc);
    } else {
#line 979 "EmailLib.c"
      __cil_tmp3 = (void *)0;
#line 979
      retValue_acc = (char *)__cil_tmp3;
#line 981
      return (retValue_acc);
    }
  }
#line 988 "EmailLib.c"
  return (retValue_acc);
}
}
#line 95 "EmailLib.c"
void setEmailSubject(int handle , char *value ) 
{ 

  {
#line 101
  if (handle == 1) {
#line 97
    __ste_email_subject0 = value;
  } else {
#line 98
    if (handle == 2) {
#line 99
      __ste_email_subject1 = value;
    } else {

    }
  }
#line 1019 "EmailLib.c"
  return;
}
}
#line 103 "EmailLib.c"
char *__ste_email_body0  =    (char *)0;
#line 105 "EmailLib.c"
char *__ste_email_body1  =    (char *)0;
#line 107 "EmailLib.c"
char *getEmailBody(int handle ) 
{ char *retValue_acc ;
  void *__cil_tmp3 ;

  {
#line 114 "EmailLib.c"
  if (handle == 1) {
#line 1044
    retValue_acc = __ste_email_body0;
#line 1046
    return (retValue_acc);
  } else {
#line 1048
    if (handle == 2) {
#line 1053
      retValue_acc = __ste_email_body1;
#line 1055
      return (retValue_acc);
    } else {
#line 1061 "EmailLib.c"
      __cil_tmp3 = (void *)0;
#line 1061
      retValue_acc = (char *)__cil_tmp3;
#line 1063
      return (retValue_acc);
    }
  }
#line 1070 "EmailLib.c"
  return (retValue_acc);
}
}
#line 117 "EmailLib.c"
void setEmailBody(int handle , char *value ) 
{ 

  {
#line 123
  if (handle == 1) {
#line 119
    __ste_email_body0 = value;
  } else {
#line 120
    if (handle == 2) {
#line 121
      __ste_email_body1 = value;
    } else {

    }
  }
#line 1101 "EmailLib.c"
  return;
}
}
#line 125 "EmailLib.c"
int __ste_email_isEncrypted0  =    0;
#line 127 "EmailLib.c"
int __ste_email_isEncrypted1  =    0;
#line 129 "EmailLib.c"
int isEncrypted(int handle ) 
{ int retValue_acc ;

  {
#line 136 "EmailLib.c"
  if (handle == 1) {
#line 1126
    retValue_acc = __ste_email_isEncrypted0;
#line 1128
    return (retValue_acc);
  } else {
#line 1130
    if (handle == 2) {
#line 1135
      retValue_acc = __ste_email_isEncrypted1;
#line 1137
      return (retValue_acc);
    } else {
#line 1143 "EmailLib.c"
      retValue_acc = 0;
#line 1145
      return (retValue_acc);
    }
  }
#line 1152 "EmailLib.c"
  return (retValue_acc);
}
}
#line 139 "EmailLib.c"
void setEmailIsEncrypted(int handle , int value ) 
{ 

  {
#line 145
  if (handle == 1) {
#line 141
    __ste_email_isEncrypted0 = value;
  } else {
#line 142
    if (handle == 2) {
#line 143
      __ste_email_isEncrypted1 = value;
    } else {

    }
  }
#line 1183 "EmailLib.c"
  return;
}
}
#line 147 "EmailLib.c"
int __ste_email_encryptionKey0  =    0;
#line 149 "EmailLib.c"
int __ste_email_encryptionKey1  =    0;
#line 151 "EmailLib.c"
int getEmailEncryptionKey(int handle ) 
{ int retValue_acc ;

  {
#line 158 "EmailLib.c"
  if (handle == 1) {
#line 1208
    retValue_acc = __ste_email_encryptionKey0;
#line 1210
    return (retValue_acc);
  } else {
#line 1212
    if (handle == 2) {
#line 1217
      retValue_acc = __ste_email_encryptionKey1;
#line 1219
      return (retValue_acc);
    } else {
#line 1225 "EmailLib.c"
      retValue_acc = 0;
#line 1227
      return (retValue_acc);
    }
  }
#line 1234 "EmailLib.c"
  return (retValue_acc);
}
}
#line 161 "EmailLib.c"
void setEmailEncryptionKey(int handle , int value ) 
{ 

  {
#line 167
  if (handle == 1) {
#line 163
    __ste_email_encryptionKey0 = value;
  } else {
#line 164
    if (handle == 2) {
#line 165
      __ste_email_encryptionKey1 = value;
    } else {

    }
  }
#line 1265 "EmailLib.c"
  return;
}
}
#line 169 "EmailLib.c"
int __ste_email_isSigned0  =    0;
#line 171 "EmailLib.c"
int __ste_email_isSigned1  =    0;
#line 173 "EmailLib.c"
int isSigned(int handle ) 
{ int retValue_acc ;

  {
#line 180 "EmailLib.c"
  if (handle == 1) {
#line 1290
    retValue_acc = __ste_email_isSigned0;
#line 1292
    return (retValue_acc);
  } else {
#line 1294
    if (handle == 2) {
#line 1299
      retValue_acc = __ste_email_isSigned1;
#line 1301
      return (retValue_acc);
    } else {
#line 1307 "EmailLib.c"
      retValue_acc = 0;
#line 1309
      return (retValue_acc);
    }
  }
#line 1316 "EmailLib.c"
  return (retValue_acc);
}
}
#line 183 "EmailLib.c"
void setEmailIsSigned(int handle , int value ) 
{ 

  {
#line 189
  if (handle == 1) {
#line 185
    __ste_email_isSigned0 = value;
  } else {
#line 186
    if (handle == 2) {
#line 187
      __ste_email_isSigned1 = value;
    } else {

    }
  }
#line 1347 "EmailLib.c"
  return;
}
}
#line 191 "EmailLib.c"
int __ste_email_signKey0  =    0;
#line 193 "EmailLib.c"
int __ste_email_signKey1  =    0;
#line 195 "EmailLib.c"
int getEmailSignKey(int handle ) 
{ int retValue_acc ;

  {
#line 202 "EmailLib.c"
  if (handle == 1) {
#line 1372
    retValue_acc = __ste_email_signKey0;
#line 1374
    return (retValue_acc);
  } else {
#line 1376
    if (handle == 2) {
#line 1381
      retValue_acc = __ste_email_signKey1;
#line 1383
      return (retValue_acc);
    } else {
#line 1389 "EmailLib.c"
      retValue_acc = 0;
#line 1391
      return (retValue_acc);
    }
  }
#line 1398 "EmailLib.c"
  return (retValue_acc);
}
}
#line 205 "EmailLib.c"
void setEmailSignKey(int handle , int value ) 
{ 

  {
#line 211
  if (handle == 1) {
#line 207
    __ste_email_signKey0 = value;
  } else {
#line 208
    if (handle == 2) {
#line 209
      __ste_email_signKey1 = value;
    } else {

    }
  }
#line 1429 "EmailLib.c"
  return;
}
}
#line 213 "EmailLib.c"
int __ste_email_isSignatureVerified0  ;
#line 215 "EmailLib.c"
int __ste_email_isSignatureVerified1  ;
#line 217 "EmailLib.c"
int isVerified(int handle ) 
{ int retValue_acc ;

  {
#line 224 "EmailLib.c"
  if (handle == 1) {
#line 1454
    retValue_acc = __ste_email_isSignatureVerified0;
#line 1456
    return (retValue_acc);
  } else {
#line 1458
    if (handle == 2) {
#line 1463
      retValue_acc = __ste_email_isSignatureVerified1;
#line 1465
      return (retValue_acc);
    } else {
#line 1471 "EmailLib.c"
      retValue_acc = 0;
#line 1473
      return (retValue_acc);
    }
  }
#line 1480 "EmailLib.c"
  return (retValue_acc);
}
}
#line 227 "EmailLib.c"
void setEmailIsSignatureVerified(int handle , int value ) 
{ 

  {
#line 233
  if (handle == 1) {
#line 229
    __ste_email_isSignatureVerified0 = value;
  } else {
#line 230
    if (handle == 2) {
#line 231
      __ste_email_isSignatureVerified1 = value;
    } else {

    }
  }
#line 1511 "EmailLib.c"
  return;
}
}
#line 1 "featureselect.o"
#pragma merger(0,"featureselect.i","")
#line 41 "featureselect.h"
int select_one(void) ;
#line 43
void select_features(void) ;
#line 45
void select_helpers(void) ;
#line 47
int valid_product(void) ;
#line 8 "featureselect.c"
int select_one(void) 
{ int retValue_acc ;
  int choice = __VERIFIER_nondet_int();

  {
#line 84 "featureselect.c"
  retValue_acc = choice;
#line 86
  return (retValue_acc);
#line 93
  return (retValue_acc);
}
}
#line 14 "featureselect.c"
void select_features(void) 
{ 

  {
#line 115 "featureselect.c"
  return;
}
}
#line 20 "featureselect.c"
void select_helpers(void) 
{ 

  {
#line 133 "featureselect.c"
  return;
}
}
#line 25 "featureselect.c"
int valid_product(void) 
{ int retValue_acc ;

  {
#line 151 "featureselect.c"
  retValue_acc = 1;
#line 153
  return (retValue_acc);
#line 160
  return (retValue_acc);
}
}
#line 1 "Client.o"
#pragma merger(0,"Client.i","")
#line 688 "/usr/include/stdio.h"
extern int puts(char const   *__s ) ;
#line 14 "Client.h"
void queue(int client , int msg ) ;
#line 17
int is_queue_empty(void) ;
#line 19
int get_queued_client(void) ;
#line 21
int get_queued_email(void) ;
#line 24
void mail(int client , int msg ) ;
#line 26
void outgoing(int client , int msg ) ;
#line 28
void deliver(int client , int msg ) ;
#line 30
void incoming(int client , int msg ) ;
#line 32
int createClient(char *name ) ;
#line 35
void sendEmail(int sender , int receiver ) ;
#line 40
int isKeyPairValid(int publicKey , int privateKey ) ;
#line 44
void generateKeyPair(int client , int seed ) ;
#line 45
void sendToAddressBook(int client , int msg ) ;
#line 47
void sign(int client , int msg ) ;
#line 49
void forward(int client , int msg ) ;
#line 51
void verify(int client , int msg ) ;
#line 6 "Client.c"
int queue_empty  =    1;
#line 9 "Client.c"
int queued_message  ;
#line 12 "Client.c"
int queued_client  ;
#line 18 "Client.c"
void mail(int client , int msg ) 
{ int tmp ;

  {
  {
#line 19
  puts("mail sent");
#line 20
  tmp = getEmailTo(msg);
#line 20
  incoming(tmp, msg);
  }
#line 737 "Client.c"
  return;
}
}
#line 27 "Client.c"
void outgoing__wrappee__Keys(int client , int msg ) 
{ int tmp ;

  {
  {
#line 28
  tmp = getClientId(client);
#line 28
  setEmailFrom(msg, tmp);
#line 29
  mail(client, msg);
  }
#line 759 "Client.c"
  return;
}
}
#line 33 "Client.c"
void outgoing__wrappee__Encrypt(int client , int msg ) 
{ int receiver ;
  int tmp ;
  int pubkey ;
  int tmp___0 ;

  {
  {
#line 36
  tmp = getEmailTo(msg);
#line 36
  receiver = tmp;
#line 37
  tmp___0 = findPublicKey(client, receiver);
#line 37
  pubkey = tmp___0;
  }
#line 38
  if (pubkey) {
    {
#line 39
    setEmailEncryptionKey(msg, pubkey);
#line 40
    setEmailIsEncrypted(msg, 1);
    }
  } else {

  }
  {
#line 45
  outgoing__wrappee__Keys(client, msg);
  }
#line 794 "Client.c"
  return;
}
}
#line 52 "Client.c"
void outgoing__wrappee__AddressBook(int client , int msg ) 
{ int size ;
  int tmp ;
  int receiver ;
  int tmp___0 ;
  int second ;
  int tmp___1 ;
  int tmp___2 ;

  {
  {
#line 54
  tmp = getClientAddressBookSize(client);
#line 54
  size = tmp;
  }
#line 56
  if (size) {
    {
#line 57
    sendToAddressBook(client, msg);
#line 58
    puts("sending to alias in address book\n");
#line 59
    tmp___0 = getEmailTo(msg);
#line 59
    receiver = tmp___0;
#line 61
    puts("sending to second receipient\n");
#line 62
    tmp___1 = getClientAddressBookAddress(client, 1);
#line 62
    second = tmp___1;
#line 63
    setEmailTo(msg, second);
#line 64
    outgoing__wrappee__Encrypt(client, msg);
#line 67
    tmp___2 = getClientAddressBookAddress(client, 0);
#line 67
    setEmailTo(msg, tmp___2);
#line 68
    outgoing__wrappee__Encrypt(client, msg);
    }
  } else {
    {
#line 70
    outgoing__wrappee__Encrypt(client, msg);
    }
  }
#line 844 "Client.c"
  return;
}
}
#line 78 "Client.c"
void outgoing(int client , int msg ) 
{ 

  {
  {
#line 79
  sign(client, msg);
#line 80
  outgoing__wrappee__AddressBook(client, msg);
  }
#line 866 "Client.c"
  return;
}
}
#line 868
void __utac_acc__VerifyForward_spec__1(int client , int msg ) ;
#line 87 "Client.c"
void deliver(int client , int msg ) 
{ int __utac__ad__arg1 ;
  int __utac__ad__arg2 ;

  {
  {
#line 879 "Client.c"
  __utac__ad__arg1 = client;
#line 880
  __utac__ad__arg2 = msg;
#line 881
  __utac_acc__VerifyForward_spec__1(__utac__ad__arg1, __utac__ad__arg2);
#line 88 "Client.c"
  puts("mail delivered\n");
  }
#line 896 "Client.c"
  return;
}
}
#line 95 "Client.c"
void incoming__wrappee__Sign(int client , int msg ) 
{ 

  {
  {
#line 96
  deliver(client, msg);
  }
#line 916 "Client.c"
  return;
}
}
#line 102 "Client.c"
void incoming__wrappee__Forward(int client , int msg ) 
{ int fwreceiver ;
  int tmp ;

  {
  {
#line 103
  incoming__wrappee__Sign(client, msg);
#line 104
  tmp = getClientForwardReceiver(client);
#line 104
  fwreceiver = tmp;
  }
#line 105
  if (fwreceiver) {
    {
#line 107
    setEmailTo(msg, fwreceiver);
#line 108
    forward(client, msg);
    }
  } else {

  }
#line 947 "Client.c"
  return;
}
}
#line 116 "Client.c"
void incoming__wrappee__Verify(int client , int msg ) 
{ 

  {
  {
#line 117
  verify(client, msg);
#line 118
  incoming__wrappee__Forward(client, msg);
  }
#line 969 "Client.c"
  return;
}
}
#line 123 "Client.c"
void incoming(int client , int msg ) 
{ int privkey ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;

  {
  {
#line 126
  tmp = getClientPrivateKey(client);
#line 126
  privkey = tmp;
  }
#line 127
  if (privkey) {
    {
#line 135
    tmp___0 = isEncrypted(msg);
    }
#line 135
    if (tmp___0) {
      {
#line 135
      tmp___1 = getEmailEncryptionKey(msg);
#line 135
      tmp___2 = isKeyPairValid(tmp___1, privkey);
      }
#line 135
      if (tmp___2) {
        {
#line 132
        setEmailIsEncrypted(msg, 0);
#line 133
        setEmailEncryptionKey(msg, 0);
        }
      } else {

      }
    } else {

    }
  } else {

  }
  {
#line 138
  incoming__wrappee__Verify(client, msg);
  }
#line 1003 "Client.c"
  return;
}
}
#line 142 "Client.c"
int createClient(char *name ) 
{ int retValue_acc ;
  int client ;
  int tmp ;

  {
  {
#line 143
  tmp = initClient();
#line 143
  client = tmp;
#line 1025 "Client.c"
  retValue_acc = client;
  }
#line 1027
  return (retValue_acc);
#line 1034
  return (retValue_acc);
}
}
#line 150 "Client.c"
void sendEmail(int sender , int receiver ) 
{ int email ;
  int tmp ;

  {
  {
#line 151
  tmp = createEmail(0, receiver);
#line 151
  email = tmp;
#line 152
  outgoing(sender, email);
  }
#line 1062 "Client.c"
  return;
}
}
#line 160 "Client.c"
void queue(int client , int msg ) 
{ 

  {
#line 161
  queue_empty = 0;
#line 162
  queued_message = msg;
#line 163
  queued_client = client;
#line 1086 "Client.c"
  return;
}
}
#line 169 "Client.c"
int is_queue_empty(void) 
{ int retValue_acc ;

  {
#line 1104 "Client.c"
  retValue_acc = queue_empty;
#line 1106
  return (retValue_acc);
#line 1113
  return (retValue_acc);
}
}
#line 176 "Client.c"
int get_queued_client(void) 
{ int retValue_acc ;

  {
#line 1135 "Client.c"
  retValue_acc = queued_client;
#line 1137
  return (retValue_acc);
#line 1144
  return (retValue_acc);
}
}
#line 183 "Client.c"
int get_queued_email(void) 
{ int retValue_acc ;

  {
#line 1166 "Client.c"
  retValue_acc = queued_message;
#line 1168
  return (retValue_acc);
#line 1175
  return (retValue_acc);
}
}
#line 189 "Client.c"
int isKeyPairValid(int publicKey , int privateKey ) 
{ int retValue_acc ;
  char const   * __restrict  __cil_tmp4 ;

  {
  {
#line 190
  __cil_tmp4 = (char const   * __restrict  )"keypair valid %d %d";
#line 190
  printf(__cil_tmp4, publicKey, privateKey);
  }
#line 191 "Client.c"
  if (! publicKey) {
#line 1200 "Client.c"
    retValue_acc = 0;
#line 1202
    return (retValue_acc);
  } else {
#line 191 "Client.c"
    if (! privateKey) {
#line 1200 "Client.c"
      retValue_acc = 0;
#line 1202
      return (retValue_acc);
    } else {

    }
  }
#line 1207 "Client.c"
  retValue_acc = privateKey == publicKey;
#line 1209
  return (retValue_acc);
#line 1216
  return (retValue_acc);
}
}
#line 199 "Client.c"
void generateKeyPair(int client , int seed ) 
{ 

  {
  {
#line 200
  setClientPrivateKey(client, seed);
  }
#line 1240 "Client.c"
  return;
}
}
#line 205 "Client.c"
void sendToAddressBook(int client , int msg ) 
{ 

  {
#line 1258 "Client.c"
  return;
}
}
#line 211 "Client.c"
void sign(int client , int msg ) 
{ int privkey ;
  int tmp ;

  {
  {
#line 212
  tmp = getClientPrivateKey(client);
#line 212
  privkey = tmp;
  }
#line 213
  if (! privkey) {
#line 214
    return;
  } else {

  }
  {
#line 215
  setEmailIsSigned(msg, 1);
#line 216
  setEmailSignKey(msg, privkey);
  }
#line 1288 "Client.c"
  return;
}
}
#line 221 "Client.c"
void forward(int client , int msg ) 
{ 

  {
  {
#line 222
  puts("Forwarding message.\n");
#line 223
  printMail(msg);
#line 224
  queue(client, msg);
  }
#line 1312 "Client.c"
  return;
}
}
#line 230 "Client.c"
void verify(int client , int msg ) 
{ int tmp ;
  int tmp___0 ;
  int pubkey ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  int tmp___4 ;

  {
  {
#line 235
  tmp = isReadable(msg);
  }
#line 235
  if (tmp) {
    {
#line 235
    tmp___0 = isSigned(msg);
    }
#line 235
    if (tmp___0) {

    } else {
#line 236
      return;
    }
  } else {
#line 236
    return;
  }
  {
#line 235
  tmp___1 = getEmailFrom(msg);
#line 235
  tmp___2 = findPublicKey(client, tmp___1);
#line 235
  pubkey = tmp___2;
  }
#line 236
  if (pubkey) {
    {
#line 236
    tmp___3 = getEmailSignKey(msg);
#line 236
    tmp___4 = isKeyPairValid(tmp___3, pubkey);
    }
#line 236
    if (tmp___4) {
      {
#line 237
      setEmailIsSignatureVerified(msg, 1);
      }
    } else {

    }
  } else {

  }
#line 1343 "Client.c"
  return;
}
}
#line 1 "VerifyForward_spec.o"
#pragma merger(0,"VerifyForward_spec.i","")
#line 4 "wsllib.h"
void __automaton_fail(void) ;
#line 12 "VerifyForward_spec.c"
void __utac_acc__VerifyForward_spec__1(int client , int msg ) 
{ int pubkey ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
#line 15
  puts("before deliver\n");
#line 17
  tmp___1 = isVerified(msg);
  }
#line 17
  if (tmp___1) {
    {
#line 18
    tmp = getEmailFrom(msg);
#line 18
    tmp___0 = findPublicKey(client, tmp);
#line 18
    pubkey = tmp___0;
    }
#line 19
    if (pubkey == 0) {
      {
#line 20
      __automaton_fail();
      }
    } else {

    }
  } else {

  }
#line 20
  return;
}
}
#line 1 "wsllib_check.o"
#pragma merger(0,"wsllib_check.i","")
#line 3 "wsllib_check.c"
void __automaton_fail(void) 
{ 

  {
  goto ERROR;
  ERROR: ;
#line 53 "wsllib_check.c"
  return;
}
}
#line 1 "libacc.o"
#pragma merger(0,"libacc.i","")
#line 73 "/usr/include/assert.h"
extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
                                                                      char const   *__file ,
                                                                      unsigned int __line ,
                                                                      char const   *__function ) ;
#line 471 "/usr/include/stdlib.h"
extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
#line 488
extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
#line 32 "libacc.c"
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 ;

  {
  {
#line 33
  excep = (struct __UTAC__EXCEPTION *)exception;
#line 34
  tmp = malloc(24UL);
#line 34
  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
#line 36
  mem_15 = (int (**)(int  , int  ))cf;
#line 36
  *mem_15 = cflow_func;
#line 37
  __cil_tmp7 = (unsigned long )cf;
#line 37
  __cil_tmp8 = __cil_tmp7 + 8;
#line 37
  mem_16 = (int *)__cil_tmp8;
#line 37
  *mem_16 = val;
#line 38
  __cil_tmp9 = (unsigned long )cf;
#line 38
  __cil_tmp10 = __cil_tmp9 + 16;
#line 38
  __cil_tmp11 = (unsigned long )excep;
#line 38
  __cil_tmp12 = __cil_tmp11 + 24;
#line 38
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
#line 38
  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
#line 38
  *mem_17 = *mem_18;
#line 39
  __cil_tmp13 = (unsigned long )excep;
#line 39
  __cil_tmp14 = __cil_tmp13 + 24;
#line 39
  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
#line 39
  *mem_19 = cf;
  }
#line 654 "libacc.c"
  return;
}
}
#line 44 "libacc.c"
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 ;

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

    } else {
      goto while_1_break;
    }
    }
    {
#line 50
    tmp = cf;
#line 51
    __cil_tmp10 = (unsigned long )cf;
#line 51
    __cil_tmp11 = __cil_tmp10 + 16;
#line 51
    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
#line 51
    cf = *mem_16;
#line 52
    __cil_tmp12 = (void *)tmp;
#line 52
    free(__cil_tmp12);
    }
  }
  while_1_break: /* CIL Label */ ;
  }
#line 55
  __cil_tmp13 = (unsigned long )excep;
#line 55
  __cil_tmp14 = __cil_tmp13 + 24;
#line 55
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
#line 55
  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
#line 694 "libacc.c"
  return;
}
}
#line 59 "libacc.c"
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 ;

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

    } else {
      goto while_2_break;
    }
    }
    {
#line 65
    mem_17 = (int (**)(int  , int  ))cf;
#line 65
    __cil_tmp10 = *mem_17;
#line 65
    __cil_tmp11 = (unsigned long )cf;
#line 65
    __cil_tmp12 = __cil_tmp11 + 8;
#line 65
    mem_18 = (int *)__cil_tmp12;
#line 65
    __cil_tmp13 = *mem_18;
#line 65
    (*__cil_tmp10)(4, __cil_tmp13);
#line 66
    __cil_tmp14 = (unsigned long )cf;
#line 66
    __cil_tmp15 = __cil_tmp14 + 16;
#line 66
    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
#line 66
    cf = *mem_19;
    }
  }
  while_2_break: /* CIL Label */ ;
  }
  {
#line 69
  __utac__exception__cf_handler_free(exception);
  }
#line 732 "libacc.c"
  return;
}
}
#line 80 "libacc.c"
void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
#line 80 "libacc.c"
static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
#line 79 "libacc.c"
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 ;

  {
#line 82 "libacc.c"
  if (count == 0) {
#line 758 "libacc.c"
    return (retValue_acc);
  } else {

  }
#line 86 "libacc.c"
  if (mode == 0) {
    {
#line 87
    tmp = malloc(16UL);
#line 87
    new = (struct __ACC__ERR *)tmp;
#line 88
    mem_18 = (void **)new;
#line 88
    *mem_18 = env;
#line 89
    __cil_tmp10 = (unsigned long )new;
#line 89
    __cil_tmp11 = __cil_tmp10 + 8;
#line 89
    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
#line 89
    *mem_19 = head;
#line 90
    head = new;
#line 776 "libacc.c"
    retValue_acc = (void *)new;
    }
#line 778
    return (retValue_acc);
  } else {

  }
#line 94 "libacc.c"
  if (mode == 1) {
#line 95
    temp = head;
    {
#line 98
    while (1) {
      while_3_continue: /* CIL Label */ ;
#line 98
      if (count > 1) {

      } else {
        goto while_3_break;
      }
      {
#line 99
      __cil_tmp12 = (unsigned long )temp;
#line 99
      __cil_tmp13 = __cil_tmp12 + 8;
#line 99
      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
#line 99
      next = *mem_20;
#line 100
      mem_21 = (void **)temp;
#line 100
      excep = *mem_21;
#line 101
      __cil_tmp14 = (void *)temp;
#line 101
      free(__cil_tmp14);
#line 102
      __utac__exception__cf_handler_reset(excep);
#line 103
      temp = next;
#line 104
      count = count - 1;
      }
    }
    while_3_break: /* CIL Label */ ;
    }
    {
#line 107
    __cil_tmp15 = (unsigned long )temp;
#line 107
    __cil_tmp16 = __cil_tmp15 + 8;
#line 107
    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
#line 107
    head = *mem_22;
#line 108
    mem_23 = (void **)temp;
#line 108
    excep = *mem_23;
#line 109
    __cil_tmp17 = (void *)temp;
#line 109
    free(__cil_tmp17);
#line 110
    __utac__exception__cf_handler_reset(excep);
#line 820 "libacc.c"
    retValue_acc = excep;
    }
#line 822
    return (retValue_acc);
  } else {

  }
#line 114
  if (mode == 2) {
#line 118 "libacc.c"
    if (head) {
#line 831
      mem_24 = (void **)head;
#line 831
      retValue_acc = *mem_24;
#line 833
      return (retValue_acc);
    } else {
#line 837 "libacc.c"
      retValue_acc = (void *)0;
#line 839
      return (retValue_acc);
    }
  } else {

  }
#line 846 "libacc.c"
  return (retValue_acc);
}
}
#line 122 "libacc.c"
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 ;

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

    } else {
      {
#line 123
      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                    123U, "__utac__get_this_arg");
      }
    }
    }
  } else {
    {
#line 123
    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                  123U, "__utac__get_this_arg");
    }
  }
#line 870 "libacc.c"
  __cil_tmp7 = i - 1;
#line 870
  __cil_tmp8 = (unsigned long )this;
#line 870
  __cil_tmp9 = __cil_tmp8 + 8;
#line 870
  mem_13 = (void ***)__cil_tmp9;
#line 870
  __cil_tmp10 = *mem_13;
#line 870
  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
#line 870
  retValue_acc = *__cil_tmp11;
#line 872
  return (retValue_acc);
#line 879
  return (retValue_acc);
}
}
#line 129 "libacc.c"
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 ;

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

    } else {
      {
#line 131
      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                    131U, "__utac__get_this_argtype");
      }
    }
    }
  } else {
    {
#line 131
    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                  131U, "__utac__get_this_argtype");
    }
  }
#line 903 "libacc.c"
  __cil_tmp7 = i - 1;
#line 903
  __cil_tmp8 = (unsigned long )this;
#line 903
  __cil_tmp9 = __cil_tmp8 + 24;
#line 903
  mem_13 = (char const   ***)__cil_tmp9;
#line 903
  __cil_tmp10 = *mem_13;
#line 903
  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
#line 903
  retValue_acc = *__cil_tmp11;
#line 905
  return (retValue_acc);
#line 912
  return (retValue_acc);
}
}
#line 1 "Test.o"
#pragma merger(0,"Test.i","")
#line 2 "Test.h"
int bob  ;
#line 5 "Test.h"
int rjh  ;
#line 8 "Test.h"
int chuck  ;
#line 11
void setup_bob(int bob___0 ) ;
#line 14
void setup_rjh(int rjh___0 ) ;
#line 17
void setup_chuck(int chuck___0 ) ;
#line 26
void rjhToBob(void) ;
#line 32
void setup(void) ;
#line 35
int main(void) ;
#line 39
void bobKeyAddChuck(void) ;
#line 45
void rjhKeyAddChuck(void) ;
#line 18 "Test.c"
void setup_bob__wrappee__Base(int bob___0 ) 
{ 

  {
  {
#line 19
  setClientId(bob___0, bob___0);
  }
#line 1334 "Test.c"
  return;
}
}
#line 23 "Test.c"
void setup_bob(int bob___0 ) 
{ 

  {
  {
#line 24
  setup_bob__wrappee__Base(bob___0);
#line 25
  setClientPrivateKey(bob___0, 123);
  }
#line 1356 "Test.c"
  return;
}
}
#line 33 "Test.c"
void setup_rjh__wrappee__Base(int rjh___0 ) 
{ 

  {
  {
#line 34
  setClientId(rjh___0, rjh___0);
  }
#line 1376 "Test.c"
  return;
}
}
#line 40 "Test.c"
void setup_rjh(int rjh___0 ) 
{ 

  {
  {
#line 42
  setup_rjh__wrappee__Base(rjh___0);
#line 43
  setClientPrivateKey(rjh___0, 456);
  }
#line 1398 "Test.c"
  return;
}
}
#line 50 "Test.c"
void setup_chuck__wrappee__Base(int chuck___0 ) 
{ 

  {
  {
#line 51
  setClientId(chuck___0, chuck___0);
  }
#line 1418 "Test.c"
  return;
}
}
#line 57 "Test.c"
void setup_chuck(int chuck___0 ) 
{ 

  {
  {
#line 58
  setup_chuck__wrappee__Base(chuck___0);
#line 59
  setClientPrivateKey(chuck___0, 789);
  }
#line 1440 "Test.c"
  return;
}
}
#line 69 "Test.c"
void bobToRjh(void) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;

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

  } else {
    {
#line 74
    tmp = get_queued_email();
#line 74
    tmp___0 = get_queued_client();
#line 74
    outgoing(tmp___0, tmp);
    }
  }
#line 1467 "Test.c"
  return;
}
}
#line 81 "Test.c"
void rjhToBob(void) 
{ 

  {
  {
#line 83
  puts("Please enter a subject and a message body.\n");
#line 84
  sendEmail(rjh, bob);
  }
#line 1489 "Test.c"
  return;
}
}
#line 88 "Test.c"
#line 95 "Test.c"
void setup(void) 
{ char const   * __restrict  __cil_tmp1 ;
  char const   * __restrict  __cil_tmp2 ;
  char const   * __restrict  __cil_tmp3 ;

  {
  {
#line 96
  bob = 1;
#line 97
  setup_bob(bob);
#line 98
  __cil_tmp1 = (char const   * __restrict  )"bob: %d\n";
#line 98
  printf(__cil_tmp1, bob);
#line 100
  rjh = 2;
#line 101
  setup_rjh(rjh);
#line 102
  __cil_tmp2 = (char const   * __restrict  )"rjh: %d\n";
#line 102
  printf(__cil_tmp2, rjh);
#line 104
  chuck = 3;
#line 105
  setup_chuck(chuck);
#line 106
  __cil_tmp3 = (char const   * __restrict  )"chuck: %d\n";
#line 106
  printf(__cil_tmp3, chuck);
  }
#line 1560 "Test.c"
  return;
}
}
#line 112 "Test.c"
int main(void) 
{ int retValue_acc ;
  int tmp ;

  {
  {
#line 113
  select_helpers();
#line 114
  select_features();
#line 115
  tmp = valid_product();
  }
#line 115
  if (tmp) {
    {
#line 116
    setup();
#line 117
    test();
    }
  } else {

  }
#line 1591 "Test.c"
  return (retValue_acc);
}
}
#line 125 "Test.c"
void bobKeyAdd(void) 
{ int tmp ;
  int tmp___0 ;
  char const   * __restrict  __cil_tmp3 ;
  char const   * __restrict  __cil_tmp4 ;

  {
  {
#line 126
  createClientKeyringEntry(bob);
#line 127
  setClientKeyringUser(bob, 0, 2);
#line 128
  setClientKeyringPublicKey(bob, 0, 456);
#line 129
  puts("bob added rjhs key");
#line 130
  tmp = getClientKeyringUser(bob, 0);
#line 130
  __cil_tmp3 = (char const   * __restrict  )"%d\n";
#line 130
  printf(__cil_tmp3, tmp);
#line 131
  tmp___0 = getClientKeyringPublicKey(bob, 0);
#line 131
  __cil_tmp4 = (char const   * __restrict  )"%d\n";
#line 131
  printf(__cil_tmp4, tmp___0);
  }
#line 1625 "Test.c"
  return;
}
}
#line 137 "Test.c"
void rjhKeyAdd(void) 
{ 

  {
  {
#line 138
  createClientKeyringEntry(rjh);
#line 139
  setClientKeyringUser(rjh, 0, 1);
#line 140
  setClientKeyringPublicKey(rjh, 0, 123);
  }
#line 1649 "Test.c"
  return;
}
}
#line 146 "Test.c"
void rjhKeyAddChuck(void) 
{ 

  {
  {
#line 147
  createClientKeyringEntry(rjh);
#line 148
  setClientKeyringUser(rjh, 0, 3);
#line 149
  setClientKeyringPublicKey(rjh, 0, 789);
  }
#line 1673 "Test.c"
  return;
}
}
#line 156 "Test.c"
void bobKeyAddChuck(void) 
{ 

  {
  {
#line 157
  createClientKeyringEntry(bob);
#line 158
  setClientKeyringUser(bob, 1, 3);
#line 159
  setClientKeyringPublicKey(bob, 1, 789);
  }
#line 1697 "Test.c"
  return;
}
}
#line 165 "Test.c"
void chuckKeyAdd(void) 
{ 

  {
  {
#line 166
  createClientKeyringEntry(chuck);
#line 167
  setClientKeyringUser(chuck, 0, 1);
#line 168
  setClientKeyringPublicKey(chuck, 0, 123);
  }
#line 1721 "Test.c"
  return;
}
}
#line 174 "Test.c"
void chuckKeyAddRjh(void) 
{ 

  {
  {
#line 175
  createClientKeyringEntry(chuck);
#line 176
  setClientKeyringUser(chuck, 0, 2);
#line 177
  setClientKeyringPublicKey(chuck, 0, 456);
  }
#line 1745 "Test.c"
  return;
}
}
#line 183 "Test.c"
void rjhDeletePrivateKey(void) 
{ 

  {
  {
#line 184
  setClientPrivateKey(rjh, 0);
  }
#line 1765 "Test.c"
  return;
}
}
#line 190 "Test.c"
void bobKeyChange(void) 
{ 

  {
  {
#line 191
  generateKeyPair(bob, 777);
  }
#line 1785 "Test.c"
  return;
}
}
#line 197 "Test.c"
void rjhKeyChange(void) 
{ 

  {
  {
#line 198
  generateKeyPair(rjh, 666);
  }
#line 1805 "Test.c"
  return;
}
}
#line 203 "Test.c"
void bobSetAddressBook(void) 
{ 

  {
  {
#line 204
  setClientAddressBookSize(bob, 1);
#line 205
  setClientAddressBookAlias(bob, 0, rjh);
#line 206
  setClientAddressBookAddress(bob, 0, rjh);
#line 207
  setClientAddressBookAddress(bob, 1, chuck);
  }
#line 1831 "Test.c"
  return;
}
}
#line 213 "Test.c"
void rjhEnableForwarding(void) 
{ 

  {
  {
#line 214
  setClientForwardReceiver(rjh, chuck);
  }
#line 1851 "Test.c"
  return;
}
}