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