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