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