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 "wsllib_check.o"
2331#pragma merger(0,"wsllib_check.i","")
2332#line 3 "wsllib_check.c"
2333void __automaton_fail(void)
2334{
2335
2336 {
2337 goto ERROR;
2338 ERROR: ;
2339#line 53 "wsllib_check.c"
2340 return;
2341}
2342}
2343#line 1 "Email.o"
2344#pragma merger(0,"Email.i","")
2345#line 359 "/usr/include/stdio.h"
2346extern int printf(char const * __restrict __format , ...) ;
2347#line 8 "featureselect.h"
2348int __SELECTED_FEATURE_Base ;
2349#line 11 "featureselect.h"
2350int __SELECTED_FEATURE_Keys ;
2351#line 14 "featureselect.h"
2352int __SELECTED_FEATURE_Encrypt ;
2353#line 17 "featureselect.h"
2354int __SELECTED_FEATURE_AutoResponder ;
2355#line 20 "featureselect.h"
2356int __SELECTED_FEATURE_AddressBook ;
2357#line 23 "featureselect.h"
2358int __SELECTED_FEATURE_Sign ;
2359#line 26 "featureselect.h"
2360int __SELECTED_FEATURE_Forward ;
2361#line 29 "featureselect.h"
2362int __SELECTED_FEATURE_Verify ;
2363#line 32 "featureselect.h"
2364int __SELECTED_FEATURE_Decrypt ;
2365#line 35 "featureselect.h"
2366int __GUIDSL_ROOT_PRODUCTION ;
2367#line 37 "featureselect.h"
2368int __GUIDSL_NON_TERMINAL_main ;
2369#line 6 "Email.h"
2370void printMail(int msg ) ;
2371#line 9
2372int isReadable(int msg ) ;
2373#line 12
2374int createEmail(int from , int to ) ;
2375#line 15
2376int cloneEmail(int msg ) ;
2377#line 9 "Email.c"
2378void printMail__wrappee__Keys(int msg )
2379{ int tmp ;
2380 int tmp___0 ;
2381 int tmp___1 ;
2382 int tmp___2 ;
2383 char const * __restrict __cil_tmp6 ;
2384 char const * __restrict __cil_tmp7 ;
2385 char const * __restrict __cil_tmp8 ;
2386 char const * __restrict __cil_tmp9 ;
2387
2388 {
2389 {
2390#line 10
2391 tmp = getEmailId(msg);
2392#line 10
2393 __cil_tmp6 = (char const * __restrict )"ID:\n %i\n";
2394#line 10
2395 printf(__cil_tmp6, tmp);
2396#line 11
2397 tmp___0 = getEmailFrom(msg);
2398#line 11
2399 __cil_tmp7 = (char const * __restrict )"FROM:\n %i\n";
2400#line 11
2401 printf(__cil_tmp7, tmp___0);
2402#line 12
2403 tmp___1 = getEmailTo(msg);
2404#line 12
2405 __cil_tmp8 = (char const * __restrict )"TO:\n %i\n";
2406#line 12
2407 printf(__cil_tmp8, tmp___1);
2408#line 13
2409 tmp___2 = isReadable(msg);
2410#line 13
2411 __cil_tmp9 = (char const * __restrict )"IS_READABLE\n %i\n";
2412#line 13
2413 printf(__cil_tmp9, tmp___2);
2414 }
2415#line 601 "Email.c"
2416 return;
2417}
2418}
2419#line 17 "Email.c"
2420void printMail(int msg )
2421{ int tmp ;
2422 int tmp___0 ;
2423 char const * __restrict __cil_tmp4 ;
2424 char const * __restrict __cil_tmp5 ;
2425
2426 {
2427 {
2428#line 18
2429 printMail__wrappee__Keys(msg);
2430#line 19
2431 tmp = isEncrypted(msg);
2432#line 19
2433 __cil_tmp4 = (char const * __restrict )"ENCRYPTED\n %d\n";
2434#line 19
2435 printf(__cil_tmp4, tmp);
2436#line 20
2437 tmp___0 = getEmailEncryptionKey(msg);
2438#line 20
2439 __cil_tmp5 = (char const * __restrict )"ENCRYPTION KEY\n %d\n";
2440#line 20
2441 printf(__cil_tmp5, tmp___0);
2442 }
2443#line 625 "Email.c"
2444 return;
2445}
2446}
2447#line 26 "Email.c"
2448int isReadable__wrappee__Keys(int msg )
2449{ int retValue_acc ;
2450
2451 {
2452#line 643 "Email.c"
2453 retValue_acc = 1;
2454#line 645
2455 return (retValue_acc);
2456#line 652
2457 return (retValue_acc);
2458}
2459}
2460#line 34 "Email.c"
2461int isReadable(int msg )
2462{ int retValue_acc ;
2463 int tmp ;
2464
2465 {
2466 {
2467#line 38
2468 tmp = isEncrypted(msg);
2469 }
2470#line 38 "Email.c"
2471 if (tmp) {
2472#line 681
2473 retValue_acc = 0;
2474#line 683
2475 return (retValue_acc);
2476 } else {
2477 {
2478#line 675 "Email.c"
2479 retValue_acc = isReadable__wrappee__Keys(msg);
2480 }
2481#line 677
2482 return (retValue_acc);
2483 }
2484#line 690 "Email.c"
2485 return (retValue_acc);
2486}
2487}
2488#line 42 "Email.c"
2489int cloneEmail(int msg )
2490{ int retValue_acc ;
2491
2492 {
2493#line 712 "Email.c"
2494 retValue_acc = msg;
2495#line 714
2496 return (retValue_acc);
2497#line 721
2498 return (retValue_acc);
2499}
2500}
2501#line 47 "Email.c"
2502int createEmail(int from , int to )
2503{ int retValue_acc ;
2504 int msg ;
2505
2506 {
2507 {
2508#line 48
2509 msg = 1;
2510#line 49
2511 setEmailFrom(msg, from);
2512#line 50
2513 setEmailTo(msg, to);
2514#line 751 "Email.c"
2515 retValue_acc = msg;
2516 }
2517#line 753
2518 return (retValue_acc);
2519#line 760
2520 return (retValue_acc);
2521}
2522}
2523#line 1 "scenario.o"
2524#pragma merger(0,"scenario.i","")
2525#line 17 "scenario.c"
2526void bobKeyAdd(void) ;
2527#line 21
2528void rjhSetAutoRespond(void) ;
2529#line 25
2530void rjhDeletePrivateKey(void) ;
2531#line 29
2532void rjhKeyAdd(void) ;
2533#line 33
2534void chuckKeyAddRjh(void) ;
2535#line 40
2536void rjhKeyChange(void) ;
2537#line 47
2538void chuckKeyAdd(void) ;
2539#line 51
2540void bobKeyChange(void) ;
2541#line 53
2542#line 60
2543void bobToRjh(void) ;
2544#line 1 "scenario.c"
2545void test(void)
2546{ int op1 ;
2547 int op2 ;
2548 int op3 ;
2549 int op4 ;
2550 int op5 ;
2551 int op6 ;
2552 int op7 ;
2553 int op8 ;
2554 int op9 ;
2555 int op10 ;
2556 int op11 ;
2557 int splverifierCounter ;
2558 int tmp ;
2559 int tmp___0 ;
2560 int tmp___1 ;
2561 int tmp___2 ;
2562 int tmp___3 ;
2563 int tmp___4 ;
2564 int tmp___5 ;
2565 int tmp___6 ;
2566 int tmp___7 ;
2567 int tmp___8 ;
2568 int tmp___9 ;
2569
2570 {
2571#line 2
2572 op1 = 0;
2573#line 3
2574 op2 = 0;
2575#line 4
2576 op3 = 0;
2577#line 5
2578 op4 = 0;
2579#line 6
2580 op5 = 0;
2581#line 7
2582 op6 = 0;
2583#line 8
2584 op7 = 0;
2585#line 9
2586 op8 = 0;
2587#line 10
2588 op9 = 0;
2589#line 11
2590 op10 = 0;
2591#line 12
2592 op11 = 0;
2593#line 13
2594 splverifierCounter = 0;
2595 {
2596#line 14
2597 while (1) {
2598 while_0_continue: ;
2599#line 14
2600 if (splverifierCounter < 4) {
2601
2602 } else {
2603 goto while_0_break;
2604 }
2605#line 15
2606 splverifierCounter = splverifierCounter + 1;
2607#line 16
2608 if (! op1) {
2609 {
2610#line 16
2611 tmp___9 = __VERIFIER_nondet_int();
2612 }
2613#line 16
2614 if (tmp___9) {
2615 {
2616#line 17
2617 bobKeyAdd();
2618#line 18
2619 op1 = 1;
2620 }
2621 } else {
2622 goto _L___8;
2623 }
2624 } else {
2625 _L___8:
2626#line 19
2627 if (! op2) {
2628 {
2629#line 19
2630 tmp___8 = __VERIFIER_nondet_int();
2631 }
2632#line 19
2633 if (tmp___8) {
2634 {
2635#line 21
2636 rjhSetAutoRespond();
2637#line 22
2638 op2 = 1;
2639 }
2640 } else {
2641 goto _L___7;
2642 }
2643 } else {
2644 _L___7:
2645#line 23
2646 if (! op3) {
2647 {
2648#line 23
2649 tmp___7 = __VERIFIER_nondet_int();
2650 }
2651#line 23
2652 if (tmp___7) {
2653 {
2654#line 25
2655 rjhDeletePrivateKey();
2656#line 26
2657 op3 = 1;
2658 }
2659 } else {
2660 goto _L___6;
2661 }
2662 } else {
2663 _L___6:
2664#line 27
2665 if (! op4) {
2666 {
2667#line 27
2668 tmp___6 = __VERIFIER_nondet_int();
2669 }
2670#line 27
2671 if (tmp___6) {
2672 {
2673#line 29
2674 rjhKeyAdd();
2675#line 30
2676 op4 = 1;
2677 }
2678 } else {
2679 goto _L___5;
2680 }
2681 } else {
2682 _L___5:
2683#line 31
2684 if (! op5) {
2685 {
2686#line 31
2687 tmp___5 = __VERIFIER_nondet_int();
2688 }
2689#line 31
2690 if (tmp___5) {
2691 {
2692#line 33
2693 chuckKeyAddRjh();
2694#line 34
2695 op5 = 1;
2696 }
2697 } else {
2698 goto _L___4;
2699 }
2700 } else {
2701 _L___4:
2702#line 35
2703 if (! op6) {
2704 {
2705#line 35
2706 tmp___4 = __VERIFIER_nondet_int();
2707 }
2708#line 35
2709 if (tmp___4) {
2710#line 37
2711 op6 = 1;
2712 } else {
2713 goto _L___3;
2714 }
2715 } else {
2716 _L___3:
2717#line 38
2718 if (! op7) {
2719 {
2720#line 38
2721 tmp___3 = __VERIFIER_nondet_int();
2722 }
2723#line 38
2724 if (tmp___3) {
2725 {
2726#line 40
2727 rjhKeyChange();
2728#line 41
2729 op7 = 1;
2730 }
2731 } else {
2732 goto _L___2;
2733 }
2734 } else {
2735 _L___2:
2736#line 42
2737 if (! op8) {
2738 {
2739#line 42
2740 tmp___2 = __VERIFIER_nondet_int();
2741 }
2742#line 42
2743 if (tmp___2) {
2744#line 44
2745 op8 = 1;
2746 } else {
2747 goto _L___1;
2748 }
2749 } else {
2750 _L___1:
2751#line 45
2752 if (! op9) {
2753 {
2754#line 45
2755 tmp___1 = __VERIFIER_nondet_int();
2756 }
2757#line 45
2758 if (tmp___1) {
2759 {
2760#line 47
2761 chuckKeyAdd();
2762#line 48
2763 op9 = 1;
2764 }
2765 } else {
2766 goto _L___0;
2767 }
2768 } else {
2769 _L___0:
2770#line 49
2771 if (! op10) {
2772 {
2773#line 49
2774 tmp___0 = __VERIFIER_nondet_int();
2775 }
2776#line 49
2777 if (tmp___0) {
2778 {
2779#line 51
2780 bobKeyChange();
2781#line 52
2782 op10 = 1;
2783 }
2784 } else {
2785 goto _L;
2786 }
2787 } else {
2788 _L:
2789#line 53
2790 if (! op11) {
2791 {
2792#line 53
2793 tmp = __VERIFIER_nondet_int();
2794 }
2795#line 53
2796 if (tmp) {
2797 {
2798#line 55
2799 chuckKeyAdd();
2800#line 56
2801 op11 = 1;
2802 }
2803 } else {
2804 goto while_0_break;
2805 }
2806 } else {
2807 goto while_0_break;
2808 }
2809 }
2810 }
2811 }
2812 }
2813 }
2814 }
2815 }
2816 }
2817 }
2818 }
2819 }
2820 while_0_break: ;
2821 }
2822 {
2823#line 60
2824 bobToRjh();
2825 }
2826#line 167 "scenario.c"
2827 return;
2828}
2829}
2830#line 1 "Test.o"
2831#pragma merger(0,"Test.i","")
2832#line 688 "/usr/include/stdio.h"
2833extern int puts(char const *__s ) ;
2834#line 43 "featureselect.h"
2835void select_features(void) ;
2836#line 45
2837void select_helpers(void) ;
2838#line 47
2839int valid_product(void) ;
2840#line 17 "Client.h"
2841int is_queue_empty(void) ;
2842#line 19
2843int get_queued_client(void) ;
2844#line 21
2845int get_queued_email(void) ;
2846#line 26
2847void outgoing(int client , int msg ) ;
2848#line 35
2849void sendEmail(int sender , int receiver ) ;
2850#line 44
2851void generateKeyPair(int client , int seed ) ;
2852#line 2 "Test.h"
2853int bob ;
2854#line 5 "Test.h"
2855int rjh ;
2856#line 8 "Test.h"
2857int chuck ;
2858#line 11
2859void setup_bob(int bob___0 ) ;
2860#line 14
2861void setup_rjh(int rjh___0 ) ;
2862#line 17
2863void setup_chuck(int chuck___0 ) ;
2864#line 26
2865void rjhToBob(void) ;
2866#line 32
2867void setup(void) ;
2868#line 35
2869int main(void) ;
2870#line 39
2871void bobKeyAddChuck(void) ;
2872#line 45
2873void rjhKeyAddChuck(void) ;
2874#line 18 "Test.c"
2875void setup_bob__wrappee__Base(int bob___0 )
2876{
2877
2878 {
2879 {
2880#line 19
2881 setClientId(bob___0, bob___0);
2882 }
2883#line 1326 "Test.c"
2884 return;
2885}
2886}
2887#line 23 "Test.c"
2888void setup_bob(int bob___0 )
2889{
2890
2891 {
2892 {
2893#line 24
2894 setup_bob__wrappee__Base(bob___0);
2895#line 25
2896 setClientPrivateKey(bob___0, 123);
2897 }
2898#line 1348 "Test.c"
2899 return;
2900}
2901}
2902#line 33 "Test.c"
2903void setup_rjh__wrappee__Base(int rjh___0 )
2904{
2905
2906 {
2907 {
2908#line 34
2909 setClientId(rjh___0, rjh___0);
2910 }
2911#line 1368 "Test.c"
2912 return;
2913}
2914}
2915#line 40 "Test.c"
2916void setup_rjh(int rjh___0 )
2917{
2918
2919 {
2920 {
2921#line 42
2922 setup_rjh__wrappee__Base(rjh___0);
2923#line 43
2924 setClientPrivateKey(rjh___0, 456);
2925 }
2926#line 1390 "Test.c"
2927 return;
2928}
2929}
2930#line 50 "Test.c"
2931void setup_chuck__wrappee__Base(int chuck___0 )
2932{
2933
2934 {
2935 {
2936#line 51
2937 setClientId(chuck___0, chuck___0);
2938 }
2939#line 1410 "Test.c"
2940 return;
2941}
2942}
2943#line 57 "Test.c"
2944void setup_chuck(int chuck___0 )
2945{
2946
2947 {
2948 {
2949#line 58
2950 setup_chuck__wrappee__Base(chuck___0);
2951#line 59
2952 setClientPrivateKey(chuck___0, 789);
2953 }
2954#line 1432 "Test.c"
2955 return;
2956}
2957}
2958#line 69 "Test.c"
2959void bobToRjh(void)
2960{ int tmp ;
2961 int tmp___0 ;
2962 int tmp___1 ;
2963
2964 {
2965 {
2966#line 71
2967 puts("Please enter a subject and a message body.\n");
2968#line 72
2969 sendEmail(bob, rjh);
2970#line 73
2971 tmp___1 = is_queue_empty();
2972 }
2973#line 73
2974 if (tmp___1) {
2975
2976 } else {
2977 {
2978#line 74
2979 tmp = get_queued_email();
2980#line 74
2981 tmp___0 = get_queued_client();
2982#line 74
2983 outgoing(tmp___0, tmp);
2984 }
2985 }
2986#line 1459 "Test.c"
2987 return;
2988}
2989}
2990#line 81 "Test.c"
2991void rjhToBob(void)
2992{
2993
2994 {
2995 {
2996#line 83
2997 puts("Please enter a subject and a message body.\n");
2998#line 84
2999 sendEmail(rjh, bob);
3000 }
3001#line 1481 "Test.c"
3002 return;
3003}
3004}
3005#line 88 "Test.c"
3006#line 95 "Test.c"
3007void setup(void)
3008{ char const * __restrict __cil_tmp1 ;
3009 char const * __restrict __cil_tmp2 ;
3010 char const * __restrict __cil_tmp3 ;
3011
3012 {
3013 {
3014#line 96
3015 bob = 1;
3016#line 97
3017 setup_bob(bob);
3018#line 98
3019 __cil_tmp1 = (char const * __restrict )"bob: %d\n";
3020#line 98
3021 printf(__cil_tmp1, bob);
3022#line 100
3023 rjh = 2;
3024#line 101
3025 setup_rjh(rjh);
3026#line 102
3027 __cil_tmp2 = (char const * __restrict )"rjh: %d\n";
3028#line 102
3029 printf(__cil_tmp2, rjh);
3030#line 104
3031 chuck = 3;
3032#line 105
3033 setup_chuck(chuck);
3034#line 106
3035 __cil_tmp3 = (char const * __restrict )"chuck: %d\n";
3036#line 106
3037 printf(__cil_tmp3, chuck);
3038 }
3039#line 1552 "Test.c"
3040 return;
3041}
3042}
3043#line 112 "Test.c"
3044int main(void)
3045{ int retValue_acc ;
3046 int tmp ;
3047
3048 {
3049 {
3050#line 113
3051 select_helpers();
3052#line 114
3053 select_features();
3054#line 115
3055 tmp = valid_product();
3056 }
3057#line 115
3058 if (tmp) {
3059 {
3060#line 116
3061 setup();
3062#line 117
3063 test();
3064 }
3065 } else {
3066
3067 }
3068#line 1583 "Test.c"
3069 return (retValue_acc);
3070}
3071}
3072#line 125 "Test.c"
3073void bobKeyAdd(void)
3074{ int tmp ;
3075 int tmp___0 ;
3076 char const * __restrict __cil_tmp3 ;
3077 char const * __restrict __cil_tmp4 ;
3078
3079 {
3080 {
3081#line 126
3082 createClientKeyringEntry(bob);
3083#line 127
3084 setClientKeyringUser(bob, 0, 2);
3085#line 128
3086 setClientKeyringPublicKey(bob, 0, 456);
3087#line 129
3088 puts("bob added rjhs key");
3089#line 130
3090 tmp = getClientKeyringUser(bob, 0);
3091#line 130
3092 __cil_tmp3 = (char const * __restrict )"%d\n";
3093#line 130
3094 printf(__cil_tmp3, tmp);
3095#line 131
3096 tmp___0 = getClientKeyringPublicKey(bob, 0);
3097#line 131
3098 __cil_tmp4 = (char const * __restrict )"%d\n";
3099#line 131
3100 printf(__cil_tmp4, tmp___0);
3101 }
3102#line 1617 "Test.c"
3103 return;
3104}
3105}
3106#line 137 "Test.c"
3107void rjhKeyAdd(void)
3108{
3109
3110 {
3111 {
3112#line 138
3113 createClientKeyringEntry(rjh);
3114#line 139
3115 setClientKeyringUser(rjh, 0, 1);
3116#line 140
3117 setClientKeyringPublicKey(rjh, 0, 123);
3118 }
3119#line 1641 "Test.c"
3120 return;
3121}
3122}
3123#line 146 "Test.c"
3124void rjhKeyAddChuck(void)
3125{
3126
3127 {
3128 {
3129#line 147
3130 createClientKeyringEntry(rjh);
3131#line 148
3132 setClientKeyringUser(rjh, 0, 3);
3133#line 149
3134 setClientKeyringPublicKey(rjh, 0, 789);
3135 }
3136#line 1665 "Test.c"
3137 return;
3138}
3139}
3140#line 156 "Test.c"
3141void bobKeyAddChuck(void)
3142{
3143
3144 {
3145 {
3146#line 157
3147 createClientKeyringEntry(bob);
3148#line 158
3149 setClientKeyringUser(bob, 1, 3);
3150#line 159
3151 setClientKeyringPublicKey(bob, 1, 789);
3152 }
3153#line 1689 "Test.c"
3154 return;
3155}
3156}
3157#line 165 "Test.c"
3158void chuckKeyAdd(void)
3159{
3160
3161 {
3162 {
3163#line 166
3164 createClientKeyringEntry(chuck);
3165#line 167
3166 setClientKeyringUser(chuck, 0, 1);
3167#line 168
3168 setClientKeyringPublicKey(chuck, 0, 123);
3169 }
3170#line 1713 "Test.c"
3171 return;
3172}
3173}
3174#line 174 "Test.c"
3175void chuckKeyAddRjh(void)
3176{
3177
3178 {
3179 {
3180#line 175
3181 createClientKeyringEntry(chuck);
3182#line 176
3183 setClientKeyringUser(chuck, 0, 2);
3184#line 177
3185 setClientKeyringPublicKey(chuck, 0, 456);
3186 }
3187#line 1737 "Test.c"
3188 return;
3189}
3190}
3191#line 183 "Test.c"
3192void rjhDeletePrivateKey(void)
3193{
3194
3195 {
3196 {
3197#line 184
3198 setClientPrivateKey(rjh, 0);
3199 }
3200#line 1757 "Test.c"
3201 return;
3202}
3203}
3204#line 190 "Test.c"
3205void bobKeyChange(void)
3206{
3207
3208 {
3209 {
3210#line 191
3211 generateKeyPair(bob, 777);
3212 }
3213#line 1777 "Test.c"
3214 return;
3215}
3216}
3217#line 197 "Test.c"
3218void rjhKeyChange(void)
3219{
3220
3221 {
3222 {
3223#line 198
3224 generateKeyPair(rjh, 666);
3225 }
3226#line 1797 "Test.c"
3227 return;
3228}
3229}
3230#line 204 "Test.c"
3231void rjhSetAutoRespond(void)
3232{
3233
3234 {
3235 {
3236#line 205
3237 setClientAutoResponse(rjh, 1);
3238 }
3239#line 1817 "Test.c"
3240 return;
3241}
3242}
3243#line 1 "libacc.o"
3244#pragma merger(0,"libacc.i","")
3245#line 73 "/usr/include/assert.h"
3246extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
3247 char const *__file ,
3248 unsigned int __line ,
3249 char const *__function ) ;
3250#line 471 "/usr/include/stdlib.h"
3251extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
3252#line 488
3253extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
3254#line 32 "libacc.c"
3255void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
3256 int ) ,
3257 int val )
3258{ struct __UTAC__EXCEPTION *excep ;
3259 struct __UTAC__CFLOW_FUNC *cf ;
3260 void *tmp ;
3261 unsigned long __cil_tmp7 ;
3262 unsigned long __cil_tmp8 ;
3263 unsigned long __cil_tmp9 ;
3264 unsigned long __cil_tmp10 ;
3265 unsigned long __cil_tmp11 ;
3266 unsigned long __cil_tmp12 ;
3267 unsigned long __cil_tmp13 ;
3268 unsigned long __cil_tmp14 ;
3269 int (**mem_15)(int , int ) ;
3270 int *mem_16 ;
3271 struct __UTAC__CFLOW_FUNC **mem_17 ;
3272 struct __UTAC__CFLOW_FUNC **mem_18 ;
3273 struct __UTAC__CFLOW_FUNC **mem_19 ;
3274
3275 {
3276 {
3277#line 33
3278 excep = (struct __UTAC__EXCEPTION *)exception;
3279#line 34
3280 tmp = malloc(24UL);
3281#line 34
3282 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
3283#line 36
3284 mem_15 = (int (**)(int , int ))cf;
3285#line 36
3286 *mem_15 = cflow_func;
3287#line 37
3288 __cil_tmp7 = (unsigned long )cf;
3289#line 37
3290 __cil_tmp8 = __cil_tmp7 + 8;
3291#line 37
3292 mem_16 = (int *)__cil_tmp8;
3293#line 37
3294 *mem_16 = val;
3295#line 38
3296 __cil_tmp9 = (unsigned long )cf;
3297#line 38
3298 __cil_tmp10 = __cil_tmp9 + 16;
3299#line 38
3300 __cil_tmp11 = (unsigned long )excep;
3301#line 38
3302 __cil_tmp12 = __cil_tmp11 + 24;
3303#line 38
3304 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
3305#line 38
3306 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
3307#line 38
3308 *mem_17 = *mem_18;
3309#line 39
3310 __cil_tmp13 = (unsigned long )excep;
3311#line 39
3312 __cil_tmp14 = __cil_tmp13 + 24;
3313#line 39
3314 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
3315#line 39
3316 *mem_19 = cf;
3317 }
3318#line 654 "libacc.c"
3319 return;
3320}
3321}
3322#line 44 "libacc.c"
3323void __utac__exception__cf_handler_free(void *exception )
3324{ struct __UTAC__EXCEPTION *excep ;
3325 struct __UTAC__CFLOW_FUNC *cf ;
3326 struct __UTAC__CFLOW_FUNC *tmp ;
3327 unsigned long __cil_tmp5 ;
3328 unsigned long __cil_tmp6 ;
3329 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
3330 unsigned long __cil_tmp8 ;
3331 unsigned long __cil_tmp9 ;
3332 unsigned long __cil_tmp10 ;
3333 unsigned long __cil_tmp11 ;
3334 void *__cil_tmp12 ;
3335 unsigned long __cil_tmp13 ;
3336 unsigned long __cil_tmp14 ;
3337 struct __UTAC__CFLOW_FUNC **mem_15 ;
3338 struct __UTAC__CFLOW_FUNC **mem_16 ;
3339 struct __UTAC__CFLOW_FUNC **mem_17 ;
3340
3341 {
3342#line 45
3343 excep = (struct __UTAC__EXCEPTION *)exception;
3344#line 46
3345 __cil_tmp5 = (unsigned long )excep;
3346#line 46
3347 __cil_tmp6 = __cil_tmp5 + 24;
3348#line 46
3349 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
3350#line 46
3351 cf = *mem_15;
3352 {
3353#line 49
3354 while (1) {
3355 while_1_continue: ;
3356 {
3357#line 49
3358 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
3359#line 49
3360 __cil_tmp8 = (unsigned long )__cil_tmp7;
3361#line 49
3362 __cil_tmp9 = (unsigned long )cf;
3363#line 49
3364 if (__cil_tmp9 != __cil_tmp8) {
3365
3366 } else {
3367 goto while_1_break;
3368 }
3369 }
3370 {
3371#line 50
3372 tmp = cf;
3373#line 51
3374 __cil_tmp10 = (unsigned long )cf;
3375#line 51
3376 __cil_tmp11 = __cil_tmp10 + 16;
3377#line 51
3378 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
3379#line 51
3380 cf = *mem_16;
3381#line 52
3382 __cil_tmp12 = (void *)tmp;
3383#line 52
3384 free(__cil_tmp12);
3385 }
3386 }
3387 while_1_break: ;
3388 }
3389#line 55
3390 __cil_tmp13 = (unsigned long )excep;
3391#line 55
3392 __cil_tmp14 = __cil_tmp13 + 24;
3393#line 55
3394 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
3395#line 55
3396 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
3397#line 694 "libacc.c"
3398 return;
3399}
3400}
3401#line 59 "libacc.c"
3402void __utac__exception__cf_handler_reset(void *exception )
3403{ struct __UTAC__EXCEPTION *excep ;
3404 struct __UTAC__CFLOW_FUNC *cf ;
3405 unsigned long __cil_tmp5 ;
3406 unsigned long __cil_tmp6 ;
3407 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
3408 unsigned long __cil_tmp8 ;
3409 unsigned long __cil_tmp9 ;
3410 int (*__cil_tmp10)(int , int ) ;
3411 unsigned long __cil_tmp11 ;
3412 unsigned long __cil_tmp12 ;
3413 int __cil_tmp13 ;
3414 unsigned long __cil_tmp14 ;
3415 unsigned long __cil_tmp15 ;
3416 struct __UTAC__CFLOW_FUNC **mem_16 ;
3417 int (**mem_17)(int , int ) ;
3418 int *mem_18 ;
3419 struct __UTAC__CFLOW_FUNC **mem_19 ;
3420
3421 {
3422#line 60
3423 excep = (struct __UTAC__EXCEPTION *)exception;
3424#line 61
3425 __cil_tmp5 = (unsigned long )excep;
3426#line 61
3427 __cil_tmp6 = __cil_tmp5 + 24;
3428#line 61
3429 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
3430#line 61
3431 cf = *mem_16;
3432 {
3433#line 64
3434 while (1) {
3435 while_2_continue: ;
3436 {
3437#line 64
3438 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
3439#line 64
3440 __cil_tmp8 = (unsigned long )__cil_tmp7;
3441#line 64
3442 __cil_tmp9 = (unsigned long )cf;
3443#line 64
3444 if (__cil_tmp9 != __cil_tmp8) {
3445
3446 } else {
3447 goto while_2_break;
3448 }
3449 }
3450 {
3451#line 65
3452 mem_17 = (int (**)(int , int ))cf;
3453#line 65
3454 __cil_tmp10 = *mem_17;
3455#line 65
3456 __cil_tmp11 = (unsigned long )cf;
3457#line 65
3458 __cil_tmp12 = __cil_tmp11 + 8;
3459#line 65
3460 mem_18 = (int *)__cil_tmp12;
3461#line 65
3462 __cil_tmp13 = *mem_18;
3463#line 65
3464 (*__cil_tmp10)(4, __cil_tmp13);
3465#line 66
3466 __cil_tmp14 = (unsigned long )cf;
3467#line 66
3468 __cil_tmp15 = __cil_tmp14 + 16;
3469#line 66
3470 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
3471#line 66
3472 cf = *mem_19;
3473 }
3474 }
3475 while_2_break: ;
3476 }
3477 {
3478#line 69
3479 __utac__exception__cf_handler_free(exception);
3480 }
3481#line 732 "libacc.c"
3482 return;
3483}
3484}
3485#line 80 "libacc.c"
3486void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
3487#line 80 "libacc.c"
3488static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
3489#line 79 "libacc.c"
3490void *__utac__error_stack_mgt(void *env , int mode , int count )
3491{ void *retValue_acc ;
3492 struct __ACC__ERR *new ;
3493 void *tmp ;
3494 struct __ACC__ERR *temp ;
3495 struct __ACC__ERR *next ;
3496 void *excep ;
3497 unsigned long __cil_tmp10 ;
3498 unsigned long __cil_tmp11 ;
3499 unsigned long __cil_tmp12 ;
3500 unsigned long __cil_tmp13 ;
3501 void *__cil_tmp14 ;
3502 unsigned long __cil_tmp15 ;
3503 unsigned long __cil_tmp16 ;
3504 void *__cil_tmp17 ;
3505 void **mem_18 ;
3506 struct __ACC__ERR **mem_19 ;
3507 struct __ACC__ERR **mem_20 ;
3508 void **mem_21 ;
3509 struct __ACC__ERR **mem_22 ;
3510 void **mem_23 ;
3511 void **mem_24 ;
3512
3513 {
3514#line 82 "libacc.c"
3515 if (count == 0) {
3516#line 758 "libacc.c"
3517 return (retValue_acc);
3518 } else {
3519
3520 }
3521#line 86 "libacc.c"
3522 if (mode == 0) {
3523 {
3524#line 87
3525 tmp = malloc(16UL);
3526#line 87
3527 new = (struct __ACC__ERR *)tmp;
3528#line 88
3529 mem_18 = (void **)new;
3530#line 88
3531 *mem_18 = env;
3532#line 89
3533 __cil_tmp10 = (unsigned long )new;
3534#line 89
3535 __cil_tmp11 = __cil_tmp10 + 8;
3536#line 89
3537 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
3538#line 89
3539 *mem_19 = head;
3540#line 90
3541 head = new;
3542#line 776 "libacc.c"
3543 retValue_acc = (void *)new;
3544 }
3545#line 778
3546 return (retValue_acc);
3547 } else {
3548
3549 }
3550#line 94 "libacc.c"
3551 if (mode == 1) {
3552#line 95
3553 temp = head;
3554 {
3555#line 98
3556 while (1) {
3557 while_3_continue: ;
3558#line 98
3559 if (count > 1) {
3560
3561 } else {
3562 goto while_3_break;
3563 }
3564 {
3565#line 99
3566 __cil_tmp12 = (unsigned long )temp;
3567#line 99
3568 __cil_tmp13 = __cil_tmp12 + 8;
3569#line 99
3570 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
3571#line 99
3572 next = *mem_20;
3573#line 100
3574 mem_21 = (void **)temp;
3575#line 100
3576 excep = *mem_21;
3577#line 101
3578 __cil_tmp14 = (void *)temp;
3579#line 101
3580 free(__cil_tmp14);
3581#line 102
3582 __utac__exception__cf_handler_reset(excep);
3583#line 103
3584 temp = next;
3585#line 104
3586 count = count - 1;
3587 }
3588 }
3589 while_3_break: ;
3590 }
3591 {
3592#line 107
3593 __cil_tmp15 = (unsigned long )temp;
3594#line 107
3595 __cil_tmp16 = __cil_tmp15 + 8;
3596#line 107
3597 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
3598#line 107
3599 head = *mem_22;
3600#line 108
3601 mem_23 = (void **)temp;
3602#line 108
3603 excep = *mem_23;
3604#line 109
3605 __cil_tmp17 = (void *)temp;
3606#line 109
3607 free(__cil_tmp17);
3608#line 110
3609 __utac__exception__cf_handler_reset(excep);
3610#line 820 "libacc.c"
3611 retValue_acc = excep;
3612 }
3613#line 822
3614 return (retValue_acc);
3615 } else {
3616
3617 }
3618#line 114
3619 if (mode == 2) {
3620#line 118 "libacc.c"
3621 if (head) {
3622#line 831
3623 mem_24 = (void **)head;
3624#line 831
3625 retValue_acc = *mem_24;
3626#line 833
3627 return (retValue_acc);
3628 } else {
3629#line 837 "libacc.c"
3630 retValue_acc = (void *)0;
3631#line 839
3632 return (retValue_acc);
3633 }
3634 } else {
3635
3636 }
3637#line 846 "libacc.c"
3638 return (retValue_acc);
3639}
3640}
3641#line 122 "libacc.c"
3642void *__utac__get_this_arg(int i , struct JoinPoint *this )
3643{ void *retValue_acc ;
3644 unsigned long __cil_tmp4 ;
3645 unsigned long __cil_tmp5 ;
3646 int __cil_tmp6 ;
3647 int __cil_tmp7 ;
3648 unsigned long __cil_tmp8 ;
3649 unsigned long __cil_tmp9 ;
3650 void **__cil_tmp10 ;
3651 void **__cil_tmp11 ;
3652 int *mem_12 ;
3653 void ***mem_13 ;
3654
3655 {
3656#line 123
3657 if (i > 0) {
3658 {
3659#line 123
3660 __cil_tmp4 = (unsigned long )this;
3661#line 123
3662 __cil_tmp5 = __cil_tmp4 + 16;
3663#line 123
3664 mem_12 = (int *)__cil_tmp5;
3665#line 123
3666 __cil_tmp6 = *mem_12;
3667#line 123
3668 if (i <= __cil_tmp6) {
3669
3670 } else {
3671 {
3672#line 123
3673 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3674 123U, "__utac__get_this_arg");
3675 }
3676 }
3677 }
3678 } else {
3679 {
3680#line 123
3681 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3682 123U, "__utac__get_this_arg");
3683 }
3684 }
3685#line 870 "libacc.c"
3686 __cil_tmp7 = i - 1;
3687#line 870
3688 __cil_tmp8 = (unsigned long )this;
3689#line 870
3690 __cil_tmp9 = __cil_tmp8 + 8;
3691#line 870
3692 mem_13 = (void ***)__cil_tmp9;
3693#line 870
3694 __cil_tmp10 = *mem_13;
3695#line 870
3696 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
3697#line 870
3698 retValue_acc = *__cil_tmp11;
3699#line 872
3700 return (retValue_acc);
3701#line 879
3702 return (retValue_acc);
3703}
3704}
3705#line 129 "libacc.c"
3706char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
3707{ char const *retValue_acc ;
3708 unsigned long __cil_tmp4 ;
3709 unsigned long __cil_tmp5 ;
3710 int __cil_tmp6 ;
3711 int __cil_tmp7 ;
3712 unsigned long __cil_tmp8 ;
3713 unsigned long __cil_tmp9 ;
3714 char const **__cil_tmp10 ;
3715 char const **__cil_tmp11 ;
3716 int *mem_12 ;
3717 char const ***mem_13 ;
3718
3719 {
3720#line 131
3721 if (i > 0) {
3722 {
3723#line 131
3724 __cil_tmp4 = (unsigned long )this;
3725#line 131
3726 __cil_tmp5 = __cil_tmp4 + 16;
3727#line 131
3728 mem_12 = (int *)__cil_tmp5;
3729#line 131
3730 __cil_tmp6 = *mem_12;
3731#line 131
3732 if (i <= __cil_tmp6) {
3733
3734 } else {
3735 {
3736#line 131
3737 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3738 131U, "__utac__get_this_argtype");
3739 }
3740 }
3741 }
3742 } else {
3743 {
3744#line 131
3745 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3746 131U, "__utac__get_this_argtype");
3747 }
3748 }
3749#line 903 "libacc.c"
3750 __cil_tmp7 = i - 1;
3751#line 903
3752 __cil_tmp8 = (unsigned long )this;
3753#line 903
3754 __cil_tmp9 = __cil_tmp8 + 24;
3755#line 903
3756 mem_13 = (char const ***)__cil_tmp9;
3757#line 903
3758 __cil_tmp10 = *mem_13;
3759#line 903
3760 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
3761#line 903
3762 retValue_acc = *__cil_tmp11;
3763#line 905
3764 return (retValue_acc);
3765#line 912
3766 return (retValue_acc);
3767}
3768}
3769#line 1 "AddressBookEncrypt_spec.o"
3770#pragma merger(0,"AddressBookEncrypt_spec.i","")
3771#line 7 "AddressBookEncrypt_spec.c"
3772int mail_is_sensitive = -1;
3773#line 11 "AddressBookEncrypt_spec.c"
3774__inline void __utac_acc__AddressBookEncrypt_spec__1(int client , int msg )
3775{ int tmp ;
3776
3777 {
3778 {
3779#line 13
3780 puts("before mail\n");
3781 }
3782#line 14
3783 if (mail_is_sensitive == -1) {
3784 {
3785#line 15
3786 mail_is_sensitive = isEncrypted(msg);
3787 }
3788 } else {
3789 {
3790#line 16
3791 tmp = isEncrypted(msg);
3792 }
3793#line 16
3794 if (mail_is_sensitive != tmp) {
3795 {
3796#line 17
3797 __automaton_fail();
3798 }
3799 } else {
3800
3801 }
3802 }
3803#line 17
3804 return;
3805}
3806}
3807#line 1 "Client.o"
3808#pragma merger(0,"Client.i","")
3809#line 14 "Client.h"
3810void queue(int client , int msg ) ;
3811#line 24
3812void mail(int client , int msg ) ;
3813#line 28
3814void deliver(int client , int msg ) ;
3815#line 30
3816void incoming(int client , int msg ) ;
3817#line 32
3818int createClient(char *name ) ;
3819#line 40
3820int isKeyPairValid(int publicKey , int privateKey ) ;
3821#line 45
3822void autoRespond(int client , int msg ) ;
3823#line 6 "Client.c"
3824int queue_empty = 1;
3825#line 9 "Client.c"
3826int queued_message ;
3827#line 12 "Client.c"
3828int queued_client ;
3829#line 18 "Client.c"
3830void mail(int client , int msg )
3831{ int __utac__ad__arg1 ;
3832 int __utac__ad__arg2 ;
3833 int tmp ;
3834
3835 {
3836 {
3837#line 722 "Client.c"
3838 __utac__ad__arg1 = client;
3839#line 723
3840 __utac__ad__arg2 = msg;
3841#line 724
3842 __utac_acc__AddressBookEncrypt_spec__1(__utac__ad__arg1, __utac__ad__arg2);
3843#line 19 "Client.c"
3844 puts("mail sent");
3845#line 20
3846 tmp = getEmailTo(msg);
3847#line 20
3848 incoming(tmp, msg);
3849 }
3850#line 741 "Client.c"
3851 return;
3852}
3853}
3854#line 27 "Client.c"
3855void outgoing__wrappee__Keys(int client , int msg )
3856{ int tmp ;
3857
3858 {
3859 {
3860#line 28
3861 tmp = getClientId(client);
3862#line 28
3863 setEmailFrom(msg, tmp);
3864#line 29
3865 mail(client, msg);
3866 }
3867#line 763 "Client.c"
3868 return;
3869}
3870}
3871#line 33 "Client.c"
3872void outgoing(int client , int msg )
3873{ int receiver ;
3874 int tmp ;
3875 int pubkey ;
3876 int tmp___0 ;
3877
3878 {
3879 {
3880#line 36
3881 tmp = getEmailTo(msg);
3882#line 36
3883 receiver = tmp;
3884#line 37
3885 tmp___0 = findPublicKey(client, receiver);
3886#line 37
3887 pubkey = tmp___0;
3888 }
3889#line 38
3890 if (pubkey) {
3891 {
3892#line 39
3893 setEmailEncryptionKey(msg, pubkey);
3894#line 40
3895 setEmailIsEncrypted(msg, 1);
3896 }
3897 } else {
3898
3899 }
3900 {
3901#line 45
3902 outgoing__wrappee__Keys(client, msg);
3903 }
3904#line 798 "Client.c"
3905 return;
3906}
3907}
3908#line 52 "Client.c"
3909void deliver(int client , int msg )
3910{
3911
3912 {
3913 {
3914#line 53
3915 puts("mail delivered\n");
3916 }
3917#line 818 "Client.c"
3918 return;
3919}
3920}
3921#line 60 "Client.c"
3922void incoming__wrappee__Encrypt(int client , int msg )
3923{
3924
3925 {
3926 {
3927#line 61
3928 deliver(client, msg);
3929 }
3930#line 838 "Client.c"
3931 return;
3932}
3933}
3934#line 67 "Client.c"
3935void incoming__wrappee__AutoResponder(int client , int msg )
3936{ int tmp ;
3937
3938 {
3939 {
3940#line 68
3941 incoming__wrappee__Encrypt(client, msg);
3942#line 69
3943 tmp = getClientAutoResponse(client);
3944 }
3945#line 69
3946 if (tmp) {
3947 {
3948#line 70
3949 autoRespond(client, msg);
3950 }
3951 } else {
3952
3953 }
3954#line 863 "Client.c"
3955 return;
3956}
3957}
3958#line 76 "Client.c"
3959void incoming(int client , int msg )
3960{ int privkey ;
3961 int tmp ;
3962 int tmp___0 ;
3963 int tmp___1 ;
3964 int tmp___2 ;
3965
3966 {
3967 {
3968#line 79
3969 tmp = getClientPrivateKey(client);
3970#line 79
3971 privkey = tmp;
3972 }
3973#line 80
3974 if (privkey) {
3975 {
3976#line 88
3977 tmp___0 = isEncrypted(msg);
3978 }
3979#line 88
3980 if (tmp___0) {
3981 {
3982#line 88
3983 tmp___1 = getEmailEncryptionKey(msg);
3984#line 88
3985 tmp___2 = isKeyPairValid(tmp___1, privkey);
3986 }
3987#line 88
3988 if (tmp___2) {
3989 {
3990#line 85
3991 setEmailIsEncrypted(msg, 0);
3992#line 86
3993 setEmailEncryptionKey(msg, 0);
3994 }
3995 } else {
3996
3997 }
3998 } else {
3999
4000 }
4001 } else {
4002
4003 }
4004 {
4005#line 91
4006 incoming__wrappee__AutoResponder(client, msg);
4007 }
4008#line 897 "Client.c"
4009 return;
4010}
4011}
4012#line 95 "Client.c"
4013int createClient(char *name )
4014{ int retValue_acc ;
4015 int client ;
4016 int tmp ;
4017
4018 {
4019 {
4020#line 96
4021 tmp = initClient();
4022#line 96
4023 client = tmp;
4024#line 919 "Client.c"
4025 retValue_acc = client;
4026 }
4027#line 921
4028 return (retValue_acc);
4029#line 928
4030 return (retValue_acc);
4031}
4032}
4033#line 103 "Client.c"
4034void sendEmail(int sender , int receiver )
4035{ int email ;
4036 int tmp ;
4037
4038 {
4039 {
4040#line 104
4041 tmp = createEmail(0, receiver);
4042#line 104
4043 email = tmp;
4044#line 105
4045 outgoing(sender, email);
4046 }
4047#line 956 "Client.c"
4048 return;
4049}
4050}
4051#line 113 "Client.c"
4052void queue(int client , int msg )
4053{
4054
4055 {
4056#line 114
4057 queue_empty = 0;
4058#line 115
4059 queued_message = msg;
4060#line 116
4061 queued_client = client;
4062#line 980 "Client.c"
4063 return;
4064}
4065}
4066#line 122 "Client.c"
4067int is_queue_empty(void)
4068{ int retValue_acc ;
4069
4070 {
4071#line 998 "Client.c"
4072 retValue_acc = queue_empty;
4073#line 1000
4074 return (retValue_acc);
4075#line 1007
4076 return (retValue_acc);
4077}
4078}
4079#line 129 "Client.c"
4080int get_queued_client(void)
4081{ int retValue_acc ;
4082
4083 {
4084#line 1029 "Client.c"
4085 retValue_acc = queued_client;
4086#line 1031
4087 return (retValue_acc);
4088#line 1038
4089 return (retValue_acc);
4090}
4091}
4092#line 136 "Client.c"
4093int get_queued_email(void)
4094{ int retValue_acc ;
4095
4096 {
4097#line 1060 "Client.c"
4098 retValue_acc = queued_message;
4099#line 1062
4100 return (retValue_acc);
4101#line 1069
4102 return (retValue_acc);
4103}
4104}
4105#line 142 "Client.c"
4106int isKeyPairValid(int publicKey , int privateKey )
4107{ int retValue_acc ;
4108 char const * __restrict __cil_tmp4 ;
4109
4110 {
4111 {
4112#line 143
4113 __cil_tmp4 = (char const * __restrict )"keypair valid %d %d";
4114#line 143
4115 printf(__cil_tmp4, publicKey, privateKey);
4116 }
4117#line 144 "Client.c"
4118 if (! publicKey) {
4119#line 1094 "Client.c"
4120 retValue_acc = 0;
4121#line 1096
4122 return (retValue_acc);
4123 } else {
4124#line 144 "Client.c"
4125 if (! privateKey) {
4126#line 1094 "Client.c"
4127 retValue_acc = 0;
4128#line 1096
4129 return (retValue_acc);
4130 } else {
4131
4132 }
4133 }
4134#line 1101 "Client.c"
4135 retValue_acc = privateKey == publicKey;
4136#line 1103
4137 return (retValue_acc);
4138#line 1110
4139 return (retValue_acc);
4140}
4141}
4142#line 152 "Client.c"
4143void generateKeyPair(int client , int seed )
4144{
4145
4146 {
4147 {
4148#line 153
4149 setClientPrivateKey(client, seed);
4150 }
4151#line 1134 "Client.c"
4152 return;
4153}
4154}
4155#line 159 "Client.c"
4156void autoRespond(int client , int msg )
4157{ int sender ;
4158 int tmp ;
4159
4160 {
4161 {
4162#line 160
4163 puts("sending autoresponse\n");
4164#line 161
4165 tmp = getEmailFrom(msg);
4166#line 161
4167 sender = tmp;
4168#line 162
4169 setEmailTo(msg, sender);
4170#line 163
4171 queue(client, msg);
4172 }
4173#line 1276 "Client.c"
4174 return;
4175}
4176}
4177#line 1 "Util.o"
4178#pragma merger(0,"Util.i","")
4179#line 1 "Util.h"
4180int prompt(char *msg ) ;
4181#line 9 "Util.c"
4182int prompt(char *msg )
4183{ int retValue_acc ;
4184 int retval ;
4185 char const * __restrict __cil_tmp4 ;
4186
4187 {
4188 {
4189#line 10
4190 __cil_tmp4 = (char const * __restrict )"%s\n";
4191#line 10
4192 printf(__cil_tmp4, msg);
4193#line 518 "Util.c"
4194 retValue_acc = retval;
4195 }
4196#line 520
4197 return (retValue_acc);
4198#line 527
4199 return (retValue_acc);
4200}
4201}
4202#line 1 "featureselect.o"
4203#pragma merger(0,"featureselect.i","")
4204#line 41 "featureselect.h"
4205int select_one(void) ;
4206#line 8 "featureselect.c"
4207int select_one(void)
4208{ int retValue_acc ;
4209 int choice = __VERIFIER_nondet_int();
4210
4211 {
4212#line 84 "featureselect.c"
4213 retValue_acc = choice;
4214#line 86
4215 return (retValue_acc);
4216#line 93
4217 return (retValue_acc);
4218}
4219}
4220#line 14 "featureselect.c"
4221void select_features(void)
4222{
4223
4224 {
4225#line 115 "featureselect.c"
4226 return;
4227}
4228}
4229#line 20 "featureselect.c"
4230void select_helpers(void)
4231{
4232
4233 {
4234#line 133 "featureselect.c"
4235 return;
4236}
4237}
4238#line 25 "featureselect.c"
4239int valid_product(void)
4240{ int retValue_acc ;
4241
4242 {
4243#line 151 "featureselect.c"
4244 retValue_acc = 1;
4245#line 153
4246 return (retValue_acc);
4247#line 160
4248 return (retValue_acc);
4249}
4250}