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