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