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 "VerifyForward_spec.o"
1706#pragma merger(0,"VerifyForward_spec.i","")
1707#line 4 "wsllib.h"
1708void __automaton_fail(void) ;
1709#line 688 "/usr/include/stdio.h"
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 10 "EmailLib.h"
1734int getEmailFrom(int handle ) ;
1735#line 42
1736int isVerified(int handle ) ;
1737#line 12 "VerifyForward_spec.c"
1738__inline void __utac_acc__VerifyForward_spec__1(int client , int msg )
1739{ int pubkey ;
1740 int tmp ;
1741 int tmp___0 ;
1742 int tmp___1 ;
1743
1744 {
1745 {
1746#line 15
1747 puts("before deliver\n");
1748#line 17
1749 tmp___1 = isVerified(msg);
1750 }
1751#line 17
1752 if (tmp___1) {
1753 {
1754#line 18
1755 tmp = getEmailFrom(msg);
1756#line 18
1757 tmp___0 = findPublicKey(client, tmp);
1758#line 18
1759 pubkey = tmp___0;
1760 }
1761#line 19
1762 if (pubkey == 0) {
1763 {
1764#line 20
1765 __automaton_fail();
1766 }
1767 } else {
1768
1769 }
1770 } else {
1771
1772 }
1773#line 20
1774 return;
1775}
1776}
1777#line 1 "wsllib_check.o"
1778#pragma merger(0,"wsllib_check.i","")
1779#line 3 "wsllib_check.c"
1780void __automaton_fail(void)
1781{
1782
1783 {
1784 goto ERROR;
1785 ERROR: ;
1786#line 53 "wsllib_check.c"
1787 return;
1788}
1789}
1790#line 1 "Util.o"
1791#pragma merger(0,"Util.i","")
1792#line 359 "/usr/include/stdio.h"
1793extern int printf(char const * __restrict __format , ...) ;
1794#line 1 "Util.h"
1795int prompt(char *msg ) ;
1796#line 9 "Util.c"
1797int prompt(char *msg )
1798{ int retValue_acc ;
1799 int retval ;
1800 char const * __restrict __cil_tmp4 ;
1801
1802 {
1803 {
1804#line 10
1805 __cil_tmp4 = (char const * __restrict )"%s\n";
1806#line 10
1807 printf(__cil_tmp4, msg);
1808#line 518 "Util.c"
1809 retValue_acc = retval;
1810 }
1811#line 520
1812 return (retValue_acc);
1813#line 527
1814 return (retValue_acc);
1815}
1816}
1817#line 1 "libacc.o"
1818#pragma merger(0,"libacc.i","")
1819#line 73 "/usr/include/assert.h"
1820extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
1821 char const *__file ,
1822 unsigned int __line ,
1823 char const *__function ) ;
1824#line 471 "/usr/include/stdlib.h"
1825extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
1826#line 488
1827extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
1828#line 32 "libacc.c"
1829void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
1830 int ) ,
1831 int val )
1832{ struct __UTAC__EXCEPTION *excep ;
1833 struct __UTAC__CFLOW_FUNC *cf ;
1834 void *tmp ;
1835 unsigned long __cil_tmp7 ;
1836 unsigned long __cil_tmp8 ;
1837 unsigned long __cil_tmp9 ;
1838 unsigned long __cil_tmp10 ;
1839 unsigned long __cil_tmp11 ;
1840 unsigned long __cil_tmp12 ;
1841 unsigned long __cil_tmp13 ;
1842 unsigned long __cil_tmp14 ;
1843 int (**mem_15)(int , int ) ;
1844 int *mem_16 ;
1845 struct __UTAC__CFLOW_FUNC **mem_17 ;
1846 struct __UTAC__CFLOW_FUNC **mem_18 ;
1847 struct __UTAC__CFLOW_FUNC **mem_19 ;
1848
1849 {
1850 {
1851#line 33
1852 excep = (struct __UTAC__EXCEPTION *)exception;
1853#line 34
1854 tmp = malloc(24UL);
1855#line 34
1856 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
1857#line 36
1858 mem_15 = (int (**)(int , int ))cf;
1859#line 36
1860 *mem_15 = cflow_func;
1861#line 37
1862 __cil_tmp7 = (unsigned long )cf;
1863#line 37
1864 __cil_tmp8 = __cil_tmp7 + 8;
1865#line 37
1866 mem_16 = (int *)__cil_tmp8;
1867#line 37
1868 *mem_16 = val;
1869#line 38
1870 __cil_tmp9 = (unsigned long )cf;
1871#line 38
1872 __cil_tmp10 = __cil_tmp9 + 16;
1873#line 38
1874 __cil_tmp11 = (unsigned long )excep;
1875#line 38
1876 __cil_tmp12 = __cil_tmp11 + 24;
1877#line 38
1878 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
1879#line 38
1880 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
1881#line 38
1882 *mem_17 = *mem_18;
1883#line 39
1884 __cil_tmp13 = (unsigned long )excep;
1885#line 39
1886 __cil_tmp14 = __cil_tmp13 + 24;
1887#line 39
1888 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
1889#line 39
1890 *mem_19 = cf;
1891 }
1892#line 654 "libacc.c"
1893 return;
1894}
1895}
1896#line 44 "libacc.c"
1897void __utac__exception__cf_handler_free(void *exception )
1898{ struct __UTAC__EXCEPTION *excep ;
1899 struct __UTAC__CFLOW_FUNC *cf ;
1900 struct __UTAC__CFLOW_FUNC *tmp ;
1901 unsigned long __cil_tmp5 ;
1902 unsigned long __cil_tmp6 ;
1903 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
1904 unsigned long __cil_tmp8 ;
1905 unsigned long __cil_tmp9 ;
1906 unsigned long __cil_tmp10 ;
1907 unsigned long __cil_tmp11 ;
1908 void *__cil_tmp12 ;
1909 unsigned long __cil_tmp13 ;
1910 unsigned long __cil_tmp14 ;
1911 struct __UTAC__CFLOW_FUNC **mem_15 ;
1912 struct __UTAC__CFLOW_FUNC **mem_16 ;
1913 struct __UTAC__CFLOW_FUNC **mem_17 ;
1914
1915 {
1916#line 45
1917 excep = (struct __UTAC__EXCEPTION *)exception;
1918#line 46
1919 __cil_tmp5 = (unsigned long )excep;
1920#line 46
1921 __cil_tmp6 = __cil_tmp5 + 24;
1922#line 46
1923 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
1924#line 46
1925 cf = *mem_15;
1926 {
1927#line 49
1928 while (1) {
1929 while_0_continue: ;
1930 {
1931#line 49
1932 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
1933#line 49
1934 __cil_tmp8 = (unsigned long )__cil_tmp7;
1935#line 49
1936 __cil_tmp9 = (unsigned long )cf;
1937#line 49
1938 if (__cil_tmp9 != __cil_tmp8) {
1939
1940 } else {
1941 goto while_0_break;
1942 }
1943 }
1944 {
1945#line 50
1946 tmp = cf;
1947#line 51
1948 __cil_tmp10 = (unsigned long )cf;
1949#line 51
1950 __cil_tmp11 = __cil_tmp10 + 16;
1951#line 51
1952 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
1953#line 51
1954 cf = *mem_16;
1955#line 52
1956 __cil_tmp12 = (void *)tmp;
1957#line 52
1958 free(__cil_tmp12);
1959 }
1960 }
1961 while_0_break: ;
1962 }
1963#line 55
1964 __cil_tmp13 = (unsigned long )excep;
1965#line 55
1966 __cil_tmp14 = __cil_tmp13 + 24;
1967#line 55
1968 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
1969#line 55
1970 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
1971#line 694 "libacc.c"
1972 return;
1973}
1974}
1975#line 59 "libacc.c"
1976void __utac__exception__cf_handler_reset(void *exception )
1977{ struct __UTAC__EXCEPTION *excep ;
1978 struct __UTAC__CFLOW_FUNC *cf ;
1979 unsigned long __cil_tmp5 ;
1980 unsigned long __cil_tmp6 ;
1981 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
1982 unsigned long __cil_tmp8 ;
1983 unsigned long __cil_tmp9 ;
1984 int (*__cil_tmp10)(int , int ) ;
1985 unsigned long __cil_tmp11 ;
1986 unsigned long __cil_tmp12 ;
1987 int __cil_tmp13 ;
1988 unsigned long __cil_tmp14 ;
1989 unsigned long __cil_tmp15 ;
1990 struct __UTAC__CFLOW_FUNC **mem_16 ;
1991 int (**mem_17)(int , int ) ;
1992 int *mem_18 ;
1993 struct __UTAC__CFLOW_FUNC **mem_19 ;
1994
1995 {
1996#line 60
1997 excep = (struct __UTAC__EXCEPTION *)exception;
1998#line 61
1999 __cil_tmp5 = (unsigned long )excep;
2000#line 61
2001 __cil_tmp6 = __cil_tmp5 + 24;
2002#line 61
2003 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
2004#line 61
2005 cf = *mem_16;
2006 {
2007#line 64
2008 while (1) {
2009 while_1_continue: ;
2010 {
2011#line 64
2012 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
2013#line 64
2014 __cil_tmp8 = (unsigned long )__cil_tmp7;
2015#line 64
2016 __cil_tmp9 = (unsigned long )cf;
2017#line 64
2018 if (__cil_tmp9 != __cil_tmp8) {
2019
2020 } else {
2021 goto while_1_break;
2022 }
2023 }
2024 {
2025#line 65
2026 mem_17 = (int (**)(int , int ))cf;
2027#line 65
2028 __cil_tmp10 = *mem_17;
2029#line 65
2030 __cil_tmp11 = (unsigned long )cf;
2031#line 65
2032 __cil_tmp12 = __cil_tmp11 + 8;
2033#line 65
2034 mem_18 = (int *)__cil_tmp12;
2035#line 65
2036 __cil_tmp13 = *mem_18;
2037#line 65
2038 (*__cil_tmp10)(4, __cil_tmp13);
2039#line 66
2040 __cil_tmp14 = (unsigned long )cf;
2041#line 66
2042 __cil_tmp15 = __cil_tmp14 + 16;
2043#line 66
2044 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
2045#line 66
2046 cf = *mem_19;
2047 }
2048 }
2049 while_1_break: ;
2050 }
2051 {
2052#line 69
2053 __utac__exception__cf_handler_free(exception);
2054 }
2055#line 732 "libacc.c"
2056 return;
2057}
2058}
2059#line 80 "libacc.c"
2060void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
2061#line 80 "libacc.c"
2062static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
2063#line 79 "libacc.c"
2064void *__utac__error_stack_mgt(void *env , int mode , int count )
2065{ void *retValue_acc ;
2066 struct __ACC__ERR *new ;
2067 void *tmp ;
2068 struct __ACC__ERR *temp ;
2069 struct __ACC__ERR *next ;
2070 void *excep ;
2071 unsigned long __cil_tmp10 ;
2072 unsigned long __cil_tmp11 ;
2073 unsigned long __cil_tmp12 ;
2074 unsigned long __cil_tmp13 ;
2075 void *__cil_tmp14 ;
2076 unsigned long __cil_tmp15 ;
2077 unsigned long __cil_tmp16 ;
2078 void *__cil_tmp17 ;
2079 void **mem_18 ;
2080 struct __ACC__ERR **mem_19 ;
2081 struct __ACC__ERR **mem_20 ;
2082 void **mem_21 ;
2083 struct __ACC__ERR **mem_22 ;
2084 void **mem_23 ;
2085 void **mem_24 ;
2086
2087 {
2088#line 82 "libacc.c"
2089 if (count == 0) {
2090#line 758 "libacc.c"
2091 return (retValue_acc);
2092 } else {
2093
2094 }
2095#line 86 "libacc.c"
2096 if (mode == 0) {
2097 {
2098#line 87
2099 tmp = malloc(16UL);
2100#line 87
2101 new = (struct __ACC__ERR *)tmp;
2102#line 88
2103 mem_18 = (void **)new;
2104#line 88
2105 *mem_18 = env;
2106#line 89
2107 __cil_tmp10 = (unsigned long )new;
2108#line 89
2109 __cil_tmp11 = __cil_tmp10 + 8;
2110#line 89
2111 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
2112#line 89
2113 *mem_19 = head;
2114#line 90
2115 head = new;
2116#line 776 "libacc.c"
2117 retValue_acc = (void *)new;
2118 }
2119#line 778
2120 return (retValue_acc);
2121 } else {
2122
2123 }
2124#line 94 "libacc.c"
2125 if (mode == 1) {
2126#line 95
2127 temp = head;
2128 {
2129#line 98
2130 while (1) {
2131 while_2_continue: ;
2132#line 98
2133 if (count > 1) {
2134
2135 } else {
2136 goto while_2_break;
2137 }
2138 {
2139#line 99
2140 __cil_tmp12 = (unsigned long )temp;
2141#line 99
2142 __cil_tmp13 = __cil_tmp12 + 8;
2143#line 99
2144 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
2145#line 99
2146 next = *mem_20;
2147#line 100
2148 mem_21 = (void **)temp;
2149#line 100
2150 excep = *mem_21;
2151#line 101
2152 __cil_tmp14 = (void *)temp;
2153#line 101
2154 free(__cil_tmp14);
2155#line 102
2156 __utac__exception__cf_handler_reset(excep);
2157#line 103
2158 temp = next;
2159#line 104
2160 count = count - 1;
2161 }
2162 }
2163 while_2_break: ;
2164 }
2165 {
2166#line 107
2167 __cil_tmp15 = (unsigned long )temp;
2168#line 107
2169 __cil_tmp16 = __cil_tmp15 + 8;
2170#line 107
2171 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
2172#line 107
2173 head = *mem_22;
2174#line 108
2175 mem_23 = (void **)temp;
2176#line 108
2177 excep = *mem_23;
2178#line 109
2179 __cil_tmp17 = (void *)temp;
2180#line 109
2181 free(__cil_tmp17);
2182#line 110
2183 __utac__exception__cf_handler_reset(excep);
2184#line 820 "libacc.c"
2185 retValue_acc = excep;
2186 }
2187#line 822
2188 return (retValue_acc);
2189 } else {
2190
2191 }
2192#line 114
2193 if (mode == 2) {
2194#line 118 "libacc.c"
2195 if (head) {
2196#line 831
2197 mem_24 = (void **)head;
2198#line 831
2199 retValue_acc = *mem_24;
2200#line 833
2201 return (retValue_acc);
2202 } else {
2203#line 837 "libacc.c"
2204 retValue_acc = (void *)0;
2205#line 839
2206 return (retValue_acc);
2207 }
2208 } else {
2209
2210 }
2211#line 846 "libacc.c"
2212 return (retValue_acc);
2213}
2214}
2215#line 122 "libacc.c"
2216void *__utac__get_this_arg(int i , struct JoinPoint *this )
2217{ void *retValue_acc ;
2218 unsigned long __cil_tmp4 ;
2219 unsigned long __cil_tmp5 ;
2220 int __cil_tmp6 ;
2221 int __cil_tmp7 ;
2222 unsigned long __cil_tmp8 ;
2223 unsigned long __cil_tmp9 ;
2224 void **__cil_tmp10 ;
2225 void **__cil_tmp11 ;
2226 int *mem_12 ;
2227 void ***mem_13 ;
2228
2229 {
2230#line 123
2231 if (i > 0) {
2232 {
2233#line 123
2234 __cil_tmp4 = (unsigned long )this;
2235#line 123
2236 __cil_tmp5 = __cil_tmp4 + 16;
2237#line 123
2238 mem_12 = (int *)__cil_tmp5;
2239#line 123
2240 __cil_tmp6 = *mem_12;
2241#line 123
2242 if (i <= __cil_tmp6) {
2243
2244 } else {
2245 {
2246#line 123
2247 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2248 123U, "__utac__get_this_arg");
2249 }
2250 }
2251 }
2252 } else {
2253 {
2254#line 123
2255 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2256 123U, "__utac__get_this_arg");
2257 }
2258 }
2259#line 870 "libacc.c"
2260 __cil_tmp7 = i - 1;
2261#line 870
2262 __cil_tmp8 = (unsigned long )this;
2263#line 870
2264 __cil_tmp9 = __cil_tmp8 + 8;
2265#line 870
2266 mem_13 = (void ***)__cil_tmp9;
2267#line 870
2268 __cil_tmp10 = *mem_13;
2269#line 870
2270 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
2271#line 870
2272 retValue_acc = *__cil_tmp11;
2273#line 872
2274 return (retValue_acc);
2275#line 879
2276 return (retValue_acc);
2277}
2278}
2279#line 129 "libacc.c"
2280char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
2281{ char const *retValue_acc ;
2282 unsigned long __cil_tmp4 ;
2283 unsigned long __cil_tmp5 ;
2284 int __cil_tmp6 ;
2285 int __cil_tmp7 ;
2286 unsigned long __cil_tmp8 ;
2287 unsigned long __cil_tmp9 ;
2288 char const **__cil_tmp10 ;
2289 char const **__cil_tmp11 ;
2290 int *mem_12 ;
2291 char const ***mem_13 ;
2292
2293 {
2294#line 131
2295 if (i > 0) {
2296 {
2297#line 131
2298 __cil_tmp4 = (unsigned long )this;
2299#line 131
2300 __cil_tmp5 = __cil_tmp4 + 16;
2301#line 131
2302 mem_12 = (int *)__cil_tmp5;
2303#line 131
2304 __cil_tmp6 = *mem_12;
2305#line 131
2306 if (i <= __cil_tmp6) {
2307
2308 } else {
2309 {
2310#line 131
2311 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2312 131U, "__utac__get_this_argtype");
2313 }
2314 }
2315 }
2316 } else {
2317 {
2318#line 131
2319 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2320 131U, "__utac__get_this_argtype");
2321 }
2322 }
2323#line 903 "libacc.c"
2324 __cil_tmp7 = i - 1;
2325#line 903
2326 __cil_tmp8 = (unsigned long )this;
2327#line 903
2328 __cil_tmp9 = __cil_tmp8 + 24;
2329#line 903
2330 mem_13 = (char const ***)__cil_tmp9;
2331#line 903
2332 __cil_tmp10 = *mem_13;
2333#line 903
2334 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
2335#line 903
2336 retValue_acc = *__cil_tmp11;
2337#line 905
2338 return (retValue_acc);
2339#line 912
2340 return (retValue_acc);
2341}
2342}
2343#line 1 "Test.o"
2344#pragma merger(0,"Test.i","")
2345#line 43 "featureselect.h"
2346void select_features(void) ;
2347#line 45
2348void select_helpers(void) ;
2349#line 47
2350int valid_product(void) ;
2351#line 17 "Client.h"
2352int is_queue_empty(void) ;
2353#line 19
2354int get_queued_client(void) ;
2355#line 21
2356int get_queued_email(void) ;
2357#line 26
2358void outgoing(int client , int msg ) ;
2359#line 35
2360void sendEmail(int sender , int receiver ) ;
2361#line 44
2362void generateKeyPair(int client , int seed ) ;
2363#line 2 "Test.h"
2364int bob ;
2365#line 5 "Test.h"
2366int rjh ;
2367#line 8 "Test.h"
2368int chuck ;
2369#line 11
2370void setup_bob(int bob___0 ) ;
2371#line 14
2372void setup_rjh(int rjh___0 ) ;
2373#line 17
2374void setup_chuck(int chuck___0 ) ;
2375#line 23
2376void bobToRjh(void) ;
2377#line 26
2378void rjhToBob(void) ;
2379#line 29
2380void test(void) ;
2381#line 32
2382void setup(void) ;
2383#line 35
2384int main(void) ;
2385#line 36
2386void bobKeyAdd(void) ;
2387#line 39
2388void bobKeyAddChuck(void) ;
2389#line 42
2390void rjhKeyAdd(void) ;
2391#line 45
2392void rjhKeyAddChuck(void) ;
2393#line 48
2394void chuckKeyAdd(void) ;
2395#line 51
2396void bobKeyChange(void) ;
2397#line 54
2398void rjhKeyChange(void) ;
2399#line 57
2400void rjhDeletePrivateKey(void) ;
2401#line 60
2402void chuckKeyAddRjh(void) ;
2403#line 61
2404void rjhSetAutoRespond(void) ;
2405#line 63
2406void bobSetAddressBook(void) ;
2407#line 18 "Test.c"
2408void setup_bob__wrappee__Base(int bob___0 )
2409{
2410
2411 {
2412 {
2413#line 19
2414 setClientId(bob___0, bob___0);
2415 }
2416#line 1334 "Test.c"
2417 return;
2418}
2419}
2420#line 23 "Test.c"
2421void setup_bob(int bob___0 )
2422{
2423
2424 {
2425 {
2426#line 24
2427 setup_bob__wrappee__Base(bob___0);
2428#line 25
2429 setClientPrivateKey(bob___0, 123);
2430 }
2431#line 1356 "Test.c"
2432 return;
2433}
2434}
2435#line 33 "Test.c"
2436void setup_rjh__wrappee__Base(int rjh___0 )
2437{
2438
2439 {
2440 {
2441#line 34
2442 setClientId(rjh___0, rjh___0);
2443 }
2444#line 1376 "Test.c"
2445 return;
2446}
2447}
2448#line 40 "Test.c"
2449void setup_rjh(int rjh___0 )
2450{
2451
2452 {
2453 {
2454#line 42
2455 setup_rjh__wrappee__Base(rjh___0);
2456#line 43
2457 setClientPrivateKey(rjh___0, 456);
2458 }
2459#line 1398 "Test.c"
2460 return;
2461}
2462}
2463#line 50 "Test.c"
2464void setup_chuck__wrappee__Base(int chuck___0 )
2465{
2466
2467 {
2468 {
2469#line 51
2470 setClientId(chuck___0, chuck___0);
2471 }
2472#line 1418 "Test.c"
2473 return;
2474}
2475}
2476#line 57 "Test.c"
2477void setup_chuck(int chuck___0 )
2478{
2479
2480 {
2481 {
2482#line 58
2483 setup_chuck__wrappee__Base(chuck___0);
2484#line 59
2485 setClientPrivateKey(chuck___0, 789);
2486 }
2487#line 1440 "Test.c"
2488 return;
2489}
2490}
2491#line 69 "Test.c"
2492void bobToRjh(void)
2493{ int tmp ;
2494 int tmp___0 ;
2495 int tmp___1 ;
2496
2497 {
2498 {
2499#line 71
2500 puts("Please enter a subject and a message body.\n");
2501#line 72
2502 sendEmail(bob, rjh);
2503#line 73
2504 tmp___1 = is_queue_empty();
2505 }
2506#line 73
2507 if (tmp___1) {
2508
2509 } else {
2510 {
2511#line 74
2512 tmp = get_queued_email();
2513#line 74
2514 tmp___0 = get_queued_client();
2515#line 74
2516 outgoing(tmp___0, tmp);
2517 }
2518 }
2519#line 1467 "Test.c"
2520 return;
2521}
2522}
2523#line 81 "Test.c"
2524void rjhToBob(void)
2525{
2526
2527 {
2528 {
2529#line 83
2530 puts("Please enter a subject and a message body.\n");
2531#line 84
2532 sendEmail(rjh, bob);
2533 }
2534#line 1489 "Test.c"
2535 return;
2536}
2537}
2538#line 88 "Test.c"
2539#line 95 "Test.c"
2540void setup(void)
2541{ char const * __restrict __cil_tmp1 ;
2542 char const * __restrict __cil_tmp2 ;
2543 char const * __restrict __cil_tmp3 ;
2544
2545 {
2546 {
2547#line 96
2548 bob = 1;
2549#line 97
2550 setup_bob(bob);
2551#line 98
2552 __cil_tmp1 = (char const * __restrict )"bob: %d\n";
2553#line 98
2554 printf(__cil_tmp1, bob);
2555#line 100
2556 rjh = 2;
2557#line 101
2558 setup_rjh(rjh);
2559#line 102
2560 __cil_tmp2 = (char const * __restrict )"rjh: %d\n";
2561#line 102
2562 printf(__cil_tmp2, rjh);
2563#line 104
2564 chuck = 3;
2565#line 105
2566 setup_chuck(chuck);
2567#line 106
2568 __cil_tmp3 = (char const * __restrict )"chuck: %d\n";
2569#line 106
2570 printf(__cil_tmp3, chuck);
2571 }
2572#line 1560 "Test.c"
2573 return;
2574}
2575}
2576#line 112 "Test.c"
2577int main(void)
2578{ int retValue_acc ;
2579 int tmp ;
2580
2581 {
2582 {
2583#line 113
2584 select_helpers();
2585#line 114
2586 select_features();
2587#line 115
2588 tmp = valid_product();
2589 }
2590#line 115
2591 if (tmp) {
2592 {
2593#line 116
2594 setup();
2595#line 117
2596 test();
2597 }
2598 } else {
2599
2600 }
2601#line 1591 "Test.c"
2602 return (retValue_acc);
2603}
2604}
2605#line 125 "Test.c"
2606void bobKeyAdd(void)
2607{ int tmp ;
2608 int tmp___0 ;
2609 char const * __restrict __cil_tmp3 ;
2610 char const * __restrict __cil_tmp4 ;
2611
2612 {
2613 {
2614#line 126
2615 createClientKeyringEntry(bob);
2616#line 127
2617 setClientKeyringUser(bob, 0, 2);
2618#line 128
2619 setClientKeyringPublicKey(bob, 0, 456);
2620#line 129
2621 puts("bob added rjhs key");
2622#line 130
2623 tmp = getClientKeyringUser(bob, 0);
2624#line 130
2625 __cil_tmp3 = (char const * __restrict )"%d\n";
2626#line 130
2627 printf(__cil_tmp3, tmp);
2628#line 131
2629 tmp___0 = getClientKeyringPublicKey(bob, 0);
2630#line 131
2631 __cil_tmp4 = (char const * __restrict )"%d\n";
2632#line 131
2633 printf(__cil_tmp4, tmp___0);
2634 }
2635#line 1625 "Test.c"
2636 return;
2637}
2638}
2639#line 137 "Test.c"
2640void rjhKeyAdd(void)
2641{
2642
2643 {
2644 {
2645#line 138
2646 createClientKeyringEntry(rjh);
2647#line 139
2648 setClientKeyringUser(rjh, 0, 1);
2649#line 140
2650 setClientKeyringPublicKey(rjh, 0, 123);
2651 }
2652#line 1649 "Test.c"
2653 return;
2654}
2655}
2656#line 146 "Test.c"
2657void rjhKeyAddChuck(void)
2658{
2659
2660 {
2661 {
2662#line 147
2663 createClientKeyringEntry(rjh);
2664#line 148
2665 setClientKeyringUser(rjh, 0, 3);
2666#line 149
2667 setClientKeyringPublicKey(rjh, 0, 789);
2668 }
2669#line 1673 "Test.c"
2670 return;
2671}
2672}
2673#line 156 "Test.c"
2674void bobKeyAddChuck(void)
2675{
2676
2677 {
2678 {
2679#line 157
2680 createClientKeyringEntry(bob);
2681#line 158
2682 setClientKeyringUser(bob, 1, 3);
2683#line 159
2684 setClientKeyringPublicKey(bob, 1, 789);
2685 }
2686#line 1697 "Test.c"
2687 return;
2688}
2689}
2690#line 165 "Test.c"
2691void chuckKeyAdd(void)
2692{
2693
2694 {
2695 {
2696#line 166
2697 createClientKeyringEntry(chuck);
2698#line 167
2699 setClientKeyringUser(chuck, 0, 1);
2700#line 168
2701 setClientKeyringPublicKey(chuck, 0, 123);
2702 }
2703#line 1721 "Test.c"
2704 return;
2705}
2706}
2707#line 174 "Test.c"
2708void chuckKeyAddRjh(void)
2709{
2710
2711 {
2712 {
2713#line 175
2714 createClientKeyringEntry(chuck);
2715#line 176
2716 setClientKeyringUser(chuck, 0, 2);
2717#line 177
2718 setClientKeyringPublicKey(chuck, 0, 456);
2719 }
2720#line 1745 "Test.c"
2721 return;
2722}
2723}
2724#line 183 "Test.c"
2725void rjhDeletePrivateKey(void)
2726{
2727
2728 {
2729 {
2730#line 184
2731 setClientPrivateKey(rjh, 0);
2732 }
2733#line 1765 "Test.c"
2734 return;
2735}
2736}
2737#line 190 "Test.c"
2738void bobKeyChange(void)
2739{
2740
2741 {
2742 {
2743#line 191
2744 generateKeyPair(bob, 777);
2745 }
2746#line 1785 "Test.c"
2747 return;
2748}
2749}
2750#line 197 "Test.c"
2751void rjhKeyChange(void)
2752{
2753
2754 {
2755 {
2756#line 198
2757 generateKeyPair(rjh, 666);
2758 }
2759#line 1805 "Test.c"
2760 return;
2761}
2762}
2763#line 204 "Test.c"
2764void rjhSetAutoRespond(void)
2765{
2766
2767 {
2768 {
2769#line 205
2770 setClientAutoResponse(rjh, 1);
2771 }
2772#line 1825 "Test.c"
2773 return;
2774}
2775}
2776#line 210 "Test.c"
2777void bobSetAddressBook(void)
2778{
2779
2780 {
2781 {
2782#line 211
2783 setClientAddressBookSize(bob, 1);
2784#line 212
2785 setClientAddressBookAlias(bob, 0, rjh);
2786#line 213
2787 setClientAddressBookAddress(bob, 0, rjh);
2788#line 214
2789 setClientAddressBookAddress(bob, 1, chuck);
2790 }
2791#line 1851 "Test.c"
2792 return;
2793}
2794}
2795#line 1 "Client.o"
2796#pragma merger(0,"Client.i","")
2797#line 12 "EmailLib.h"
2798void setEmailFrom(int handle , int value ) ;
2799#line 14
2800int getEmailTo(int handle ) ;
2801#line 16
2802void setEmailTo(int handle , int value ) ;
2803#line 26
2804int isEncrypted(int handle ) ;
2805#line 28
2806void setEmailIsEncrypted(int handle , int value ) ;
2807#line 30
2808int getEmailEncryptionKey(int handle ) ;
2809#line 32
2810void setEmailEncryptionKey(int handle , int value ) ;
2811#line 34
2812int isSigned(int handle ) ;
2813#line 36
2814void setEmailIsSigned(int handle , int value ) ;
2815#line 38
2816int getEmailSignKey(int handle ) ;
2817#line 40
2818void setEmailSignKey(int handle , int value ) ;
2819#line 44
2820void setEmailIsSignatureVerified(int handle , int value ) ;
2821#line 9 "Email.h"
2822int isReadable(int msg ) ;
2823#line 12
2824int createEmail(int from , int to ) ;
2825#line 14 "Client.h"
2826void queue(int client , int msg ) ;
2827#line 24
2828void mail(int client , int msg ) ;
2829#line 28
2830void deliver(int client , int msg ) ;
2831#line 30
2832void incoming(int client , int msg ) ;
2833#line 32
2834int createClient(char *name ) ;
2835#line 40
2836int isKeyPairValid(int publicKey , int privateKey ) ;
2837#line 45
2838void autoRespond(int client , int msg ) ;
2839#line 46
2840void sendToAddressBook(int client , int msg ) ;
2841#line 48
2842void sign(int client , int msg ) ;
2843#line 50
2844void verify(int client , int msg ) ;
2845#line 6 "Client.c"
2846int queue_empty = 1;
2847#line 9 "Client.c"
2848int queued_message ;
2849#line 12 "Client.c"
2850int queued_client ;
2851#line 18 "Client.c"
2852void mail(int client , int msg )
2853{ int tmp ;
2854
2855 {
2856 {
2857#line 19
2858 puts("mail sent");
2859#line 20
2860 tmp = getEmailTo(msg);
2861#line 20
2862 incoming(tmp, msg);
2863 }
2864#line 737 "Client.c"
2865 return;
2866}
2867}
2868#line 27 "Client.c"
2869void outgoing__wrappee__Keys(int client , int msg )
2870{ int tmp ;
2871
2872 {
2873 {
2874#line 28
2875 tmp = getClientId(client);
2876#line 28
2877 setEmailFrom(msg, tmp);
2878#line 29
2879 mail(client, msg);
2880 }
2881#line 759 "Client.c"
2882 return;
2883}
2884}
2885#line 33 "Client.c"
2886void outgoing__wrappee__AutoResponder(int client , int msg )
2887{ int receiver ;
2888 int tmp ;
2889 int pubkey ;
2890 int tmp___0 ;
2891
2892 {
2893 {
2894#line 36
2895 tmp = getEmailTo(msg);
2896#line 36
2897 receiver = tmp;
2898#line 37
2899 tmp___0 = findPublicKey(client, receiver);
2900#line 37
2901 pubkey = tmp___0;
2902 }
2903#line 38
2904 if (pubkey) {
2905 {
2906#line 39
2907 setEmailEncryptionKey(msg, pubkey);
2908#line 40
2909 setEmailIsEncrypted(msg, 1);
2910 }
2911 } else {
2912
2913 }
2914 {
2915#line 45
2916 outgoing__wrappee__Keys(client, msg);
2917 }
2918#line 794 "Client.c"
2919 return;
2920}
2921}
2922#line 52 "Client.c"
2923void outgoing__wrappee__AddressBook(int client , int msg )
2924{ int size ;
2925 int tmp ;
2926 int receiver ;
2927 int tmp___0 ;
2928 int second ;
2929 int tmp___1 ;
2930 int tmp___2 ;
2931
2932 {
2933 {
2934#line 54
2935 tmp = getClientAddressBookSize(client);
2936#line 54
2937 size = tmp;
2938 }
2939#line 56
2940 if (size) {
2941 {
2942#line 57
2943 sendToAddressBook(client, msg);
2944#line 58
2945 puts("sending to alias in address book\n");
2946#line 59
2947 tmp___0 = getEmailTo(msg);
2948#line 59
2949 receiver = tmp___0;
2950#line 61
2951 puts("sending to second receipient\n");
2952#line 62
2953 tmp___1 = getClientAddressBookAddress(client, 1);
2954#line 62
2955 second = tmp___1;
2956#line 63
2957 setEmailTo(msg, second);
2958#line 64
2959 outgoing__wrappee__AutoResponder(client, msg);
2960#line 67
2961 tmp___2 = getClientAddressBookAddress(client, 0);
2962#line 67
2963 setEmailTo(msg, tmp___2);
2964#line 68
2965 outgoing__wrappee__AutoResponder(client, msg);
2966 }
2967 } else {
2968 {
2969#line 70
2970 outgoing__wrappee__AutoResponder(client, msg);
2971 }
2972 }
2973#line 844 "Client.c"
2974 return;
2975}
2976}
2977#line 78 "Client.c"
2978void outgoing(int client , int msg )
2979{
2980
2981 {
2982 {
2983#line 79
2984 sign(client, msg);
2985#line 80
2986 outgoing__wrappee__AddressBook(client, msg);
2987 }
2988#line 866 "Client.c"
2989 return;
2990}
2991}
2992#line 87 "Client.c"
2993void deliver(int client , int msg )
2994{ int __utac__ad__arg1 ;
2995 int __utac__ad__arg2 ;
2996
2997 {
2998 {
2999#line 879 "Client.c"
3000 __utac__ad__arg1 = client;
3001#line 880
3002 __utac__ad__arg2 = msg;
3003#line 881
3004 __utac_acc__VerifyForward_spec__1(__utac__ad__arg1, __utac__ad__arg2);
3005#line 88 "Client.c"
3006 puts("mail delivered\n");
3007 }
3008#line 896 "Client.c"
3009 return;
3010}
3011}
3012#line 95 "Client.c"
3013void incoming__wrappee__Encrypt(int client , int msg )
3014{
3015
3016 {
3017 {
3018#line 96
3019 deliver(client, msg);
3020 }
3021#line 916 "Client.c"
3022 return;
3023}
3024}
3025#line 102 "Client.c"
3026void incoming__wrappee__Sign(int client , int msg )
3027{ int tmp ;
3028
3029 {
3030 {
3031#line 103
3032 incoming__wrappee__Encrypt(client, msg);
3033#line 104
3034 tmp = getClientAutoResponse(client);
3035 }
3036#line 104
3037 if (tmp) {
3038 {
3039#line 105
3040 autoRespond(client, msg);
3041 }
3042 } else {
3043
3044 }
3045#line 941 "Client.c"
3046 return;
3047}
3048}
3049#line 112 "Client.c"
3050void incoming__wrappee__Verify(int client , int msg )
3051{
3052
3053 {
3054 {
3055#line 113
3056 verify(client, msg);
3057#line 114
3058 incoming__wrappee__Sign(client, msg);
3059 }
3060#line 963 "Client.c"
3061 return;
3062}
3063}
3064#line 119 "Client.c"
3065void incoming(int client , int msg )
3066{ int privkey ;
3067 int tmp ;
3068 int tmp___0 ;
3069 int tmp___1 ;
3070 int tmp___2 ;
3071
3072 {
3073 {
3074#line 122
3075 tmp = getClientPrivateKey(client);
3076#line 122
3077 privkey = tmp;
3078 }
3079#line 123
3080 if (privkey) {
3081 {
3082#line 131
3083 tmp___0 = isEncrypted(msg);
3084 }
3085#line 131
3086 if (tmp___0) {
3087 {
3088#line 131
3089 tmp___1 = getEmailEncryptionKey(msg);
3090#line 131
3091 tmp___2 = isKeyPairValid(tmp___1, privkey);
3092 }
3093#line 131
3094 if (tmp___2) {
3095 {
3096#line 128
3097 setEmailIsEncrypted(msg, 0);
3098#line 129
3099 setEmailEncryptionKey(msg, 0);
3100 }
3101 } else {
3102
3103 }
3104 } else {
3105
3106 }
3107 } else {
3108
3109 }
3110 {
3111#line 134
3112 incoming__wrappee__Verify(client, msg);
3113 }
3114#line 997 "Client.c"
3115 return;
3116}
3117}
3118#line 138 "Client.c"
3119int createClient(char *name )
3120{ int retValue_acc ;
3121 int client ;
3122 int tmp ;
3123
3124 {
3125 {
3126#line 139
3127 tmp = initClient();
3128#line 139
3129 client = tmp;
3130#line 1019 "Client.c"
3131 retValue_acc = client;
3132 }
3133#line 1021
3134 return (retValue_acc);
3135#line 1028
3136 return (retValue_acc);
3137}
3138}
3139#line 146 "Client.c"
3140void sendEmail(int sender , int receiver )
3141{ int email ;
3142 int tmp ;
3143
3144 {
3145 {
3146#line 147
3147 tmp = createEmail(0, receiver);
3148#line 147
3149 email = tmp;
3150#line 148
3151 outgoing(sender, email);
3152 }
3153#line 1056 "Client.c"
3154 return;
3155}
3156}
3157#line 156 "Client.c"
3158void queue(int client , int msg )
3159{
3160
3161 {
3162#line 157
3163 queue_empty = 0;
3164#line 158
3165 queued_message = msg;
3166#line 159
3167 queued_client = client;
3168#line 1080 "Client.c"
3169 return;
3170}
3171}
3172#line 165 "Client.c"
3173int is_queue_empty(void)
3174{ int retValue_acc ;
3175
3176 {
3177#line 1098 "Client.c"
3178 retValue_acc = queue_empty;
3179#line 1100
3180 return (retValue_acc);
3181#line 1107
3182 return (retValue_acc);
3183}
3184}
3185#line 172 "Client.c"
3186int get_queued_client(void)
3187{ int retValue_acc ;
3188
3189 {
3190#line 1129 "Client.c"
3191 retValue_acc = queued_client;
3192#line 1131
3193 return (retValue_acc);
3194#line 1138
3195 return (retValue_acc);
3196}
3197}
3198#line 179 "Client.c"
3199int get_queued_email(void)
3200{ int retValue_acc ;
3201
3202 {
3203#line 1160 "Client.c"
3204 retValue_acc = queued_message;
3205#line 1162
3206 return (retValue_acc);
3207#line 1169
3208 return (retValue_acc);
3209}
3210}
3211#line 185 "Client.c"
3212int isKeyPairValid(int publicKey , int privateKey )
3213{ int retValue_acc ;
3214 char const * __restrict __cil_tmp4 ;
3215
3216 {
3217 {
3218#line 186
3219 __cil_tmp4 = (char const * __restrict )"keypair valid %d %d";
3220#line 186
3221 printf(__cil_tmp4, publicKey, privateKey);
3222 }
3223#line 187 "Client.c"
3224 if (! publicKey) {
3225#line 1194 "Client.c"
3226 retValue_acc = 0;
3227#line 1196
3228 return (retValue_acc);
3229 } else {
3230#line 187 "Client.c"
3231 if (! privateKey) {
3232#line 1194 "Client.c"
3233 retValue_acc = 0;
3234#line 1196
3235 return (retValue_acc);
3236 } else {
3237
3238 }
3239 }
3240#line 1201 "Client.c"
3241 retValue_acc = privateKey == publicKey;
3242#line 1203
3243 return (retValue_acc);
3244#line 1210
3245 return (retValue_acc);
3246}
3247}
3248#line 195 "Client.c"
3249void generateKeyPair(int client , int seed )
3250{
3251
3252 {
3253 {
3254#line 196
3255 setClientPrivateKey(client, seed);
3256 }
3257#line 1234 "Client.c"
3258 return;
3259}
3260}
3261#line 202 "Client.c"
3262void autoRespond(int client , int msg )
3263{ int sender ;
3264 int tmp ;
3265
3266 {
3267 {
3268#line 203
3269 puts("sending autoresponse\n");
3270#line 204
3271 tmp = getEmailFrom(msg);
3272#line 204
3273 sender = tmp;
3274#line 205
3275 setEmailTo(msg, sender);
3276#line 206
3277 queue(client, msg);
3278 }
3279#line 1376 "Client.c"
3280 return;
3281}
3282}
3283#line 211 "Client.c"
3284void sendToAddressBook(int client , int msg )
3285{
3286
3287 {
3288#line 1394 "Client.c"
3289 return;
3290}
3291}
3292#line 217 "Client.c"
3293void sign(int client , int msg )
3294{ int privkey ;
3295 int tmp ;
3296
3297 {
3298 {
3299#line 218
3300 tmp = getClientPrivateKey(client);
3301#line 218
3302 privkey = tmp;
3303 }
3304#line 219
3305 if (! privkey) {
3306#line 220
3307 return;
3308 } else {
3309
3310 }
3311 {
3312#line 221
3313 setEmailIsSigned(msg, 1);
3314#line 222
3315 setEmailSignKey(msg, privkey);
3316 }
3317#line 1424 "Client.c"
3318 return;
3319}
3320}
3321#line 227 "Client.c"
3322void verify(int client , int msg )
3323{ int tmp ;
3324 int tmp___0 ;
3325 int pubkey ;
3326 int tmp___1 ;
3327 int tmp___2 ;
3328 int tmp___3 ;
3329 int tmp___4 ;
3330
3331 {
3332 {
3333#line 232
3334 tmp = isReadable(msg);
3335 }
3336#line 232
3337 if (tmp) {
3338 {
3339#line 232
3340 tmp___0 = isSigned(msg);
3341 }
3342#line 232
3343 if (tmp___0) {
3344
3345 } else {
3346#line 233
3347 return;
3348 }
3349 } else {
3350#line 233
3351 return;
3352 }
3353 {
3354#line 232
3355 tmp___1 = getEmailFrom(msg);
3356#line 232
3357 tmp___2 = findPublicKey(client, tmp___1);
3358#line 232
3359 pubkey = tmp___2;
3360 }
3361#line 233
3362 if (pubkey) {
3363 {
3364#line 233
3365 tmp___3 = getEmailSignKey(msg);
3366#line 233
3367 tmp___4 = isKeyPairValid(tmp___3, pubkey);
3368 }
3369#line 233
3370 if (tmp___4) {
3371 {
3372#line 234
3373 setEmailIsSignatureVerified(msg, 1);
3374 }
3375 } else {
3376
3377 }
3378 } else {
3379
3380 }
3381#line 1455 "Client.c"
3382 return;
3383}
3384}
3385#line 1 "EmailLib.o"
3386#pragma merger(0,"EmailLib.i","")
3387#line 4 "EmailLib.h"
3388int initEmail(void) ;
3389#line 6
3390int getEmailId(int handle ) ;
3391#line 8
3392void setEmailId(int handle , int value ) ;
3393#line 18
3394char *getEmailSubject(int handle ) ;
3395#line 20
3396void setEmailSubject(int handle , char *value ) ;
3397#line 22
3398char *getEmailBody(int handle ) ;
3399#line 24
3400void setEmailBody(int handle , char *value ) ;
3401#line 5 "EmailLib.c"
3402int __ste_Email_counter = 0;
3403#line 7 "EmailLib.c"
3404int initEmail(void)
3405{ int retValue_acc ;
3406
3407 {
3408#line 12 "EmailLib.c"
3409 if (__ste_Email_counter < 2) {
3410#line 670
3411 __ste_Email_counter = __ste_Email_counter + 1;
3412#line 670
3413 retValue_acc = __ste_Email_counter;
3414#line 672
3415 return (retValue_acc);
3416 } else {
3417#line 678 "EmailLib.c"
3418 retValue_acc = -1;
3419#line 680
3420 return (retValue_acc);
3421 }
3422#line 687 "EmailLib.c"
3423 return (retValue_acc);
3424}
3425}
3426#line 15 "EmailLib.c"
3427int __ste_email_id0 = 0;
3428#line 17 "EmailLib.c"
3429int __ste_email_id1 = 0;
3430#line 19 "EmailLib.c"
3431int getEmailId(int handle )
3432{ int retValue_acc ;
3433
3434 {
3435#line 26 "EmailLib.c"
3436 if (handle == 1) {
3437#line 716
3438 retValue_acc = __ste_email_id0;
3439#line 718
3440 return (retValue_acc);
3441 } else {
3442#line 720
3443 if (handle == 2) {
3444#line 725
3445 retValue_acc = __ste_email_id1;
3446#line 727
3447 return (retValue_acc);
3448 } else {
3449#line 733 "EmailLib.c"
3450 retValue_acc = 0;
3451#line 735
3452 return (retValue_acc);
3453 }
3454 }
3455#line 742 "EmailLib.c"
3456 return (retValue_acc);
3457}
3458}
3459#line 29 "EmailLib.c"
3460void setEmailId(int handle , int value )
3461{
3462
3463 {
3464#line 35
3465 if (handle == 1) {
3466#line 31
3467 __ste_email_id0 = value;
3468 } else {
3469#line 32
3470 if (handle == 2) {
3471#line 33
3472 __ste_email_id1 = value;
3473 } else {
3474
3475 }
3476 }
3477#line 773 "EmailLib.c"
3478 return;
3479}
3480}
3481#line 37 "EmailLib.c"
3482int __ste_email_from0 = 0;
3483#line 39 "EmailLib.c"
3484int __ste_email_from1 = 0;
3485#line 41 "EmailLib.c"
3486int getEmailFrom(int handle )
3487{ int retValue_acc ;
3488
3489 {
3490#line 48 "EmailLib.c"
3491 if (handle == 1) {
3492#line 798
3493 retValue_acc = __ste_email_from0;
3494#line 800
3495 return (retValue_acc);
3496 } else {
3497#line 802
3498 if (handle == 2) {
3499#line 807
3500 retValue_acc = __ste_email_from1;
3501#line 809
3502 return (retValue_acc);
3503 } else {
3504#line 815 "EmailLib.c"
3505 retValue_acc = 0;
3506#line 817
3507 return (retValue_acc);
3508 }
3509 }
3510#line 824 "EmailLib.c"
3511 return (retValue_acc);
3512}
3513}
3514#line 51 "EmailLib.c"
3515void setEmailFrom(int handle , int value )
3516{
3517
3518 {
3519#line 57
3520 if (handle == 1) {
3521#line 53
3522 __ste_email_from0 = value;
3523 } else {
3524#line 54
3525 if (handle == 2) {
3526#line 55
3527 __ste_email_from1 = value;
3528 } else {
3529
3530 }
3531 }
3532#line 855 "EmailLib.c"
3533 return;
3534}
3535}
3536#line 59 "EmailLib.c"
3537int __ste_email_to0 = 0;
3538#line 61 "EmailLib.c"
3539int __ste_email_to1 = 0;
3540#line 63 "EmailLib.c"
3541int getEmailTo(int handle )
3542{ int retValue_acc ;
3543
3544 {
3545#line 70 "EmailLib.c"
3546 if (handle == 1) {
3547#line 880
3548 retValue_acc = __ste_email_to0;
3549#line 882
3550 return (retValue_acc);
3551 } else {
3552#line 884
3553 if (handle == 2) {
3554#line 889
3555 retValue_acc = __ste_email_to1;
3556#line 891
3557 return (retValue_acc);
3558 } else {
3559#line 897 "EmailLib.c"
3560 retValue_acc = 0;
3561#line 899
3562 return (retValue_acc);
3563 }
3564 }
3565#line 906 "EmailLib.c"
3566 return (retValue_acc);
3567}
3568}
3569#line 73 "EmailLib.c"
3570void setEmailTo(int handle , int value )
3571{
3572
3573 {
3574#line 79
3575 if (handle == 1) {
3576#line 75
3577 __ste_email_to0 = value;
3578 } else {
3579#line 76
3580 if (handle == 2) {
3581#line 77
3582 __ste_email_to1 = value;
3583 } else {
3584
3585 }
3586 }
3587#line 937 "EmailLib.c"
3588 return;
3589}
3590}
3591#line 81 "EmailLib.c"
3592char *__ste_email_subject0 ;
3593#line 83 "EmailLib.c"
3594char *__ste_email_subject1 ;
3595#line 85 "EmailLib.c"
3596char *getEmailSubject(int handle )
3597{ char *retValue_acc ;
3598 void *__cil_tmp3 ;
3599
3600 {
3601#line 92 "EmailLib.c"
3602 if (handle == 1) {
3603#line 962
3604 retValue_acc = __ste_email_subject0;
3605#line 964
3606 return (retValue_acc);
3607 } else {
3608#line 966
3609 if (handle == 2) {
3610#line 971
3611 retValue_acc = __ste_email_subject1;
3612#line 973
3613 return (retValue_acc);
3614 } else {
3615#line 979 "EmailLib.c"
3616 __cil_tmp3 = (void *)0;
3617#line 979
3618 retValue_acc = (char *)__cil_tmp3;
3619#line 981
3620 return (retValue_acc);
3621 }
3622 }
3623#line 988 "EmailLib.c"
3624 return (retValue_acc);
3625}
3626}
3627#line 95 "EmailLib.c"
3628void setEmailSubject(int handle , char *value )
3629{
3630
3631 {
3632#line 101
3633 if (handle == 1) {
3634#line 97
3635 __ste_email_subject0 = value;
3636 } else {
3637#line 98
3638 if (handle == 2) {
3639#line 99
3640 __ste_email_subject1 = value;
3641 } else {
3642
3643 }
3644 }
3645#line 1019 "EmailLib.c"
3646 return;
3647}
3648}
3649#line 103 "EmailLib.c"
3650char *__ste_email_body0 = (char *)0;
3651#line 105 "EmailLib.c"
3652char *__ste_email_body1 = (char *)0;
3653#line 107 "EmailLib.c"
3654char *getEmailBody(int handle )
3655{ char *retValue_acc ;
3656 void *__cil_tmp3 ;
3657
3658 {
3659#line 114 "EmailLib.c"
3660 if (handle == 1) {
3661#line 1044
3662 retValue_acc = __ste_email_body0;
3663#line 1046
3664 return (retValue_acc);
3665 } else {
3666#line 1048
3667 if (handle == 2) {
3668#line 1053
3669 retValue_acc = __ste_email_body1;
3670#line 1055
3671 return (retValue_acc);
3672 } else {
3673#line 1061 "EmailLib.c"
3674 __cil_tmp3 = (void *)0;
3675#line 1061
3676 retValue_acc = (char *)__cil_tmp3;
3677#line 1063
3678 return (retValue_acc);
3679 }
3680 }
3681#line 1070 "EmailLib.c"
3682 return (retValue_acc);
3683}
3684}
3685#line 117 "EmailLib.c"
3686void setEmailBody(int handle , char *value )
3687{
3688
3689 {
3690#line 123
3691 if (handle == 1) {
3692#line 119
3693 __ste_email_body0 = value;
3694 } else {
3695#line 120
3696 if (handle == 2) {
3697#line 121
3698 __ste_email_body1 = value;
3699 } else {
3700
3701 }
3702 }
3703#line 1101 "EmailLib.c"
3704 return;
3705}
3706}
3707#line 125 "EmailLib.c"
3708int __ste_email_isEncrypted0 = 0;
3709#line 127 "EmailLib.c"
3710int __ste_email_isEncrypted1 = 0;
3711#line 129 "EmailLib.c"
3712int isEncrypted(int handle )
3713{ int retValue_acc ;
3714
3715 {
3716#line 136 "EmailLib.c"
3717 if (handle == 1) {
3718#line 1126
3719 retValue_acc = __ste_email_isEncrypted0;
3720#line 1128
3721 return (retValue_acc);
3722 } else {
3723#line 1130
3724 if (handle == 2) {
3725#line 1135
3726 retValue_acc = __ste_email_isEncrypted1;
3727#line 1137
3728 return (retValue_acc);
3729 } else {
3730#line 1143 "EmailLib.c"
3731 retValue_acc = 0;
3732#line 1145
3733 return (retValue_acc);
3734 }
3735 }
3736#line 1152 "EmailLib.c"
3737 return (retValue_acc);
3738}
3739}
3740#line 139 "EmailLib.c"
3741void setEmailIsEncrypted(int handle , int value )
3742{
3743
3744 {
3745#line 145
3746 if (handle == 1) {
3747#line 141
3748 __ste_email_isEncrypted0 = value;
3749 } else {
3750#line 142
3751 if (handle == 2) {
3752#line 143
3753 __ste_email_isEncrypted1 = value;
3754 } else {
3755
3756 }
3757 }
3758#line 1183 "EmailLib.c"
3759 return;
3760}
3761}
3762#line 147 "EmailLib.c"
3763int __ste_email_encryptionKey0 = 0;
3764#line 149 "EmailLib.c"
3765int __ste_email_encryptionKey1 = 0;
3766#line 151 "EmailLib.c"
3767int getEmailEncryptionKey(int handle )
3768{ int retValue_acc ;
3769
3770 {
3771#line 158 "EmailLib.c"
3772 if (handle == 1) {
3773#line 1208
3774 retValue_acc = __ste_email_encryptionKey0;
3775#line 1210
3776 return (retValue_acc);
3777 } else {
3778#line 1212
3779 if (handle == 2) {
3780#line 1217
3781 retValue_acc = __ste_email_encryptionKey1;
3782#line 1219
3783 return (retValue_acc);
3784 } else {
3785#line 1225 "EmailLib.c"
3786 retValue_acc = 0;
3787#line 1227
3788 return (retValue_acc);
3789 }
3790 }
3791#line 1234 "EmailLib.c"
3792 return (retValue_acc);
3793}
3794}
3795#line 161 "EmailLib.c"
3796void setEmailEncryptionKey(int handle , int value )
3797{
3798
3799 {
3800#line 167
3801 if (handle == 1) {
3802#line 163
3803 __ste_email_encryptionKey0 = value;
3804 } else {
3805#line 164
3806 if (handle == 2) {
3807#line 165
3808 __ste_email_encryptionKey1 = value;
3809 } else {
3810
3811 }
3812 }
3813#line 1265 "EmailLib.c"
3814 return;
3815}
3816}
3817#line 169 "EmailLib.c"
3818int __ste_email_isSigned0 = 0;
3819#line 171 "EmailLib.c"
3820int __ste_email_isSigned1 = 0;
3821#line 173 "EmailLib.c"
3822int isSigned(int handle )
3823{ int retValue_acc ;
3824
3825 {
3826#line 180 "EmailLib.c"
3827 if (handle == 1) {
3828#line 1290
3829 retValue_acc = __ste_email_isSigned0;
3830#line 1292
3831 return (retValue_acc);
3832 } else {
3833#line 1294
3834 if (handle == 2) {
3835#line 1299
3836 retValue_acc = __ste_email_isSigned1;
3837#line 1301
3838 return (retValue_acc);
3839 } else {
3840#line 1307 "EmailLib.c"
3841 retValue_acc = 0;
3842#line 1309
3843 return (retValue_acc);
3844 }
3845 }
3846#line 1316 "EmailLib.c"
3847 return (retValue_acc);
3848}
3849}
3850#line 183 "EmailLib.c"
3851void setEmailIsSigned(int handle , int value )
3852{
3853
3854 {
3855#line 189
3856 if (handle == 1) {
3857#line 185
3858 __ste_email_isSigned0 = value;
3859 } else {
3860#line 186
3861 if (handle == 2) {
3862#line 187
3863 __ste_email_isSigned1 = value;
3864 } else {
3865
3866 }
3867 }
3868#line 1347 "EmailLib.c"
3869 return;
3870}
3871}
3872#line 191 "EmailLib.c"
3873int __ste_email_signKey0 = 0;
3874#line 193 "EmailLib.c"
3875int __ste_email_signKey1 = 0;
3876#line 195 "EmailLib.c"
3877int getEmailSignKey(int handle )
3878{ int retValue_acc ;
3879
3880 {
3881#line 202 "EmailLib.c"
3882 if (handle == 1) {
3883#line 1372
3884 retValue_acc = __ste_email_signKey0;
3885#line 1374
3886 return (retValue_acc);
3887 } else {
3888#line 1376
3889 if (handle == 2) {
3890#line 1381
3891 retValue_acc = __ste_email_signKey1;
3892#line 1383
3893 return (retValue_acc);
3894 } else {
3895#line 1389 "EmailLib.c"
3896 retValue_acc = 0;
3897#line 1391
3898 return (retValue_acc);
3899 }
3900 }
3901#line 1398 "EmailLib.c"
3902 return (retValue_acc);
3903}
3904}
3905#line 205 "EmailLib.c"
3906void setEmailSignKey(int handle , int value )
3907{
3908
3909 {
3910#line 211
3911 if (handle == 1) {
3912#line 207
3913 __ste_email_signKey0 = value;
3914 } else {
3915#line 208
3916 if (handle == 2) {
3917#line 209
3918 __ste_email_signKey1 = value;
3919 } else {
3920
3921 }
3922 }
3923#line 1429 "EmailLib.c"
3924 return;
3925}
3926}
3927#line 213 "EmailLib.c"
3928int __ste_email_isSignatureVerified0 ;
3929#line 215 "EmailLib.c"
3930int __ste_email_isSignatureVerified1 ;
3931#line 217 "EmailLib.c"
3932int isVerified(int handle )
3933{ int retValue_acc ;
3934
3935 {
3936#line 224 "EmailLib.c"
3937 if (handle == 1) {
3938#line 1454
3939 retValue_acc = __ste_email_isSignatureVerified0;
3940#line 1456
3941 return (retValue_acc);
3942 } else {
3943#line 1458
3944 if (handle == 2) {
3945#line 1463
3946 retValue_acc = __ste_email_isSignatureVerified1;
3947#line 1465
3948 return (retValue_acc);
3949 } else {
3950#line 1471 "EmailLib.c"
3951 retValue_acc = 0;
3952#line 1473
3953 return (retValue_acc);
3954 }
3955 }
3956#line 1480 "EmailLib.c"
3957 return (retValue_acc);
3958}
3959}
3960#line 227 "EmailLib.c"
3961void setEmailIsSignatureVerified(int handle , int value )
3962{
3963
3964 {
3965#line 233
3966 if (handle == 1) {
3967#line 229
3968 __ste_email_isSignatureVerified0 = value;
3969 } else {
3970#line 230
3971 if (handle == 2) {
3972#line 231
3973 __ste_email_isSignatureVerified1 = value;
3974 } else {
3975
3976 }
3977 }
3978#line 1511 "EmailLib.c"
3979 return;
3980}
3981}
3982#line 1 "featureselect.o"
3983#pragma merger(0,"featureselect.i","")
3984#line 41 "featureselect.h"
3985int select_one(void) ;
3986#line 8 "featureselect.c"
3987int select_one(void)
3988{ int retValue_acc ;
3989 int choice = __VERIFIER_nondet_int();
3990
3991 {
3992#line 84 "featureselect.c"
3993 retValue_acc = choice;
3994#line 86
3995 return (retValue_acc);
3996#line 93
3997 return (retValue_acc);
3998}
3999}
4000#line 14 "featureselect.c"
4001void select_features(void)
4002{
4003
4004 {
4005#line 115 "featureselect.c"
4006 return;
4007}
4008}
4009#line 20 "featureselect.c"
4010void select_helpers(void)
4011{
4012
4013 {
4014#line 133 "featureselect.c"
4015 return;
4016}
4017}
4018#line 25 "featureselect.c"
4019int valid_product(void)
4020{ int retValue_acc ;
4021
4022 {
4023#line 151 "featureselect.c"
4024 retValue_acc = 1;
4025#line 153
4026 return (retValue_acc);
4027#line 160
4028 return (retValue_acc);
4029}
4030}
4031#line 1 "Email.o"
4032#pragma merger(0,"Email.i","")
4033#line 6 "Email.h"
4034void printMail(int msg ) ;
4035#line 15
4036int cloneEmail(int msg ) ;
4037#line 9 "Email.c"
4038void printMail__wrappee__Keys(int msg )
4039{ int tmp ;
4040 int tmp___0 ;
4041 int tmp___1 ;
4042 int tmp___2 ;
4043 char const * __restrict __cil_tmp6 ;
4044 char const * __restrict __cil_tmp7 ;
4045 char const * __restrict __cil_tmp8 ;
4046 char const * __restrict __cil_tmp9 ;
4047
4048 {
4049 {
4050#line 10
4051 tmp = getEmailId(msg);
4052#line 10
4053 __cil_tmp6 = (char const * __restrict )"ID:\n %i\n";
4054#line 10
4055 printf(__cil_tmp6, tmp);
4056#line 11
4057 tmp___0 = getEmailFrom(msg);
4058#line 11
4059 __cil_tmp7 = (char const * __restrict )"FROM:\n %i\n";
4060#line 11
4061 printf(__cil_tmp7, tmp___0);
4062#line 12
4063 tmp___1 = getEmailTo(msg);
4064#line 12
4065 __cil_tmp8 = (char const * __restrict )"TO:\n %i\n";
4066#line 12
4067 printf(__cil_tmp8, tmp___1);
4068#line 13
4069 tmp___2 = isReadable(msg);
4070#line 13
4071 __cil_tmp9 = (char const * __restrict )"IS_READABLE\n %i\n";
4072#line 13
4073 printf(__cil_tmp9, tmp___2);
4074 }
4075#line 601 "Email.c"
4076 return;
4077}
4078}
4079#line 17 "Email.c"
4080void printMail__wrappee__AddressBook(int msg )
4081{ int tmp ;
4082 int tmp___0 ;
4083 char const * __restrict __cil_tmp4 ;
4084 char const * __restrict __cil_tmp5 ;
4085
4086 {
4087 {
4088#line 18
4089 printMail__wrappee__Keys(msg);
4090#line 19
4091 tmp = isEncrypted(msg);
4092#line 19
4093 __cil_tmp4 = (char const * __restrict )"ENCRYPTED\n %d\n";
4094#line 19
4095 printf(__cil_tmp4, tmp);
4096#line 20
4097 tmp___0 = getEmailEncryptionKey(msg);
4098#line 20
4099 __cil_tmp5 = (char const * __restrict )"ENCRYPTION KEY\n %d\n";
4100#line 20
4101 printf(__cil_tmp5, tmp___0);
4102 }
4103#line 625 "Email.c"
4104 return;
4105}
4106}
4107#line 26 "Email.c"
4108void printMail__wrappee__Sign(int msg )
4109{ int tmp ;
4110 int tmp___0 ;
4111 char const * __restrict __cil_tmp4 ;
4112 char const * __restrict __cil_tmp5 ;
4113
4114 {
4115 {
4116#line 27
4117 printMail__wrappee__AddressBook(msg);
4118#line 28
4119 tmp = isSigned(msg);
4120#line 28
4121 __cil_tmp4 = (char const * __restrict )"SIGNED\n %i\n";
4122#line 28
4123 printf(__cil_tmp4, tmp);
4124#line 29
4125 tmp___0 = getEmailSignKey(msg);
4126#line 29
4127 __cil_tmp5 = (char const * __restrict )"SIGNATURE\n %i\n";
4128#line 29
4129 printf(__cil_tmp5, tmp___0);
4130 }
4131#line 649 "Email.c"
4132 return;
4133}
4134}
4135#line 33 "Email.c"
4136void printMail(int msg )
4137{ int tmp ;
4138 char const * __restrict __cil_tmp3 ;
4139
4140 {
4141 {
4142#line 34
4143 printMail__wrappee__Sign(msg);
4144#line 35
4145 tmp = isVerified(msg);
4146#line 35
4147 __cil_tmp3 = (char const * __restrict )"SIGNATURE VERIFIED\n %d\n";
4148#line 35
4149 printf(__cil_tmp3, tmp);
4150 }
4151#line 671 "Email.c"
4152 return;
4153}
4154}
4155#line 41 "Email.c"
4156int isReadable__wrappee__Keys(int msg )
4157{ int retValue_acc ;
4158
4159 {
4160#line 689 "Email.c"
4161 retValue_acc = 1;
4162#line 691
4163 return (retValue_acc);
4164#line 698
4165 return (retValue_acc);
4166}
4167}
4168#line 49 "Email.c"
4169int isReadable(int msg )
4170{ int retValue_acc ;
4171 int tmp ;
4172
4173 {
4174 {
4175#line 53
4176 tmp = isEncrypted(msg);
4177 }
4178#line 53 "Email.c"
4179 if (tmp) {
4180#line 727
4181 retValue_acc = 0;
4182#line 729
4183 return (retValue_acc);
4184 } else {
4185 {
4186#line 721 "Email.c"
4187 retValue_acc = isReadable__wrappee__Keys(msg);
4188 }
4189#line 723
4190 return (retValue_acc);
4191 }
4192#line 736 "Email.c"
4193 return (retValue_acc);
4194}
4195}
4196#line 57 "Email.c"
4197int cloneEmail(int msg )
4198{ int retValue_acc ;
4199
4200 {
4201#line 758 "Email.c"
4202 retValue_acc = msg;
4203#line 760
4204 return (retValue_acc);
4205#line 767
4206 return (retValue_acc);
4207}
4208}
4209#line 62 "Email.c"
4210int createEmail(int from , int to )
4211{ int retValue_acc ;
4212 int msg ;
4213
4214 {
4215 {
4216#line 63
4217 msg = 1;
4218#line 64
4219 setEmailFrom(msg, from);
4220#line 65
4221 setEmailTo(msg, to);
4222#line 797 "Email.c"
4223 retValue_acc = msg;
4224 }
4225#line 799
4226 return (retValue_acc);
4227#line 806
4228 return (retValue_acc);
4229}
4230}
4231#line 1 "scenario.o"
4232#pragma merger(0,"scenario.i","")
4233#line 1 "scenario.c"
4234void test(void)
4235{ int op1 ;
4236 int op2 ;
4237 int op3 ;
4238 int op4 ;
4239 int op5 ;
4240 int op6 ;
4241 int op7 ;
4242 int op8 ;
4243 int op9 ;
4244 int op10 ;
4245 int op11 ;
4246 int splverifierCounter ;
4247 int tmp ;
4248 int tmp___0 ;
4249 int tmp___1 ;
4250 int tmp___2 ;
4251 int tmp___3 ;
4252 int tmp___4 ;
4253 int tmp___5 ;
4254 int tmp___6 ;
4255 int tmp___7 ;
4256 int tmp___8 ;
4257 int tmp___9 ;
4258
4259 {
4260#line 2
4261 op1 = 0;
4262#line 3
4263 op2 = 0;
4264#line 4
4265 op3 = 0;
4266#line 5
4267 op4 = 0;
4268#line 6
4269 op5 = 0;
4270#line 7
4271 op6 = 0;
4272#line 8
4273 op7 = 0;
4274#line 9
4275 op8 = 0;
4276#line 10
4277 op9 = 0;
4278#line 11
4279 op10 = 0;
4280#line 12
4281 op11 = 0;
4282#line 13
4283 splverifierCounter = 0;
4284 {
4285#line 14
4286 while (1) {
4287 while_3_continue: ;
4288#line 14
4289 if (splverifierCounter < 4) {
4290
4291 } else {
4292 goto while_3_break;
4293 }
4294#line 15
4295 splverifierCounter = splverifierCounter + 1;
4296#line 16
4297 if (! op1) {
4298 {
4299#line 16
4300 tmp___9 = __VERIFIER_nondet_int();
4301 }
4302#line 16
4303 if (tmp___9) {
4304 {
4305#line 17
4306 bobKeyAdd();
4307#line 18
4308 op1 = 1;
4309 }
4310 } else {
4311 goto _L___8;
4312 }
4313 } else {
4314 _L___8:
4315#line 19
4316 if (! op2) {
4317 {
4318#line 19
4319 tmp___8 = __VERIFIER_nondet_int();
4320 }
4321#line 19
4322 if (tmp___8) {
4323 {
4324#line 21
4325 rjhSetAutoRespond();
4326#line 22
4327 op2 = 1;
4328 }
4329 } else {
4330 goto _L___7;
4331 }
4332 } else {
4333 _L___7:
4334#line 23
4335 if (! op3) {
4336 {
4337#line 23
4338 tmp___7 = __VERIFIER_nondet_int();
4339 }
4340#line 23
4341 if (tmp___7) {
4342 {
4343#line 25
4344 rjhDeletePrivateKey();
4345#line 26
4346 op3 = 1;
4347 }
4348 } else {
4349 goto _L___6;
4350 }
4351 } else {
4352 _L___6:
4353#line 27
4354 if (! op4) {
4355 {
4356#line 27
4357 tmp___6 = __VERIFIER_nondet_int();
4358 }
4359#line 27
4360 if (tmp___6) {
4361 {
4362#line 29
4363 rjhKeyAdd();
4364#line 30
4365 op4 = 1;
4366 }
4367 } else {
4368 goto _L___5;
4369 }
4370 } else {
4371 _L___5:
4372#line 31
4373 if (! op5) {
4374 {
4375#line 31
4376 tmp___5 = __VERIFIER_nondet_int();
4377 }
4378#line 31
4379 if (tmp___5) {
4380 {
4381#line 33
4382 chuckKeyAddRjh();
4383#line 34
4384 op5 = 1;
4385 }
4386 } else {
4387 goto _L___4;
4388 }
4389 } else {
4390 _L___4:
4391#line 35
4392 if (! op6) {
4393 {
4394#line 35
4395 tmp___4 = __VERIFIER_nondet_int();
4396 }
4397#line 35
4398 if (tmp___4) {
4399#line 37
4400 op6 = 1;
4401 } else {
4402 goto _L___3;
4403 }
4404 } else {
4405 _L___3:
4406#line 38
4407 if (! op7) {
4408 {
4409#line 38
4410 tmp___3 = __VERIFIER_nondet_int();
4411 }
4412#line 38
4413 if (tmp___3) {
4414 {
4415#line 40
4416 rjhKeyChange();
4417#line 41
4418 op7 = 1;
4419 }
4420 } else {
4421 goto _L___2;
4422 }
4423 } else {
4424 _L___2:
4425#line 42
4426 if (! op8) {
4427 {
4428#line 42
4429 tmp___2 = __VERIFIER_nondet_int();
4430 }
4431#line 42
4432 if (tmp___2) {
4433 {
4434#line 44
4435 bobSetAddressBook();
4436#line 45
4437 op8 = 1;
4438 }
4439 } else {
4440 goto _L___1;
4441 }
4442 } else {
4443 _L___1:
4444#line 46
4445 if (! op9) {
4446 {
4447#line 46
4448 tmp___1 = __VERIFIER_nondet_int();
4449 }
4450#line 46
4451 if (tmp___1) {
4452 {
4453#line 48
4454 chuckKeyAdd();
4455#line 49
4456 op9 = 1;
4457 }
4458 } else {
4459 goto _L___0;
4460 }
4461 } else {
4462 _L___0:
4463#line 50
4464 if (! op10) {
4465 {
4466#line 50
4467 tmp___0 = __VERIFIER_nondet_int();
4468 }
4469#line 50
4470 if (tmp___0) {
4471 {
4472#line 52
4473 bobKeyChange();
4474#line 53
4475 op10 = 1;
4476 }
4477 } else {
4478 goto _L;
4479 }
4480 } else {
4481 _L:
4482#line 54
4483 if (! op11) {
4484 {
4485#line 54
4486 tmp = __VERIFIER_nondet_int();
4487 }
4488#line 54
4489 if (tmp) {
4490 {
4491#line 56
4492 chuckKeyAdd();
4493#line 57
4494 op11 = 1;
4495 }
4496 } else {
4497 goto while_3_break;
4498 }
4499 } else {
4500 goto while_3_break;
4501 }
4502 }
4503 }
4504 }
4505 }
4506 }
4507 }
4508 }
4509 }
4510 }
4511 }
4512 }
4513 while_3_break: ;
4514 }
4515 {
4516#line 61
4517 bobToRjh();
4518 }
4519#line 169 "scenario.c"
4520 return;
4521}
4522}