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