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