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