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