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