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