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 "scenario.o"
42#pragma merger(0,"scenario.i","")
43#line 17 "scenario.c"
44void bobKeyAdd(void) ;
45#line 21
46void rjhSetAutoRespond(void) ;
47#line 25
48void rjhDeletePrivateKey(void) ;
49#line 29
50void rjhKeyAdd(void) ;
51#line 33
52void chuckKeyAddRjh(void) ;
53#line 40
54void rjhKeyChange(void) ;
55#line 44
56void bobSetAddressBook(void) ;
57#line 48
58void chuckKeyAdd(void) ;
59#line 52
60void bobKeyChange(void) ;
61#line 54
62#line 61
63void bobToRjh(void) ;
64#line 1 "scenario.c"
65void test(void)
66{ int op1 ;
67 int op2 ;
68 int op3 ;
69 int op4 ;
70 int op5 ;
71 int op6 ;
72 int op7 ;
73 int op8 ;
74 int op9 ;
75 int op10 ;
76 int op11 ;
77 int splverifierCounter ;
78 int tmp ;
79 int tmp___0 ;
80 int tmp___1 ;
81 int tmp___2 ;
82 int tmp___3 ;
83 int tmp___4 ;
84 int tmp___5 ;
85 int tmp___6 ;
86 int tmp___7 ;
87 int tmp___8 ;
88 int tmp___9 ;
89
90 {
91#line 2
92 op1 = 0;
93#line 3
94 op2 = 0;
95#line 4
96 op3 = 0;
97#line 5
98 op4 = 0;
99#line 6
100 op5 = 0;
101#line 7
102 op6 = 0;
103#line 8
104 op7 = 0;
105#line 9
106 op8 = 0;
107#line 10
108 op9 = 0;
109#line 11
110 op10 = 0;
111#line 12
112 op11 = 0;
113#line 13
114 splverifierCounter = 0;
115 {
116#line 14
117 while (1) {
118 while_0_continue: ;
119#line 14
120 if (splverifierCounter < 4) {
121
122 } else {
123 goto while_0_break;
124 }
125#line 15
126 splverifierCounter = splverifierCounter + 1;
127#line 16
128 if (! op1) {
129 {
130#line 16
131 tmp___9 = __VERIFIER_nondet_int();
132 }
133#line 16
134 if (tmp___9) {
135 {
136#line 17
137 bobKeyAdd();
138#line 18
139 op1 = 1;
140 }
141 } else {
142 goto _L___8;
143 }
144 } else {
145 _L___8:
146#line 19
147 if (! op2) {
148 {
149#line 19
150 tmp___8 = __VERIFIER_nondet_int();
151 }
152#line 19
153 if (tmp___8) {
154 {
155#line 21
156 rjhSetAutoRespond();
157#line 22
158 op2 = 1;
159 }
160 } else {
161 goto _L___7;
162 }
163 } else {
164 _L___7:
165#line 23
166 if (! op3) {
167 {
168#line 23
169 tmp___7 = __VERIFIER_nondet_int();
170 }
171#line 23
172 if (tmp___7) {
173 {
174#line 25
175 rjhDeletePrivateKey();
176#line 26
177 op3 = 1;
178 }
179 } else {
180 goto _L___6;
181 }
182 } else {
183 _L___6:
184#line 27
185 if (! op4) {
186 {
187#line 27
188 tmp___6 = __VERIFIER_nondet_int();
189 }
190#line 27
191 if (tmp___6) {
192 {
193#line 29
194 rjhKeyAdd();
195#line 30
196 op4 = 1;
197 }
198 } else {
199 goto _L___5;
200 }
201 } else {
202 _L___5:
203#line 31
204 if (! op5) {
205 {
206#line 31
207 tmp___5 = __VERIFIER_nondet_int();
208 }
209#line 31
210 if (tmp___5) {
211 {
212#line 33
213 chuckKeyAddRjh();
214#line 34
215 op5 = 1;
216 }
217 } else {
218 goto _L___4;
219 }
220 } else {
221 _L___4:
222#line 35
223 if (! op6) {
224 {
225#line 35
226 tmp___4 = __VERIFIER_nondet_int();
227 }
228#line 35
229 if (tmp___4) {
230#line 37
231 op6 = 1;
232 } else {
233 goto _L___3;
234 }
235 } else {
236 _L___3:
237#line 38
238 if (! op7) {
239 {
240#line 38
241 tmp___3 = __VERIFIER_nondet_int();
242 }
243#line 38
244 if (tmp___3) {
245 {
246#line 40
247 rjhKeyChange();
248#line 41
249 op7 = 1;
250 }
251 } else {
252 goto _L___2;
253 }
254 } else {
255 _L___2:
256#line 42
257 if (! op8) {
258 {
259#line 42
260 tmp___2 = __VERIFIER_nondet_int();
261 }
262#line 42
263 if (tmp___2) {
264 {
265#line 44
266 bobSetAddressBook();
267#line 45
268 op8 = 1;
269 }
270 } else {
271 goto _L___1;
272 }
273 } else {
274 _L___1:
275#line 46
276 if (! op9) {
277 {
278#line 46
279 tmp___1 = __VERIFIER_nondet_int();
280 }
281#line 46
282 if (tmp___1) {
283 {
284#line 48
285 chuckKeyAdd();
286#line 49
287 op9 = 1;
288 }
289 } else {
290 goto _L___0;
291 }
292 } else {
293 _L___0:
294#line 50
295 if (! op10) {
296 {
297#line 50
298 tmp___0 = __VERIFIER_nondet_int();
299 }
300#line 50
301 if (tmp___0) {
302 {
303#line 52
304 bobKeyChange();
305#line 53
306 op10 = 1;
307 }
308 } else {
309 goto _L;
310 }
311 } else {
312 _L:
313#line 54
314 if (! op11) {
315 {
316#line 54
317 tmp = __VERIFIER_nondet_int();
318 }
319#line 54
320 if (tmp) {
321 {
322#line 56
323 chuckKeyAdd();
324#line 57
325 op11 = 1;
326 }
327 } else {
328 goto while_0_break;
329 }
330 } else {
331 goto while_0_break;
332 }
333 }
334 }
335 }
336 }
337 }
338 }
339 }
340 }
341 }
342 }
343 }
344 while_0_break: ;
345 }
346 {
347#line 61
348 bobToRjh();
349 }
350#line 169 "scenario.c"
351 return;
352}
353}
354#line 1 "ClientLib.o"
355#pragma merger(0,"ClientLib.i","")
356#line 4 "ClientLib.h"
357int initClient(void) ;
358#line 6
359char *getClientName(int handle ) ;
360#line 8
361void setClientName(int handle , char *value ) ;
362#line 10
363int getClientOutbuffer(int handle ) ;
364#line 12
365void setClientOutbuffer(int handle , int value ) ;
366#line 14
367int getClientAddressBookSize(int handle ) ;
368#line 16
369void setClientAddressBookSize(int handle , int value ) ;
370#line 18
371int createClientAddressBookEntry(int handle ) ;
372#line 20
373int getClientAddressBookAlias(int handle , int index ) ;
374#line 22
375void setClientAddressBookAlias(int handle , int index , int value ) ;
376#line 24
377int getClientAddressBookAddress(int handle , int index ) ;
378#line 26
379void setClientAddressBookAddress(int handle , int index , int value ) ;
380#line 29
381int getClientAutoResponse(int handle ) ;
382#line 31
383void setClientAutoResponse(int handle , int value ) ;
384#line 33
385int getClientPrivateKey(int handle ) ;
386#line 35
387void setClientPrivateKey(int handle , int value ) ;
388#line 37
389int getClientKeyringSize(int handle ) ;
390#line 39
391int createClientKeyringEntry(int handle ) ;
392#line 41
393int getClientKeyringUser(int handle , int index ) ;
394#line 43
395void setClientKeyringUser(int handle , int index , int value ) ;
396#line 45
397int getClientKeyringPublicKey(int handle , int index ) ;
398#line 47
399void setClientKeyringPublicKey(int handle , int index , int value ) ;
400#line 49
401int getClientForwardReceiver(int handle ) ;
402#line 51
403void setClientForwardReceiver(int handle , int value ) ;
404#line 53
405int getClientId(int handle ) ;
406#line 55
407void setClientId(int handle , int value ) ;
408#line 57
409int findPublicKey(int handle , int userid ) ;
410#line 59
411int findClientAddressBookAlias(int handle , int userid ) ;
412#line 5 "ClientLib.c"
413int __ste_Client_counter = 0;
414#line 7 "ClientLib.c"
415int initClient(void)
416{ int retValue_acc ;
417
418 {
419#line 12 "ClientLib.c"
420 if (__ste_Client_counter < 3) {
421#line 684
422 __ste_Client_counter = __ste_Client_counter + 1;
423#line 684
424 retValue_acc = __ste_Client_counter;
425#line 686
426 return (retValue_acc);
427 } else {
428#line 692 "ClientLib.c"
429 retValue_acc = -1;
430#line 694
431 return (retValue_acc);
432 }
433#line 701 "ClientLib.c"
434 return (retValue_acc);
435}
436}
437#line 15 "ClientLib.c"
438char *__ste_client_name0 = (char *)0;
439#line 17 "ClientLib.c"
440char *__ste_client_name1 = (char *)0;
441#line 19 "ClientLib.c"
442char *__ste_client_name2 = (char *)0;
443#line 22 "ClientLib.c"
444char *getClientName(int handle )
445{ char *retValue_acc ;
446 void *__cil_tmp3 ;
447
448 {
449#line 31 "ClientLib.c"
450 if (handle == 1) {
451#line 732
452 retValue_acc = __ste_client_name0;
453#line 734
454 return (retValue_acc);
455 } else {
456#line 736
457 if (handle == 2) {
458#line 741
459 retValue_acc = __ste_client_name1;
460#line 743
461 return (retValue_acc);
462 } else {
463#line 745
464 if (handle == 3) {
465#line 750
466 retValue_acc = __ste_client_name2;
467#line 752
468 return (retValue_acc);
469 } else {
470#line 758 "ClientLib.c"
471 __cil_tmp3 = (void *)0;
472#line 758
473 retValue_acc = (char *)__cil_tmp3;
474#line 760
475 return (retValue_acc);
476 }
477 }
478 }
479#line 767 "ClientLib.c"
480 return (retValue_acc);
481}
482}
483#line 34 "ClientLib.c"
484void setClientName(int handle , char *value )
485{
486
487 {
488#line 42
489 if (handle == 1) {
490#line 36
491 __ste_client_name0 = value;
492 } else {
493#line 37
494 if (handle == 2) {
495#line 38
496 __ste_client_name1 = value;
497 } else {
498#line 39
499 if (handle == 3) {
500#line 40
501 __ste_client_name2 = value;
502 } else {
503
504 }
505 }
506 }
507#line 802 "ClientLib.c"
508 return;
509}
510}
511#line 44 "ClientLib.c"
512int __ste_client_outbuffer0 = 0;
513#line 46 "ClientLib.c"
514int __ste_client_outbuffer1 = 0;
515#line 48 "ClientLib.c"
516int __ste_client_outbuffer2 = 0;
517#line 50 "ClientLib.c"
518int __ste_client_outbuffer3 = 0;
519#line 53 "ClientLib.c"
520int getClientOutbuffer(int handle )
521{ int retValue_acc ;
522
523 {
524#line 62 "ClientLib.c"
525 if (handle == 1) {
526#line 831
527 retValue_acc = __ste_client_outbuffer0;
528#line 833
529 return (retValue_acc);
530 } else {
531#line 835
532 if (handle == 2) {
533#line 840
534 retValue_acc = __ste_client_outbuffer1;
535#line 842
536 return (retValue_acc);
537 } else {
538#line 844
539 if (handle == 3) {
540#line 849
541 retValue_acc = __ste_client_outbuffer2;
542#line 851
543 return (retValue_acc);
544 } else {
545#line 857 "ClientLib.c"
546 retValue_acc = 0;
547#line 859
548 return (retValue_acc);
549 }
550 }
551 }
552#line 866 "ClientLib.c"
553 return (retValue_acc);
554}
555}
556#line 65 "ClientLib.c"
557void setClientOutbuffer(int handle , int value )
558{
559
560 {
561#line 73
562 if (handle == 1) {
563#line 67
564 __ste_client_outbuffer0 = value;
565 } else {
566#line 68
567 if (handle == 2) {
568#line 69
569 __ste_client_outbuffer1 = value;
570 } else {
571#line 70
572 if (handle == 3) {
573#line 71
574 __ste_client_outbuffer2 = value;
575 } else {
576
577 }
578 }
579 }
580#line 901 "ClientLib.c"
581 return;
582}
583}
584#line 77 "ClientLib.c"
585int __ste_ClientAddressBook_size0 = 0;
586#line 79 "ClientLib.c"
587int __ste_ClientAddressBook_size1 = 0;
588#line 81 "ClientLib.c"
589int __ste_ClientAddressBook_size2 = 0;
590#line 84 "ClientLib.c"
591int getClientAddressBookSize(int handle )
592{ int retValue_acc ;
593
594 {
595#line 93 "ClientLib.c"
596 if (handle == 1) {
597#line 928
598 retValue_acc = __ste_ClientAddressBook_size0;
599#line 930
600 return (retValue_acc);
601 } else {
602#line 932
603 if (handle == 2) {
604#line 937
605 retValue_acc = __ste_ClientAddressBook_size1;
606#line 939
607 return (retValue_acc);
608 } else {
609#line 941
610 if (handle == 3) {
611#line 946
612 retValue_acc = __ste_ClientAddressBook_size2;
613#line 948
614 return (retValue_acc);
615 } else {
616#line 954 "ClientLib.c"
617 retValue_acc = 0;
618#line 956
619 return (retValue_acc);
620 }
621 }
622 }
623#line 963 "ClientLib.c"
624 return (retValue_acc);
625}
626}
627#line 96 "ClientLib.c"
628void setClientAddressBookSize(int handle , int value )
629{
630
631 {
632#line 104
633 if (handle == 1) {
634#line 98
635 __ste_ClientAddressBook_size0 = value;
636 } else {
637#line 99
638 if (handle == 2) {
639#line 100
640 __ste_ClientAddressBook_size1 = value;
641 } else {
642#line 101
643 if (handle == 3) {
644#line 102
645 __ste_ClientAddressBook_size2 = value;
646 } else {
647
648 }
649 }
650 }
651#line 998 "ClientLib.c"
652 return;
653}
654}
655#line 106 "ClientLib.c"
656int createClientAddressBookEntry(int handle )
657{ int retValue_acc ;
658 int size ;
659 int tmp ;
660 int __cil_tmp5 ;
661
662 {
663 {
664#line 107
665 tmp = getClientAddressBookSize(handle);
666#line 107
667 size = tmp;
668 }
669#line 108 "ClientLib.c"
670 if (size < 3) {
671 {
672#line 109 "ClientLib.c"
673 __cil_tmp5 = size + 1;
674#line 109
675 setClientAddressBookSize(handle, __cil_tmp5);
676#line 1025 "ClientLib.c"
677 retValue_acc = size + 1;
678 }
679#line 1027
680 return (retValue_acc);
681 } else {
682#line 1031 "ClientLib.c"
683 retValue_acc = -1;
684#line 1033
685 return (retValue_acc);
686 }
687#line 1040 "ClientLib.c"
688 return (retValue_acc);
689}
690}
691#line 115 "ClientLib.c"
692int __ste_Client_AddressBook0_Alias0 = 0;
693#line 117 "ClientLib.c"
694int __ste_Client_AddressBook0_Alias1 = 0;
695#line 119 "ClientLib.c"
696int __ste_Client_AddressBook0_Alias2 = 0;
697#line 121 "ClientLib.c"
698int __ste_Client_AddressBook1_Alias0 = 0;
699#line 123 "ClientLib.c"
700int __ste_Client_AddressBook1_Alias1 = 0;
701#line 125 "ClientLib.c"
702int __ste_Client_AddressBook1_Alias2 = 0;
703#line 127 "ClientLib.c"
704int __ste_Client_AddressBook2_Alias0 = 0;
705#line 129 "ClientLib.c"
706int __ste_Client_AddressBook2_Alias1 = 0;
707#line 131 "ClientLib.c"
708int __ste_Client_AddressBook2_Alias2 = 0;
709#line 134 "ClientLib.c"
710int getClientAddressBookAlias(int handle , int index )
711{ int retValue_acc ;
712
713 {
714#line 167
715 if (handle == 1) {
716#line 144 "ClientLib.c"
717 if (index == 0) {
718#line 1086
719 retValue_acc = __ste_Client_AddressBook0_Alias0;
720#line 1088
721 return (retValue_acc);
722 } else {
723#line 1090
724 if (index == 1) {
725#line 1095
726 retValue_acc = __ste_Client_AddressBook0_Alias1;
727#line 1097
728 return (retValue_acc);
729 } else {
730#line 1099
731 if (index == 2) {
732#line 1104
733 retValue_acc = __ste_Client_AddressBook0_Alias2;
734#line 1106
735 return (retValue_acc);
736 } else {
737#line 1112
738 retValue_acc = 0;
739#line 1114
740 return (retValue_acc);
741 }
742 }
743 }
744 } else {
745#line 1116 "ClientLib.c"
746 if (handle == 2) {
747#line 154 "ClientLib.c"
748 if (index == 0) {
749#line 1124
750 retValue_acc = __ste_Client_AddressBook1_Alias0;
751#line 1126
752 return (retValue_acc);
753 } else {
754#line 1128
755 if (index == 1) {
756#line 1133
757 retValue_acc = __ste_Client_AddressBook1_Alias1;
758#line 1135
759 return (retValue_acc);
760 } else {
761#line 1137
762 if (index == 2) {
763#line 1142
764 retValue_acc = __ste_Client_AddressBook1_Alias2;
765#line 1144
766 return (retValue_acc);
767 } else {
768#line 1150
769 retValue_acc = 0;
770#line 1152
771 return (retValue_acc);
772 }
773 }
774 }
775 } else {
776#line 1154 "ClientLib.c"
777 if (handle == 3) {
778#line 164 "ClientLib.c"
779 if (index == 0) {
780#line 1162
781 retValue_acc = __ste_Client_AddressBook2_Alias0;
782#line 1164
783 return (retValue_acc);
784 } else {
785#line 1166
786 if (index == 1) {
787#line 1171
788 retValue_acc = __ste_Client_AddressBook2_Alias1;
789#line 1173
790 return (retValue_acc);
791 } else {
792#line 1175
793 if (index == 2) {
794#line 1180
795 retValue_acc = __ste_Client_AddressBook2_Alias2;
796#line 1182
797 return (retValue_acc);
798 } else {
799#line 1188
800 retValue_acc = 0;
801#line 1190
802 return (retValue_acc);
803 }
804 }
805 }
806 } else {
807#line 1196 "ClientLib.c"
808 retValue_acc = 0;
809#line 1198
810 return (retValue_acc);
811 }
812 }
813 }
814#line 1205 "ClientLib.c"
815 return (retValue_acc);
816}
817}
818#line 171 "ClientLib.c"
819int findClientAddressBookAlias(int handle , int userid )
820{ int retValue_acc ;
821
822 {
823#line 204
824 if (handle == 1) {
825#line 181 "ClientLib.c"
826 if (userid == __ste_Client_AddressBook0_Alias0) {
827#line 1233
828 retValue_acc = 0;
829#line 1235
830 return (retValue_acc);
831 } else {
832#line 1237
833 if (userid == __ste_Client_AddressBook0_Alias1) {
834#line 1242
835 retValue_acc = 1;
836#line 1244
837 return (retValue_acc);
838 } else {
839#line 1246
840 if (userid == __ste_Client_AddressBook0_Alias2) {
841#line 1251
842 retValue_acc = 2;
843#line 1253
844 return (retValue_acc);
845 } else {
846#line 1259
847 retValue_acc = -1;
848#line 1261
849 return (retValue_acc);
850 }
851 }
852 }
853 } else {
854#line 1263 "ClientLib.c"
855 if (handle == 2) {
856#line 191 "ClientLib.c"
857 if (userid == __ste_Client_AddressBook1_Alias0) {
858#line 1271
859 retValue_acc = 0;
860#line 1273
861 return (retValue_acc);
862 } else {
863#line 1275
864 if (userid == __ste_Client_AddressBook1_Alias1) {
865#line 1280
866 retValue_acc = 1;
867#line 1282
868 return (retValue_acc);
869 } else {
870#line 1284
871 if (userid == __ste_Client_AddressBook1_Alias2) {
872#line 1289
873 retValue_acc = 2;
874#line 1291
875 return (retValue_acc);
876 } else {
877#line 1297
878 retValue_acc = -1;
879#line 1299
880 return (retValue_acc);
881 }
882 }
883 }
884 } else {
885#line 1301 "ClientLib.c"
886 if (handle == 3) {
887#line 201 "ClientLib.c"
888 if (userid == __ste_Client_AddressBook2_Alias0) {
889#line 1309
890 retValue_acc = 0;
891#line 1311
892 return (retValue_acc);
893 } else {
894#line 1313
895 if (userid == __ste_Client_AddressBook2_Alias1) {
896#line 1318
897 retValue_acc = 1;
898#line 1320
899 return (retValue_acc);
900 } else {
901#line 1322
902 if (userid == __ste_Client_AddressBook2_Alias2) {
903#line 1327
904 retValue_acc = 2;
905#line 1329
906 return (retValue_acc);
907 } else {
908#line 1335
909 retValue_acc = -1;
910#line 1337
911 return (retValue_acc);
912 }
913 }
914 }
915 } else {
916#line 1343 "ClientLib.c"
917 retValue_acc = -1;
918#line 1345
919 return (retValue_acc);
920 }
921 }
922 }
923#line 1352 "ClientLib.c"
924 return (retValue_acc);
925}
926}
927#line 208 "ClientLib.c"
928void setClientAddressBookAlias(int handle , int index , int value )
929{
930
931 {
932#line 234
933 if (handle == 1) {
934#line 217
935 if (index == 0) {
936#line 211
937 __ste_Client_AddressBook0_Alias0 = value;
938 } else {
939#line 212
940 if (index == 1) {
941#line 213
942 __ste_Client_AddressBook0_Alias1 = value;
943 } else {
944#line 214
945 if (index == 2) {
946#line 215
947 __ste_Client_AddressBook0_Alias2 = value;
948 } else {
949
950 }
951 }
952 }
953 } else {
954#line 216
955 if (handle == 2) {
956#line 225
957 if (index == 0) {
958#line 219
959 __ste_Client_AddressBook1_Alias0 = value;
960 } else {
961#line 220
962 if (index == 1) {
963#line 221
964 __ste_Client_AddressBook1_Alias1 = value;
965 } else {
966#line 222
967 if (index == 2) {
968#line 223
969 __ste_Client_AddressBook1_Alias2 = value;
970 } else {
971
972 }
973 }
974 }
975 } else {
976#line 224
977 if (handle == 3) {
978#line 233
979 if (index == 0) {
980#line 227
981 __ste_Client_AddressBook2_Alias0 = value;
982 } else {
983#line 228
984 if (index == 1) {
985#line 229
986 __ste_Client_AddressBook2_Alias1 = value;
987 } else {
988#line 230
989 if (index == 2) {
990#line 231
991 __ste_Client_AddressBook2_Alias2 = value;
992 } else {
993
994 }
995 }
996 }
997 } else {
998
999 }
1000 }
1001 }
1002#line 1420 "ClientLib.c"
1003 return;
1004}
1005}
1006#line 236 "ClientLib.c"
1007int __ste_Client_AddressBook0_Address0 = 0;
1008#line 238 "ClientLib.c"
1009int __ste_Client_AddressBook0_Address1 = 0;
1010#line 240 "ClientLib.c"
1011int __ste_Client_AddressBook0_Address2 = 0;
1012#line 242 "ClientLib.c"
1013int __ste_Client_AddressBook1_Address0 = 0;
1014#line 244 "ClientLib.c"
1015int __ste_Client_AddressBook1_Address1 = 0;
1016#line 246 "ClientLib.c"
1017int __ste_Client_AddressBook1_Address2 = 0;
1018#line 248 "ClientLib.c"
1019int __ste_Client_AddressBook2_Address0 = 0;
1020#line 250 "ClientLib.c"
1021int __ste_Client_AddressBook2_Address1 = 0;
1022#line 252 "ClientLib.c"
1023int __ste_Client_AddressBook2_Address2 = 0;
1024#line 255 "ClientLib.c"
1025int getClientAddressBookAddress(int handle , int index )
1026{ int retValue_acc ;
1027
1028 {
1029#line 288
1030 if (handle == 1) {
1031#line 265 "ClientLib.c"
1032 if (index == 0) {
1033#line 1462
1034 retValue_acc = __ste_Client_AddressBook0_Address0;
1035#line 1464
1036 return (retValue_acc);
1037 } else {
1038#line 1466
1039 if (index == 1) {
1040#line 1471
1041 retValue_acc = __ste_Client_AddressBook0_Address1;
1042#line 1473
1043 return (retValue_acc);
1044 } else {
1045#line 1475
1046 if (index == 2) {
1047#line 1480
1048 retValue_acc = __ste_Client_AddressBook0_Address2;
1049#line 1482
1050 return (retValue_acc);
1051 } else {
1052#line 1488
1053 retValue_acc = 0;
1054#line 1490
1055 return (retValue_acc);
1056 }
1057 }
1058 }
1059 } else {
1060#line 1492 "ClientLib.c"
1061 if (handle == 2) {
1062#line 275 "ClientLib.c"
1063 if (index == 0) {
1064#line 1500
1065 retValue_acc = __ste_Client_AddressBook1_Address0;
1066#line 1502
1067 return (retValue_acc);
1068 } else {
1069#line 1504
1070 if (index == 1) {
1071#line 1509
1072 retValue_acc = __ste_Client_AddressBook1_Address1;
1073#line 1511
1074 return (retValue_acc);
1075 } else {
1076#line 1513
1077 if (index == 2) {
1078#line 1518
1079 retValue_acc = __ste_Client_AddressBook1_Address2;
1080#line 1520
1081 return (retValue_acc);
1082 } else {
1083#line 1526
1084 retValue_acc = 0;
1085#line 1528
1086 return (retValue_acc);
1087 }
1088 }
1089 }
1090 } else {
1091#line 1530 "ClientLib.c"
1092 if (handle == 3) {
1093#line 285 "ClientLib.c"
1094 if (index == 0) {
1095#line 1538
1096 retValue_acc = __ste_Client_AddressBook2_Address0;
1097#line 1540
1098 return (retValue_acc);
1099 } else {
1100#line 1542
1101 if (index == 1) {
1102#line 1547
1103 retValue_acc = __ste_Client_AddressBook2_Address1;
1104#line 1549
1105 return (retValue_acc);
1106 } else {
1107#line 1551
1108 if (index == 2) {
1109#line 1556
1110 retValue_acc = __ste_Client_AddressBook2_Address2;
1111#line 1558
1112 return (retValue_acc);
1113 } else {
1114#line 1564
1115 retValue_acc = 0;
1116#line 1566
1117 return (retValue_acc);
1118 }
1119 }
1120 }
1121 } else {
1122#line 1572 "ClientLib.c"
1123 retValue_acc = 0;
1124#line 1574
1125 return (retValue_acc);
1126 }
1127 }
1128 }
1129#line 1581 "ClientLib.c"
1130 return (retValue_acc);
1131}
1132}
1133#line 291 "ClientLib.c"
1134void setClientAddressBookAddress(int handle , int index , int value )
1135{
1136
1137 {
1138#line 317
1139 if (handle == 1) {
1140#line 300
1141 if (index == 0) {
1142#line 294
1143 __ste_Client_AddressBook0_Address0 = value;
1144 } else {
1145#line 295
1146 if (index == 1) {
1147#line 296
1148 __ste_Client_AddressBook0_Address1 = value;
1149 } else {
1150#line 297
1151 if (index == 2) {
1152#line 298
1153 __ste_Client_AddressBook0_Address2 = value;
1154 } else {
1155
1156 }
1157 }
1158 }
1159 } else {
1160#line 299
1161 if (handle == 2) {
1162#line 308
1163 if (index == 0) {
1164#line 302
1165 __ste_Client_AddressBook1_Address0 = value;
1166 } else {
1167#line 303
1168 if (index == 1) {
1169#line 304
1170 __ste_Client_AddressBook1_Address1 = value;
1171 } else {
1172#line 305
1173 if (index == 2) {
1174#line 306
1175 __ste_Client_AddressBook1_Address2 = value;
1176 } else {
1177
1178 }
1179 }
1180 }
1181 } else {
1182#line 307
1183 if (handle == 3) {
1184#line 316
1185 if (index == 0) {
1186#line 310
1187 __ste_Client_AddressBook2_Address0 = value;
1188 } else {
1189#line 311
1190 if (index == 1) {
1191#line 312
1192 __ste_Client_AddressBook2_Address1 = value;
1193 } else {
1194#line 313
1195 if (index == 2) {
1196#line 314
1197 __ste_Client_AddressBook2_Address2 = value;
1198 } else {
1199
1200 }
1201 }
1202 }
1203 } else {
1204
1205 }
1206 }
1207 }
1208#line 1649 "ClientLib.c"
1209 return;
1210}
1211}
1212#line 319 "ClientLib.c"
1213int __ste_client_autoResponse0 = 0;
1214#line 321 "ClientLib.c"
1215int __ste_client_autoResponse1 = 0;
1216#line 323 "ClientLib.c"
1217int __ste_client_autoResponse2 = 0;
1218#line 326 "ClientLib.c"
1219int getClientAutoResponse(int handle )
1220{ int retValue_acc ;
1221
1222 {
1223#line 335 "ClientLib.c"
1224 if (handle == 1) {
1225#line 1676
1226 retValue_acc = __ste_client_autoResponse0;
1227#line 1678
1228 return (retValue_acc);
1229 } else {
1230#line 1680
1231 if (handle == 2) {
1232#line 1685
1233 retValue_acc = __ste_client_autoResponse1;
1234#line 1687
1235 return (retValue_acc);
1236 } else {
1237#line 1689
1238 if (handle == 3) {
1239#line 1694
1240 retValue_acc = __ste_client_autoResponse2;
1241#line 1696
1242 return (retValue_acc);
1243 } else {
1244#line 1702 "ClientLib.c"
1245 retValue_acc = -1;
1246#line 1704
1247 return (retValue_acc);
1248 }
1249 }
1250 }
1251#line 1711 "ClientLib.c"
1252 return (retValue_acc);
1253}
1254}
1255#line 338 "ClientLib.c"
1256void setClientAutoResponse(int handle , int value )
1257{
1258
1259 {
1260#line 346
1261 if (handle == 1) {
1262#line 340
1263 __ste_client_autoResponse0 = value;
1264 } else {
1265#line 341
1266 if (handle == 2) {
1267#line 342
1268 __ste_client_autoResponse1 = value;
1269 } else {
1270#line 343
1271 if (handle == 3) {
1272#line 344
1273 __ste_client_autoResponse2 = value;
1274 } else {
1275
1276 }
1277 }
1278 }
1279#line 1746 "ClientLib.c"
1280 return;
1281}
1282}
1283#line 348 "ClientLib.c"
1284int __ste_client_privateKey0 = 0;
1285#line 350 "ClientLib.c"
1286int __ste_client_privateKey1 = 0;
1287#line 352 "ClientLib.c"
1288int __ste_client_privateKey2 = 0;
1289#line 355 "ClientLib.c"
1290int getClientPrivateKey(int handle )
1291{ int retValue_acc ;
1292
1293 {
1294#line 364 "ClientLib.c"
1295 if (handle == 1) {
1296#line 1773
1297 retValue_acc = __ste_client_privateKey0;
1298#line 1775
1299 return (retValue_acc);
1300 } else {
1301#line 1777
1302 if (handle == 2) {
1303#line 1782
1304 retValue_acc = __ste_client_privateKey1;
1305#line 1784
1306 return (retValue_acc);
1307 } else {
1308#line 1786
1309 if (handle == 3) {
1310#line 1791
1311 retValue_acc = __ste_client_privateKey2;
1312#line 1793
1313 return (retValue_acc);
1314 } else {
1315#line 1799 "ClientLib.c"
1316 retValue_acc = 0;
1317#line 1801
1318 return (retValue_acc);
1319 }
1320 }
1321 }
1322#line 1808 "ClientLib.c"
1323 return (retValue_acc);
1324}
1325}
1326#line 367 "ClientLib.c"
1327void setClientPrivateKey(int handle , int value )
1328{
1329
1330 {
1331#line 375
1332 if (handle == 1) {
1333#line 369
1334 __ste_client_privateKey0 = value;
1335 } else {
1336#line 370
1337 if (handle == 2) {
1338#line 371
1339 __ste_client_privateKey1 = value;
1340 } else {
1341#line 372
1342 if (handle == 3) {
1343#line 373
1344 __ste_client_privateKey2 = value;
1345 } else {
1346
1347 }
1348 }
1349 }
1350#line 1843 "ClientLib.c"
1351 return;
1352}
1353}
1354#line 377 "ClientLib.c"
1355int __ste_ClientKeyring_size0 = 0;
1356#line 379 "ClientLib.c"
1357int __ste_ClientKeyring_size1 = 0;
1358#line 381 "ClientLib.c"
1359int __ste_ClientKeyring_size2 = 0;
1360#line 384 "ClientLib.c"
1361int getClientKeyringSize(int handle )
1362{ int retValue_acc ;
1363
1364 {
1365#line 393 "ClientLib.c"
1366 if (handle == 1) {
1367#line 1870
1368 retValue_acc = __ste_ClientKeyring_size0;
1369#line 1872
1370 return (retValue_acc);
1371 } else {
1372#line 1874
1373 if (handle == 2) {
1374#line 1879
1375 retValue_acc = __ste_ClientKeyring_size1;
1376#line 1881
1377 return (retValue_acc);
1378 } else {
1379#line 1883
1380 if (handle == 3) {
1381#line 1888
1382 retValue_acc = __ste_ClientKeyring_size2;
1383#line 1890
1384 return (retValue_acc);
1385 } else {
1386#line 1896 "ClientLib.c"
1387 retValue_acc = 0;
1388#line 1898
1389 return (retValue_acc);
1390 }
1391 }
1392 }
1393#line 1905 "ClientLib.c"
1394 return (retValue_acc);
1395}
1396}
1397#line 396 "ClientLib.c"
1398void setClientKeyringSize(int handle , int value )
1399{
1400
1401 {
1402#line 404
1403 if (handle == 1) {
1404#line 398
1405 __ste_ClientKeyring_size0 = value;
1406 } else {
1407#line 399
1408 if (handle == 2) {
1409#line 400
1410 __ste_ClientKeyring_size1 = value;
1411 } else {
1412#line 401
1413 if (handle == 3) {
1414#line 402
1415 __ste_ClientKeyring_size2 = value;
1416 } else {
1417
1418 }
1419 }
1420 }
1421#line 1940 "ClientLib.c"
1422 return;
1423}
1424}
1425#line 406 "ClientLib.c"
1426int createClientKeyringEntry(int handle )
1427{ int retValue_acc ;
1428 int size ;
1429 int tmp ;
1430 int __cil_tmp5 ;
1431
1432 {
1433 {
1434#line 407
1435 tmp = getClientKeyringSize(handle);
1436#line 407
1437 size = tmp;
1438 }
1439#line 408 "ClientLib.c"
1440 if (size < 2) {
1441 {
1442#line 409 "ClientLib.c"
1443 __cil_tmp5 = size + 1;
1444#line 409
1445 setClientKeyringSize(handle, __cil_tmp5);
1446#line 1967 "ClientLib.c"
1447 retValue_acc = size + 1;
1448 }
1449#line 1969
1450 return (retValue_acc);
1451 } else {
1452#line 1973 "ClientLib.c"
1453 retValue_acc = -1;
1454#line 1975
1455 return (retValue_acc);
1456 }
1457#line 1982 "ClientLib.c"
1458 return (retValue_acc);
1459}
1460}
1461#line 414 "ClientLib.c"
1462int __ste_Client_Keyring0_User0 = 0;
1463#line 416 "ClientLib.c"
1464int __ste_Client_Keyring0_User1 = 0;
1465#line 418 "ClientLib.c"
1466int __ste_Client_Keyring0_User2 = 0;
1467#line 420 "ClientLib.c"
1468int __ste_Client_Keyring1_User0 = 0;
1469#line 422 "ClientLib.c"
1470int __ste_Client_Keyring1_User1 = 0;
1471#line 424 "ClientLib.c"
1472int __ste_Client_Keyring1_User2 = 0;
1473#line 426 "ClientLib.c"
1474int __ste_Client_Keyring2_User0 = 0;
1475#line 428 "ClientLib.c"
1476int __ste_Client_Keyring2_User1 = 0;
1477#line 430 "ClientLib.c"
1478int __ste_Client_Keyring2_User2 = 0;
1479#line 433 "ClientLib.c"
1480int getClientKeyringUser(int handle , int index )
1481{ int retValue_acc ;
1482
1483 {
1484#line 466
1485 if (handle == 1) {
1486#line 443 "ClientLib.c"
1487 if (index == 0) {
1488#line 2028
1489 retValue_acc = __ste_Client_Keyring0_User0;
1490#line 2030
1491 return (retValue_acc);
1492 } else {
1493#line 2032
1494 if (index == 1) {
1495#line 2037
1496 retValue_acc = __ste_Client_Keyring0_User1;
1497#line 2039
1498 return (retValue_acc);
1499 } else {
1500#line 2045
1501 retValue_acc = 0;
1502#line 2047
1503 return (retValue_acc);
1504 }
1505 }
1506 } else {
1507#line 2049 "ClientLib.c"
1508 if (handle == 2) {
1509#line 453 "ClientLib.c"
1510 if (index == 0) {
1511#line 2057
1512 retValue_acc = __ste_Client_Keyring1_User0;
1513#line 2059
1514 return (retValue_acc);
1515 } else {
1516#line 2061
1517 if (index == 1) {
1518#line 2066
1519 retValue_acc = __ste_Client_Keyring1_User1;
1520#line 2068
1521 return (retValue_acc);
1522 } else {
1523#line 2074
1524 retValue_acc = 0;
1525#line 2076
1526 return (retValue_acc);
1527 }
1528 }
1529 } else {
1530#line 2078 "ClientLib.c"
1531 if (handle == 3) {
1532#line 463 "ClientLib.c"
1533 if (index == 0) {
1534#line 2086
1535 retValue_acc = __ste_Client_Keyring2_User0;
1536#line 2088
1537 return (retValue_acc);
1538 } else {
1539#line 2090
1540 if (index == 1) {
1541#line 2095
1542 retValue_acc = __ste_Client_Keyring2_User1;
1543#line 2097
1544 return (retValue_acc);
1545 } else {
1546#line 2103
1547 retValue_acc = 0;
1548#line 2105
1549 return (retValue_acc);
1550 }
1551 }
1552 } else {
1553#line 2111 "ClientLib.c"
1554 retValue_acc = 0;
1555#line 2113
1556 return (retValue_acc);
1557 }
1558 }
1559 }
1560#line 2120 "ClientLib.c"
1561 return (retValue_acc);
1562}
1563}
1564#line 473 "ClientLib.c"
1565void setClientKeyringUser(int handle , int index , int value )
1566{
1567
1568 {
1569#line 499
1570 if (handle == 1) {
1571#line 482
1572 if (index == 0) {
1573#line 476
1574 __ste_Client_Keyring0_User0 = value;
1575 } else {
1576#line 477
1577 if (index == 1) {
1578#line 478
1579 __ste_Client_Keyring0_User1 = value;
1580 } else {
1581
1582 }
1583 }
1584 } else {
1585#line 479
1586 if (handle == 2) {
1587#line 490
1588 if (index == 0) {
1589#line 484
1590 __ste_Client_Keyring1_User0 = value;
1591 } else {
1592#line 485
1593 if (index == 1) {
1594#line 486
1595 __ste_Client_Keyring1_User1 = value;
1596 } else {
1597
1598 }
1599 }
1600 } else {
1601#line 487
1602 if (handle == 3) {
1603#line 498
1604 if (index == 0) {
1605#line 492
1606 __ste_Client_Keyring2_User0 = value;
1607 } else {
1608#line 493
1609 if (index == 1) {
1610#line 494
1611 __ste_Client_Keyring2_User1 = value;
1612 } else {
1613
1614 }
1615 }
1616 } else {
1617
1618 }
1619 }
1620 }
1621#line 2176 "ClientLib.c"
1622 return;
1623}
1624}
1625#line 501 "ClientLib.c"
1626int __ste_Client_Keyring0_PublicKey0 = 0;
1627#line 503 "ClientLib.c"
1628int __ste_Client_Keyring0_PublicKey1 = 0;
1629#line 505 "ClientLib.c"
1630int __ste_Client_Keyring0_PublicKey2 = 0;
1631#line 507 "ClientLib.c"
1632int __ste_Client_Keyring1_PublicKey0 = 0;
1633#line 509 "ClientLib.c"
1634int __ste_Client_Keyring1_PublicKey1 = 0;
1635#line 511 "ClientLib.c"
1636int __ste_Client_Keyring1_PublicKey2 = 0;
1637#line 513 "ClientLib.c"
1638int __ste_Client_Keyring2_PublicKey0 = 0;
1639#line 515 "ClientLib.c"
1640int __ste_Client_Keyring2_PublicKey1 = 0;
1641#line 517 "ClientLib.c"
1642int __ste_Client_Keyring2_PublicKey2 = 0;
1643#line 520 "ClientLib.c"
1644int getClientKeyringPublicKey(int handle , int index )
1645{ int retValue_acc ;
1646
1647 {
1648#line 553
1649 if (handle == 1) {
1650#line 530 "ClientLib.c"
1651 if (index == 0) {
1652#line 2218
1653 retValue_acc = __ste_Client_Keyring0_PublicKey0;
1654#line 2220
1655 return (retValue_acc);
1656 } else {
1657#line 2222
1658 if (index == 1) {
1659#line 2227
1660 retValue_acc = __ste_Client_Keyring0_PublicKey1;
1661#line 2229
1662 return (retValue_acc);
1663 } else {
1664#line 2235
1665 retValue_acc = 0;
1666#line 2237
1667 return (retValue_acc);
1668 }
1669 }
1670 } else {
1671#line 2239 "ClientLib.c"
1672 if (handle == 2) {
1673#line 540 "ClientLib.c"
1674 if (index == 0) {
1675#line 2247
1676 retValue_acc = __ste_Client_Keyring1_PublicKey0;
1677#line 2249
1678 return (retValue_acc);
1679 } else {
1680#line 2251
1681 if (index == 1) {
1682#line 2256
1683 retValue_acc = __ste_Client_Keyring1_PublicKey1;
1684#line 2258
1685 return (retValue_acc);
1686 } else {
1687#line 2264
1688 retValue_acc = 0;
1689#line 2266
1690 return (retValue_acc);
1691 }
1692 }
1693 } else {
1694#line 2268 "ClientLib.c"
1695 if (handle == 3) {
1696#line 550 "ClientLib.c"
1697 if (index == 0) {
1698#line 2276
1699 retValue_acc = __ste_Client_Keyring2_PublicKey0;
1700#line 2278
1701 return (retValue_acc);
1702 } else {
1703#line 2280
1704 if (index == 1) {
1705#line 2285
1706 retValue_acc = __ste_Client_Keyring2_PublicKey1;
1707#line 2287
1708 return (retValue_acc);
1709 } else {
1710#line 2293
1711 retValue_acc = 0;
1712#line 2295
1713 return (retValue_acc);
1714 }
1715 }
1716 } else {
1717#line 2301 "ClientLib.c"
1718 retValue_acc = 0;
1719#line 2303
1720 return (retValue_acc);
1721 }
1722 }
1723 }
1724#line 2310 "ClientLib.c"
1725 return (retValue_acc);
1726}
1727}
1728#line 557 "ClientLib.c"
1729int findPublicKey(int handle , int userid )
1730{ int retValue_acc ;
1731
1732 {
1733#line 591
1734 if (handle == 1) {
1735#line 568 "ClientLib.c"
1736 if (userid == __ste_Client_Keyring0_User0) {
1737#line 2338
1738 retValue_acc = __ste_Client_Keyring0_PublicKey0;
1739#line 2340
1740 return (retValue_acc);
1741 } else {
1742#line 2342
1743 if (userid == __ste_Client_Keyring0_User1) {
1744#line 2347
1745 retValue_acc = __ste_Client_Keyring0_PublicKey1;
1746#line 2349
1747 return (retValue_acc);
1748 } else {
1749#line 2355
1750 retValue_acc = 0;
1751#line 2357
1752 return (retValue_acc);
1753 }
1754 }
1755 } else {
1756#line 2359 "ClientLib.c"
1757 if (handle == 2) {
1758#line 578 "ClientLib.c"
1759 if (userid == __ste_Client_Keyring1_User0) {
1760#line 2367
1761 retValue_acc = __ste_Client_Keyring1_PublicKey0;
1762#line 2369
1763 return (retValue_acc);
1764 } else {
1765#line 2371
1766 if (userid == __ste_Client_Keyring1_User1) {
1767#line 2376
1768 retValue_acc = __ste_Client_Keyring1_PublicKey1;
1769#line 2378
1770 return (retValue_acc);
1771 } else {
1772#line 2384
1773 retValue_acc = 0;
1774#line 2386
1775 return (retValue_acc);
1776 }
1777 }
1778 } else {
1779#line 2388 "ClientLib.c"
1780 if (handle == 3) {
1781#line 588 "ClientLib.c"
1782 if (userid == __ste_Client_Keyring2_User0) {
1783#line 2396
1784 retValue_acc = __ste_Client_Keyring2_PublicKey0;
1785#line 2398
1786 return (retValue_acc);
1787 } else {
1788#line 2400
1789 if (userid == __ste_Client_Keyring2_User1) {
1790#line 2405
1791 retValue_acc = __ste_Client_Keyring2_PublicKey1;
1792#line 2407
1793 return (retValue_acc);
1794 } else {
1795#line 2413
1796 retValue_acc = 0;
1797#line 2415
1798 return (retValue_acc);
1799 }
1800 }
1801 } else {
1802#line 2421 "ClientLib.c"
1803 retValue_acc = 0;
1804#line 2423
1805 return (retValue_acc);
1806 }
1807 }
1808 }
1809#line 2430 "ClientLib.c"
1810 return (retValue_acc);
1811}
1812}
1813#line 595 "ClientLib.c"
1814void setClientKeyringPublicKey(int handle , int index , int value )
1815{
1816
1817 {
1818#line 621
1819 if (handle == 1) {
1820#line 604
1821 if (index == 0) {
1822#line 598
1823 __ste_Client_Keyring0_PublicKey0 = value;
1824 } else {
1825#line 599
1826 if (index == 1) {
1827#line 600
1828 __ste_Client_Keyring0_PublicKey1 = value;
1829 } else {
1830
1831 }
1832 }
1833 } else {
1834#line 601
1835 if (handle == 2) {
1836#line 612
1837 if (index == 0) {
1838#line 606
1839 __ste_Client_Keyring1_PublicKey0 = value;
1840 } else {
1841#line 607
1842 if (index == 1) {
1843#line 608
1844 __ste_Client_Keyring1_PublicKey1 = value;
1845 } else {
1846
1847 }
1848 }
1849 } else {
1850#line 609
1851 if (handle == 3) {
1852#line 620
1853 if (index == 0) {
1854#line 614
1855 __ste_Client_Keyring2_PublicKey0 = value;
1856 } else {
1857#line 615
1858 if (index == 1) {
1859#line 616
1860 __ste_Client_Keyring2_PublicKey1 = value;
1861 } else {
1862
1863 }
1864 }
1865 } else {
1866
1867 }
1868 }
1869 }
1870#line 2486 "ClientLib.c"
1871 return;
1872}
1873}
1874#line 623 "ClientLib.c"
1875int __ste_client_forwardReceiver0 = 0;
1876#line 625 "ClientLib.c"
1877int __ste_client_forwardReceiver1 = 0;
1878#line 627 "ClientLib.c"
1879int __ste_client_forwardReceiver2 = 0;
1880#line 629 "ClientLib.c"
1881int __ste_client_forwardReceiver3 = 0;
1882#line 631 "ClientLib.c"
1883int getClientForwardReceiver(int handle )
1884{ int retValue_acc ;
1885
1886 {
1887#line 640 "ClientLib.c"
1888 if (handle == 1) {
1889#line 2515
1890 retValue_acc = __ste_client_forwardReceiver0;
1891#line 2517
1892 return (retValue_acc);
1893 } else {
1894#line 2519
1895 if (handle == 2) {
1896#line 2524
1897 retValue_acc = __ste_client_forwardReceiver1;
1898#line 2526
1899 return (retValue_acc);
1900 } else {
1901#line 2528
1902 if (handle == 3) {
1903#line 2533
1904 retValue_acc = __ste_client_forwardReceiver2;
1905#line 2535
1906 return (retValue_acc);
1907 } else {
1908#line 2541 "ClientLib.c"
1909 retValue_acc = 0;
1910#line 2543
1911 return (retValue_acc);
1912 }
1913 }
1914 }
1915#line 2550 "ClientLib.c"
1916 return (retValue_acc);
1917}
1918}
1919#line 643 "ClientLib.c"
1920void setClientForwardReceiver(int handle , int value )
1921{
1922
1923 {
1924#line 651
1925 if (handle == 1) {
1926#line 645
1927 __ste_client_forwardReceiver0 = value;
1928 } else {
1929#line 646
1930 if (handle == 2) {
1931#line 647
1932 __ste_client_forwardReceiver1 = value;
1933 } else {
1934#line 648
1935 if (handle == 3) {
1936#line 649
1937 __ste_client_forwardReceiver2 = value;
1938 } else {
1939
1940 }
1941 }
1942 }
1943#line 2585 "ClientLib.c"
1944 return;
1945}
1946}
1947#line 653 "ClientLib.c"
1948int __ste_client_idCounter0 = 0;
1949#line 655 "ClientLib.c"
1950int __ste_client_idCounter1 = 0;
1951#line 657 "ClientLib.c"
1952int __ste_client_idCounter2 = 0;
1953#line 660 "ClientLib.c"
1954int getClientId(int handle )
1955{ int retValue_acc ;
1956
1957 {
1958#line 669 "ClientLib.c"
1959 if (handle == 1) {
1960#line 2612
1961 retValue_acc = __ste_client_idCounter0;
1962#line 2614
1963 return (retValue_acc);
1964 } else {
1965#line 2616
1966 if (handle == 2) {
1967#line 2621
1968 retValue_acc = __ste_client_idCounter1;
1969#line 2623
1970 return (retValue_acc);
1971 } else {
1972#line 2625
1973 if (handle == 3) {
1974#line 2630
1975 retValue_acc = __ste_client_idCounter2;
1976#line 2632
1977 return (retValue_acc);
1978 } else {
1979#line 2638 "ClientLib.c"
1980 retValue_acc = 0;
1981#line 2640
1982 return (retValue_acc);
1983 }
1984 }
1985 }
1986#line 2647 "ClientLib.c"
1987 return (retValue_acc);
1988}
1989}
1990#line 672 "ClientLib.c"
1991void setClientId(int handle , int value )
1992{
1993
1994 {
1995#line 680
1996 if (handle == 1) {
1997#line 674
1998 __ste_client_idCounter0 = value;
1999 } else {
2000#line 675
2001 if (handle == 2) {
2002#line 676
2003 __ste_client_idCounter1 = value;
2004 } else {
2005#line 677
2006 if (handle == 3) {
2007#line 678
2008 __ste_client_idCounter2 = value;
2009 } else {
2010
2011 }
2012 }
2013 }
2014#line 2682 "ClientLib.c"
2015 return;
2016}
2017}
2018#line 1 "EmailLib.o"
2019#pragma merger(0,"EmailLib.i","")
2020#line 4 "EmailLib.h"
2021int initEmail(void) ;
2022#line 6
2023int getEmailId(int handle ) ;
2024#line 8
2025void setEmailId(int handle , int value ) ;
2026#line 10
2027int getEmailFrom(int handle ) ;
2028#line 12
2029void setEmailFrom(int handle , int value ) ;
2030#line 14
2031int getEmailTo(int handle ) ;
2032#line 16
2033void setEmailTo(int handle , int value ) ;
2034#line 18
2035char *getEmailSubject(int handle ) ;
2036#line 20
2037void setEmailSubject(int handle , char *value ) ;
2038#line 22
2039char *getEmailBody(int handle ) ;
2040#line 24
2041void setEmailBody(int handle , char *value ) ;
2042#line 26
2043int isEncrypted(int handle ) ;
2044#line 28
2045void setEmailIsEncrypted(int handle , int value ) ;
2046#line 30
2047int getEmailEncryptionKey(int handle ) ;
2048#line 32
2049void setEmailEncryptionKey(int handle , int value ) ;
2050#line 34
2051int isSigned(int handle ) ;
2052#line 36
2053void setEmailIsSigned(int handle , int value ) ;
2054#line 38
2055int getEmailSignKey(int handle ) ;
2056#line 40
2057void setEmailSignKey(int handle , int value ) ;
2058#line 42
2059int isVerified(int handle ) ;
2060#line 44
2061void setEmailIsSignatureVerified(int handle , int value ) ;
2062#line 5 "EmailLib.c"
2063int __ste_Email_counter = 0;
2064#line 7 "EmailLib.c"
2065int initEmail(void)
2066{ int retValue_acc ;
2067
2068 {
2069#line 12 "EmailLib.c"
2070 if (__ste_Email_counter < 2) {
2071#line 670
2072 __ste_Email_counter = __ste_Email_counter + 1;
2073#line 670
2074 retValue_acc = __ste_Email_counter;
2075#line 672
2076 return (retValue_acc);
2077 } else {
2078#line 678 "EmailLib.c"
2079 retValue_acc = -1;
2080#line 680
2081 return (retValue_acc);
2082 }
2083#line 687 "EmailLib.c"
2084 return (retValue_acc);
2085}
2086}
2087#line 15 "EmailLib.c"
2088int __ste_email_id0 = 0;
2089#line 17 "EmailLib.c"
2090int __ste_email_id1 = 0;
2091#line 19 "EmailLib.c"
2092int getEmailId(int handle )
2093{ int retValue_acc ;
2094
2095 {
2096#line 26 "EmailLib.c"
2097 if (handle == 1) {
2098#line 716
2099 retValue_acc = __ste_email_id0;
2100#line 718
2101 return (retValue_acc);
2102 } else {
2103#line 720
2104 if (handle == 2) {
2105#line 725
2106 retValue_acc = __ste_email_id1;
2107#line 727
2108 return (retValue_acc);
2109 } else {
2110#line 733 "EmailLib.c"
2111 retValue_acc = 0;
2112#line 735
2113 return (retValue_acc);
2114 }
2115 }
2116#line 742 "EmailLib.c"
2117 return (retValue_acc);
2118}
2119}
2120#line 29 "EmailLib.c"
2121void setEmailId(int handle , int value )
2122{
2123
2124 {
2125#line 35
2126 if (handle == 1) {
2127#line 31
2128 __ste_email_id0 = value;
2129 } else {
2130#line 32
2131 if (handle == 2) {
2132#line 33
2133 __ste_email_id1 = value;
2134 } else {
2135
2136 }
2137 }
2138#line 773 "EmailLib.c"
2139 return;
2140}
2141}
2142#line 37 "EmailLib.c"
2143int __ste_email_from0 = 0;
2144#line 39 "EmailLib.c"
2145int __ste_email_from1 = 0;
2146#line 41 "EmailLib.c"
2147int getEmailFrom(int handle )
2148{ int retValue_acc ;
2149
2150 {
2151#line 48 "EmailLib.c"
2152 if (handle == 1) {
2153#line 798
2154 retValue_acc = __ste_email_from0;
2155#line 800
2156 return (retValue_acc);
2157 } else {
2158#line 802
2159 if (handle == 2) {
2160#line 807
2161 retValue_acc = __ste_email_from1;
2162#line 809
2163 return (retValue_acc);
2164 } else {
2165#line 815 "EmailLib.c"
2166 retValue_acc = 0;
2167#line 817
2168 return (retValue_acc);
2169 }
2170 }
2171#line 824 "EmailLib.c"
2172 return (retValue_acc);
2173}
2174}
2175#line 51 "EmailLib.c"
2176void setEmailFrom(int handle , int value )
2177{
2178
2179 {
2180#line 57
2181 if (handle == 1) {
2182#line 53
2183 __ste_email_from0 = value;
2184 } else {
2185#line 54
2186 if (handle == 2) {
2187#line 55
2188 __ste_email_from1 = value;
2189 } else {
2190
2191 }
2192 }
2193#line 855 "EmailLib.c"
2194 return;
2195}
2196}
2197#line 59 "EmailLib.c"
2198int __ste_email_to0 = 0;
2199#line 61 "EmailLib.c"
2200int __ste_email_to1 = 0;
2201#line 63 "EmailLib.c"
2202int getEmailTo(int handle )
2203{ int retValue_acc ;
2204
2205 {
2206#line 70 "EmailLib.c"
2207 if (handle == 1) {
2208#line 880
2209 retValue_acc = __ste_email_to0;
2210#line 882
2211 return (retValue_acc);
2212 } else {
2213#line 884
2214 if (handle == 2) {
2215#line 889
2216 retValue_acc = __ste_email_to1;
2217#line 891
2218 return (retValue_acc);
2219 } else {
2220#line 897 "EmailLib.c"
2221 retValue_acc = 0;
2222#line 899
2223 return (retValue_acc);
2224 }
2225 }
2226#line 906 "EmailLib.c"
2227 return (retValue_acc);
2228}
2229}
2230#line 73 "EmailLib.c"
2231void setEmailTo(int handle , int value )
2232{
2233
2234 {
2235#line 79
2236 if (handle == 1) {
2237#line 75
2238 __ste_email_to0 = value;
2239 } else {
2240#line 76
2241 if (handle == 2) {
2242#line 77
2243 __ste_email_to1 = value;
2244 } else {
2245
2246 }
2247 }
2248#line 937 "EmailLib.c"
2249 return;
2250}
2251}
2252#line 81 "EmailLib.c"
2253char *__ste_email_subject0 ;
2254#line 83 "EmailLib.c"
2255char *__ste_email_subject1 ;
2256#line 85 "EmailLib.c"
2257char *getEmailSubject(int handle )
2258{ char *retValue_acc ;
2259 void *__cil_tmp3 ;
2260
2261 {
2262#line 92 "EmailLib.c"
2263 if (handle == 1) {
2264#line 962
2265 retValue_acc = __ste_email_subject0;
2266#line 964
2267 return (retValue_acc);
2268 } else {
2269#line 966
2270 if (handle == 2) {
2271#line 971
2272 retValue_acc = __ste_email_subject1;
2273#line 973
2274 return (retValue_acc);
2275 } else {
2276#line 979 "EmailLib.c"
2277 __cil_tmp3 = (void *)0;
2278#line 979
2279 retValue_acc = (char *)__cil_tmp3;
2280#line 981
2281 return (retValue_acc);
2282 }
2283 }
2284#line 988 "EmailLib.c"
2285 return (retValue_acc);
2286}
2287}
2288#line 95 "EmailLib.c"
2289void setEmailSubject(int handle , char *value )
2290{
2291
2292 {
2293#line 101
2294 if (handle == 1) {
2295#line 97
2296 __ste_email_subject0 = value;
2297 } else {
2298#line 98
2299 if (handle == 2) {
2300#line 99
2301 __ste_email_subject1 = value;
2302 } else {
2303
2304 }
2305 }
2306#line 1019 "EmailLib.c"
2307 return;
2308}
2309}
2310#line 103 "EmailLib.c"
2311char *__ste_email_body0 = (char *)0;
2312#line 105 "EmailLib.c"
2313char *__ste_email_body1 = (char *)0;
2314#line 107 "EmailLib.c"
2315char *getEmailBody(int handle )
2316{ char *retValue_acc ;
2317 void *__cil_tmp3 ;
2318
2319 {
2320#line 114 "EmailLib.c"
2321 if (handle == 1) {
2322#line 1044
2323 retValue_acc = __ste_email_body0;
2324#line 1046
2325 return (retValue_acc);
2326 } else {
2327#line 1048
2328 if (handle == 2) {
2329#line 1053
2330 retValue_acc = __ste_email_body1;
2331#line 1055
2332 return (retValue_acc);
2333 } else {
2334#line 1061 "EmailLib.c"
2335 __cil_tmp3 = (void *)0;
2336#line 1061
2337 retValue_acc = (char *)__cil_tmp3;
2338#line 1063
2339 return (retValue_acc);
2340 }
2341 }
2342#line 1070 "EmailLib.c"
2343 return (retValue_acc);
2344}
2345}
2346#line 117 "EmailLib.c"
2347void setEmailBody(int handle , char *value )
2348{
2349
2350 {
2351#line 123
2352 if (handle == 1) {
2353#line 119
2354 __ste_email_body0 = value;
2355 } else {
2356#line 120
2357 if (handle == 2) {
2358#line 121
2359 __ste_email_body1 = value;
2360 } else {
2361
2362 }
2363 }
2364#line 1101 "EmailLib.c"
2365 return;
2366}
2367}
2368#line 125 "EmailLib.c"
2369int __ste_email_isEncrypted0 = 0;
2370#line 127 "EmailLib.c"
2371int __ste_email_isEncrypted1 = 0;
2372#line 129 "EmailLib.c"
2373int isEncrypted(int handle )
2374{ int retValue_acc ;
2375
2376 {
2377#line 136 "EmailLib.c"
2378 if (handle == 1) {
2379#line 1126
2380 retValue_acc = __ste_email_isEncrypted0;
2381#line 1128
2382 return (retValue_acc);
2383 } else {
2384#line 1130
2385 if (handle == 2) {
2386#line 1135
2387 retValue_acc = __ste_email_isEncrypted1;
2388#line 1137
2389 return (retValue_acc);
2390 } else {
2391#line 1143 "EmailLib.c"
2392 retValue_acc = 0;
2393#line 1145
2394 return (retValue_acc);
2395 }
2396 }
2397#line 1152 "EmailLib.c"
2398 return (retValue_acc);
2399}
2400}
2401#line 139 "EmailLib.c"
2402void setEmailIsEncrypted(int handle , int value )
2403{
2404
2405 {
2406#line 145
2407 if (handle == 1) {
2408#line 141
2409 __ste_email_isEncrypted0 = value;
2410 } else {
2411#line 142
2412 if (handle == 2) {
2413#line 143
2414 __ste_email_isEncrypted1 = value;
2415 } else {
2416
2417 }
2418 }
2419#line 1183 "EmailLib.c"
2420 return;
2421}
2422}
2423#line 147 "EmailLib.c"
2424int __ste_email_encryptionKey0 = 0;
2425#line 149 "EmailLib.c"
2426int __ste_email_encryptionKey1 = 0;
2427#line 151 "EmailLib.c"
2428int getEmailEncryptionKey(int handle )
2429{ int retValue_acc ;
2430
2431 {
2432#line 158 "EmailLib.c"
2433 if (handle == 1) {
2434#line 1208
2435 retValue_acc = __ste_email_encryptionKey0;
2436#line 1210
2437 return (retValue_acc);
2438 } else {
2439#line 1212
2440 if (handle == 2) {
2441#line 1217
2442 retValue_acc = __ste_email_encryptionKey1;
2443#line 1219
2444 return (retValue_acc);
2445 } else {
2446#line 1225 "EmailLib.c"
2447 retValue_acc = 0;
2448#line 1227
2449 return (retValue_acc);
2450 }
2451 }
2452#line 1234 "EmailLib.c"
2453 return (retValue_acc);
2454}
2455}
2456#line 161 "EmailLib.c"
2457void setEmailEncryptionKey(int handle , int value )
2458{
2459
2460 {
2461#line 167
2462 if (handle == 1) {
2463#line 163
2464 __ste_email_encryptionKey0 = value;
2465 } else {
2466#line 164
2467 if (handle == 2) {
2468#line 165
2469 __ste_email_encryptionKey1 = value;
2470 } else {
2471
2472 }
2473 }
2474#line 1265 "EmailLib.c"
2475 return;
2476}
2477}
2478#line 169 "EmailLib.c"
2479int __ste_email_isSigned0 = 0;
2480#line 171 "EmailLib.c"
2481int __ste_email_isSigned1 = 0;
2482#line 173 "EmailLib.c"
2483int isSigned(int handle )
2484{ int retValue_acc ;
2485
2486 {
2487#line 180 "EmailLib.c"
2488 if (handle == 1) {
2489#line 1290
2490 retValue_acc = __ste_email_isSigned0;
2491#line 1292
2492 return (retValue_acc);
2493 } else {
2494#line 1294
2495 if (handle == 2) {
2496#line 1299
2497 retValue_acc = __ste_email_isSigned1;
2498#line 1301
2499 return (retValue_acc);
2500 } else {
2501#line 1307 "EmailLib.c"
2502 retValue_acc = 0;
2503#line 1309
2504 return (retValue_acc);
2505 }
2506 }
2507#line 1316 "EmailLib.c"
2508 return (retValue_acc);
2509}
2510}
2511#line 183 "EmailLib.c"
2512void setEmailIsSigned(int handle , int value )
2513{
2514
2515 {
2516#line 189
2517 if (handle == 1) {
2518#line 185
2519 __ste_email_isSigned0 = value;
2520 } else {
2521#line 186
2522 if (handle == 2) {
2523#line 187
2524 __ste_email_isSigned1 = value;
2525 } else {
2526
2527 }
2528 }
2529#line 1347 "EmailLib.c"
2530 return;
2531}
2532}
2533#line 191 "EmailLib.c"
2534int __ste_email_signKey0 = 0;
2535#line 193 "EmailLib.c"
2536int __ste_email_signKey1 = 0;
2537#line 195 "EmailLib.c"
2538int getEmailSignKey(int handle )
2539{ int retValue_acc ;
2540
2541 {
2542#line 202 "EmailLib.c"
2543 if (handle == 1) {
2544#line 1372
2545 retValue_acc = __ste_email_signKey0;
2546#line 1374
2547 return (retValue_acc);
2548 } else {
2549#line 1376
2550 if (handle == 2) {
2551#line 1381
2552 retValue_acc = __ste_email_signKey1;
2553#line 1383
2554 return (retValue_acc);
2555 } else {
2556#line 1389 "EmailLib.c"
2557 retValue_acc = 0;
2558#line 1391
2559 return (retValue_acc);
2560 }
2561 }
2562#line 1398 "EmailLib.c"
2563 return (retValue_acc);
2564}
2565}
2566#line 205 "EmailLib.c"
2567void setEmailSignKey(int handle , int value )
2568{
2569
2570 {
2571#line 211
2572 if (handle == 1) {
2573#line 207
2574 __ste_email_signKey0 = value;
2575 } else {
2576#line 208
2577 if (handle == 2) {
2578#line 209
2579 __ste_email_signKey1 = value;
2580 } else {
2581
2582 }
2583 }
2584#line 1429 "EmailLib.c"
2585 return;
2586}
2587}
2588#line 213 "EmailLib.c"
2589int __ste_email_isSignatureVerified0 ;
2590#line 215 "EmailLib.c"
2591int __ste_email_isSignatureVerified1 ;
2592#line 217 "EmailLib.c"
2593int isVerified(int handle )
2594{ int retValue_acc ;
2595
2596 {
2597#line 224 "EmailLib.c"
2598 if (handle == 1) {
2599#line 1454
2600 retValue_acc = __ste_email_isSignatureVerified0;
2601#line 1456
2602 return (retValue_acc);
2603 } else {
2604#line 1458
2605 if (handle == 2) {
2606#line 1463
2607 retValue_acc = __ste_email_isSignatureVerified1;
2608#line 1465
2609 return (retValue_acc);
2610 } else {
2611#line 1471 "EmailLib.c"
2612 retValue_acc = 0;
2613#line 1473
2614 return (retValue_acc);
2615 }
2616 }
2617#line 1480 "EmailLib.c"
2618 return (retValue_acc);
2619}
2620}
2621#line 227 "EmailLib.c"
2622void setEmailIsSignatureVerified(int handle , int value )
2623{
2624
2625 {
2626#line 233
2627 if (handle == 1) {
2628#line 229
2629 __ste_email_isSignatureVerified0 = value;
2630 } else {
2631#line 230
2632 if (handle == 2) {
2633#line 231
2634 __ste_email_isSignatureVerified1 = value;
2635 } else {
2636
2637 }
2638 }
2639#line 1511 "EmailLib.c"
2640 return;
2641}
2642}
2643#line 1 "wsllib_check.o"
2644#pragma merger(0,"wsllib_check.i","")
2645#line 3 "wsllib_check.c"
2646void __automaton_fail(void)
2647{
2648
2649 {
2650 goto ERROR;
2651 ERROR: ;
2652#line 53 "wsllib_check.c"
2653 return;
2654}
2655}
2656#line 1 "Util.o"
2657#pragma merger(0,"Util.i","")
2658#line 359 "/usr/include/stdio.h"
2659extern int printf(char const * __restrict __format , ...) ;
2660#line 1 "Util.h"
2661int prompt(char *msg ) ;
2662#line 9 "Util.c"
2663int prompt(char *msg )
2664{ int retValue_acc ;
2665 int retval ;
2666 char const * __restrict __cil_tmp4 ;
2667
2668 {
2669 {
2670#line 10
2671 __cil_tmp4 = (char const * __restrict )"%s\n";
2672#line 10
2673 printf(__cil_tmp4, msg);
2674#line 518 "Util.c"
2675 retValue_acc = retval;
2676 }
2677#line 520
2678 return (retValue_acc);
2679#line 527
2680 return (retValue_acc);
2681}
2682}
2683#line 1 "libacc.o"
2684#pragma merger(0,"libacc.i","")
2685#line 73 "/usr/include/assert.h"
2686extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
2687 char const *__file ,
2688 unsigned int __line ,
2689 char const *__function ) ;
2690#line 471 "/usr/include/stdlib.h"
2691extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
2692#line 488
2693extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
2694#line 32 "libacc.c"
2695void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
2696 int ) ,
2697 int val )
2698{ struct __UTAC__EXCEPTION *excep ;
2699 struct __UTAC__CFLOW_FUNC *cf ;
2700 void *tmp ;
2701 unsigned long __cil_tmp7 ;
2702 unsigned long __cil_tmp8 ;
2703 unsigned long __cil_tmp9 ;
2704 unsigned long __cil_tmp10 ;
2705 unsigned long __cil_tmp11 ;
2706 unsigned long __cil_tmp12 ;
2707 unsigned long __cil_tmp13 ;
2708 unsigned long __cil_tmp14 ;
2709 int (**mem_15)(int , int ) ;
2710 int *mem_16 ;
2711 struct __UTAC__CFLOW_FUNC **mem_17 ;
2712 struct __UTAC__CFLOW_FUNC **mem_18 ;
2713 struct __UTAC__CFLOW_FUNC **mem_19 ;
2714
2715 {
2716 {
2717#line 33
2718 excep = (struct __UTAC__EXCEPTION *)exception;
2719#line 34
2720 tmp = malloc(24UL);
2721#line 34
2722 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
2723#line 36
2724 mem_15 = (int (**)(int , int ))cf;
2725#line 36
2726 *mem_15 = cflow_func;
2727#line 37
2728 __cil_tmp7 = (unsigned long )cf;
2729#line 37
2730 __cil_tmp8 = __cil_tmp7 + 8;
2731#line 37
2732 mem_16 = (int *)__cil_tmp8;
2733#line 37
2734 *mem_16 = val;
2735#line 38
2736 __cil_tmp9 = (unsigned long )cf;
2737#line 38
2738 __cil_tmp10 = __cil_tmp9 + 16;
2739#line 38
2740 __cil_tmp11 = (unsigned long )excep;
2741#line 38
2742 __cil_tmp12 = __cil_tmp11 + 24;
2743#line 38
2744 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
2745#line 38
2746 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
2747#line 38
2748 *mem_17 = *mem_18;
2749#line 39
2750 __cil_tmp13 = (unsigned long )excep;
2751#line 39
2752 __cil_tmp14 = __cil_tmp13 + 24;
2753#line 39
2754 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
2755#line 39
2756 *mem_19 = cf;
2757 }
2758#line 654 "libacc.c"
2759 return;
2760}
2761}
2762#line 44 "libacc.c"
2763void __utac__exception__cf_handler_free(void *exception )
2764{ struct __UTAC__EXCEPTION *excep ;
2765 struct __UTAC__CFLOW_FUNC *cf ;
2766 struct __UTAC__CFLOW_FUNC *tmp ;
2767 unsigned long __cil_tmp5 ;
2768 unsigned long __cil_tmp6 ;
2769 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
2770 unsigned long __cil_tmp8 ;
2771 unsigned long __cil_tmp9 ;
2772 unsigned long __cil_tmp10 ;
2773 unsigned long __cil_tmp11 ;
2774 void *__cil_tmp12 ;
2775 unsigned long __cil_tmp13 ;
2776 unsigned long __cil_tmp14 ;
2777 struct __UTAC__CFLOW_FUNC **mem_15 ;
2778 struct __UTAC__CFLOW_FUNC **mem_16 ;
2779 struct __UTAC__CFLOW_FUNC **mem_17 ;
2780
2781 {
2782#line 45
2783 excep = (struct __UTAC__EXCEPTION *)exception;
2784#line 46
2785 __cil_tmp5 = (unsigned long )excep;
2786#line 46
2787 __cil_tmp6 = __cil_tmp5 + 24;
2788#line 46
2789 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
2790#line 46
2791 cf = *mem_15;
2792 {
2793#line 49
2794 while (1) {
2795 while_1_continue: ;
2796 {
2797#line 49
2798 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
2799#line 49
2800 __cil_tmp8 = (unsigned long )__cil_tmp7;
2801#line 49
2802 __cil_tmp9 = (unsigned long )cf;
2803#line 49
2804 if (__cil_tmp9 != __cil_tmp8) {
2805
2806 } else {
2807 goto while_1_break;
2808 }
2809 }
2810 {
2811#line 50
2812 tmp = cf;
2813#line 51
2814 __cil_tmp10 = (unsigned long )cf;
2815#line 51
2816 __cil_tmp11 = __cil_tmp10 + 16;
2817#line 51
2818 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
2819#line 51
2820 cf = *mem_16;
2821#line 52
2822 __cil_tmp12 = (void *)tmp;
2823#line 52
2824 free(__cil_tmp12);
2825 }
2826 }
2827 while_1_break: ;
2828 }
2829#line 55
2830 __cil_tmp13 = (unsigned long )excep;
2831#line 55
2832 __cil_tmp14 = __cil_tmp13 + 24;
2833#line 55
2834 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
2835#line 55
2836 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
2837#line 694 "libacc.c"
2838 return;
2839}
2840}
2841#line 59 "libacc.c"
2842void __utac__exception__cf_handler_reset(void *exception )
2843{ struct __UTAC__EXCEPTION *excep ;
2844 struct __UTAC__CFLOW_FUNC *cf ;
2845 unsigned long __cil_tmp5 ;
2846 unsigned long __cil_tmp6 ;
2847 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
2848 unsigned long __cil_tmp8 ;
2849 unsigned long __cil_tmp9 ;
2850 int (*__cil_tmp10)(int , int ) ;
2851 unsigned long __cil_tmp11 ;
2852 unsigned long __cil_tmp12 ;
2853 int __cil_tmp13 ;
2854 unsigned long __cil_tmp14 ;
2855 unsigned long __cil_tmp15 ;
2856 struct __UTAC__CFLOW_FUNC **mem_16 ;
2857 int (**mem_17)(int , int ) ;
2858 int *mem_18 ;
2859 struct __UTAC__CFLOW_FUNC **mem_19 ;
2860
2861 {
2862#line 60
2863 excep = (struct __UTAC__EXCEPTION *)exception;
2864#line 61
2865 __cil_tmp5 = (unsigned long )excep;
2866#line 61
2867 __cil_tmp6 = __cil_tmp5 + 24;
2868#line 61
2869 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
2870#line 61
2871 cf = *mem_16;
2872 {
2873#line 64
2874 while (1) {
2875 while_2_continue: ;
2876 {
2877#line 64
2878 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
2879#line 64
2880 __cil_tmp8 = (unsigned long )__cil_tmp7;
2881#line 64
2882 __cil_tmp9 = (unsigned long )cf;
2883#line 64
2884 if (__cil_tmp9 != __cil_tmp8) {
2885
2886 } else {
2887 goto while_2_break;
2888 }
2889 }
2890 {
2891#line 65
2892 mem_17 = (int (**)(int , int ))cf;
2893#line 65
2894 __cil_tmp10 = *mem_17;
2895#line 65
2896 __cil_tmp11 = (unsigned long )cf;
2897#line 65
2898 __cil_tmp12 = __cil_tmp11 + 8;
2899#line 65
2900 mem_18 = (int *)__cil_tmp12;
2901#line 65
2902 __cil_tmp13 = *mem_18;
2903#line 65
2904 (*__cil_tmp10)(4, __cil_tmp13);
2905#line 66
2906 __cil_tmp14 = (unsigned long )cf;
2907#line 66
2908 __cil_tmp15 = __cil_tmp14 + 16;
2909#line 66
2910 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
2911#line 66
2912 cf = *mem_19;
2913 }
2914 }
2915 while_2_break: ;
2916 }
2917 {
2918#line 69
2919 __utac__exception__cf_handler_free(exception);
2920 }
2921#line 732 "libacc.c"
2922 return;
2923}
2924}
2925#line 80 "libacc.c"
2926void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
2927#line 80 "libacc.c"
2928static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
2929#line 79 "libacc.c"
2930void *__utac__error_stack_mgt(void *env , int mode , int count )
2931{ void *retValue_acc ;
2932 struct __ACC__ERR *new ;
2933 void *tmp ;
2934 struct __ACC__ERR *temp ;
2935 struct __ACC__ERR *next ;
2936 void *excep ;
2937 unsigned long __cil_tmp10 ;
2938 unsigned long __cil_tmp11 ;
2939 unsigned long __cil_tmp12 ;
2940 unsigned long __cil_tmp13 ;
2941 void *__cil_tmp14 ;
2942 unsigned long __cil_tmp15 ;
2943 unsigned long __cil_tmp16 ;
2944 void *__cil_tmp17 ;
2945 void **mem_18 ;
2946 struct __ACC__ERR **mem_19 ;
2947 struct __ACC__ERR **mem_20 ;
2948 void **mem_21 ;
2949 struct __ACC__ERR **mem_22 ;
2950 void **mem_23 ;
2951 void **mem_24 ;
2952
2953 {
2954#line 82 "libacc.c"
2955 if (count == 0) {
2956#line 758 "libacc.c"
2957 return (retValue_acc);
2958 } else {
2959
2960 }
2961#line 86 "libacc.c"
2962 if (mode == 0) {
2963 {
2964#line 87
2965 tmp = malloc(16UL);
2966#line 87
2967 new = (struct __ACC__ERR *)tmp;
2968#line 88
2969 mem_18 = (void **)new;
2970#line 88
2971 *mem_18 = env;
2972#line 89
2973 __cil_tmp10 = (unsigned long )new;
2974#line 89
2975 __cil_tmp11 = __cil_tmp10 + 8;
2976#line 89
2977 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
2978#line 89
2979 *mem_19 = head;
2980#line 90
2981 head = new;
2982#line 776 "libacc.c"
2983 retValue_acc = (void *)new;
2984 }
2985#line 778
2986 return (retValue_acc);
2987 } else {
2988
2989 }
2990#line 94 "libacc.c"
2991 if (mode == 1) {
2992#line 95
2993 temp = head;
2994 {
2995#line 98
2996 while (1) {
2997 while_3_continue: ;
2998#line 98
2999 if (count > 1) {
3000
3001 } else {
3002 goto while_3_break;
3003 }
3004 {
3005#line 99
3006 __cil_tmp12 = (unsigned long )temp;
3007#line 99
3008 __cil_tmp13 = __cil_tmp12 + 8;
3009#line 99
3010 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
3011#line 99
3012 next = *mem_20;
3013#line 100
3014 mem_21 = (void **)temp;
3015#line 100
3016 excep = *mem_21;
3017#line 101
3018 __cil_tmp14 = (void *)temp;
3019#line 101
3020 free(__cil_tmp14);
3021#line 102
3022 __utac__exception__cf_handler_reset(excep);
3023#line 103
3024 temp = next;
3025#line 104
3026 count = count - 1;
3027 }
3028 }
3029 while_3_break: ;
3030 }
3031 {
3032#line 107
3033 __cil_tmp15 = (unsigned long )temp;
3034#line 107
3035 __cil_tmp16 = __cil_tmp15 + 8;
3036#line 107
3037 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
3038#line 107
3039 head = *mem_22;
3040#line 108
3041 mem_23 = (void **)temp;
3042#line 108
3043 excep = *mem_23;
3044#line 109
3045 __cil_tmp17 = (void *)temp;
3046#line 109
3047 free(__cil_tmp17);
3048#line 110
3049 __utac__exception__cf_handler_reset(excep);
3050#line 820 "libacc.c"
3051 retValue_acc = excep;
3052 }
3053#line 822
3054 return (retValue_acc);
3055 } else {
3056
3057 }
3058#line 114
3059 if (mode == 2) {
3060#line 118 "libacc.c"
3061 if (head) {
3062#line 831
3063 mem_24 = (void **)head;
3064#line 831
3065 retValue_acc = *mem_24;
3066#line 833
3067 return (retValue_acc);
3068 } else {
3069#line 837 "libacc.c"
3070 retValue_acc = (void *)0;
3071#line 839
3072 return (retValue_acc);
3073 }
3074 } else {
3075
3076 }
3077#line 846 "libacc.c"
3078 return (retValue_acc);
3079}
3080}
3081#line 122 "libacc.c"
3082void *__utac__get_this_arg(int i , struct JoinPoint *this )
3083{ void *retValue_acc ;
3084 unsigned long __cil_tmp4 ;
3085 unsigned long __cil_tmp5 ;
3086 int __cil_tmp6 ;
3087 int __cil_tmp7 ;
3088 unsigned long __cil_tmp8 ;
3089 unsigned long __cil_tmp9 ;
3090 void **__cil_tmp10 ;
3091 void **__cil_tmp11 ;
3092 int *mem_12 ;
3093 void ***mem_13 ;
3094
3095 {
3096#line 123
3097 if (i > 0) {
3098 {
3099#line 123
3100 __cil_tmp4 = (unsigned long )this;
3101#line 123
3102 __cil_tmp5 = __cil_tmp4 + 16;
3103#line 123
3104 mem_12 = (int *)__cil_tmp5;
3105#line 123
3106 __cil_tmp6 = *mem_12;
3107#line 123
3108 if (i <= __cil_tmp6) {
3109
3110 } else {
3111 {
3112#line 123
3113 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3114 123U, "__utac__get_this_arg");
3115 }
3116 }
3117 }
3118 } else {
3119 {
3120#line 123
3121 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3122 123U, "__utac__get_this_arg");
3123 }
3124 }
3125#line 870 "libacc.c"
3126 __cil_tmp7 = i - 1;
3127#line 870
3128 __cil_tmp8 = (unsigned long )this;
3129#line 870
3130 __cil_tmp9 = __cil_tmp8 + 8;
3131#line 870
3132 mem_13 = (void ***)__cil_tmp9;
3133#line 870
3134 __cil_tmp10 = *mem_13;
3135#line 870
3136 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
3137#line 870
3138 retValue_acc = *__cil_tmp11;
3139#line 872
3140 return (retValue_acc);
3141#line 879
3142 return (retValue_acc);
3143}
3144}
3145#line 129 "libacc.c"
3146char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
3147{ char const *retValue_acc ;
3148 unsigned long __cil_tmp4 ;
3149 unsigned long __cil_tmp5 ;
3150 int __cil_tmp6 ;
3151 int __cil_tmp7 ;
3152 unsigned long __cil_tmp8 ;
3153 unsigned long __cil_tmp9 ;
3154 char const **__cil_tmp10 ;
3155 char const **__cil_tmp11 ;
3156 int *mem_12 ;
3157 char const ***mem_13 ;
3158
3159 {
3160#line 131
3161 if (i > 0) {
3162 {
3163#line 131
3164 __cil_tmp4 = (unsigned long )this;
3165#line 131
3166 __cil_tmp5 = __cil_tmp4 + 16;
3167#line 131
3168 mem_12 = (int *)__cil_tmp5;
3169#line 131
3170 __cil_tmp6 = *mem_12;
3171#line 131
3172 if (i <= __cil_tmp6) {
3173
3174 } else {
3175 {
3176#line 131
3177 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3178 131U, "__utac__get_this_argtype");
3179 }
3180 }
3181 }
3182 } else {
3183 {
3184#line 131
3185 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
3186 131U, "__utac__get_this_argtype");
3187 }
3188 }
3189#line 903 "libacc.c"
3190 __cil_tmp7 = i - 1;
3191#line 903
3192 __cil_tmp8 = (unsigned long )this;
3193#line 903
3194 __cil_tmp9 = __cil_tmp8 + 24;
3195#line 903
3196 mem_13 = (char const ***)__cil_tmp9;
3197#line 903
3198 __cil_tmp10 = *mem_13;
3199#line 903
3200 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
3201#line 903
3202 retValue_acc = *__cil_tmp11;
3203#line 905
3204 return (retValue_acc);
3205#line 912
3206 return (retValue_acc);
3207}
3208}
3209#line 1 "Client.o"
3210#pragma merger(0,"Client.i","")
3211#line 688 "/usr/include/stdio.h"
3212extern int puts(char const *__s ) ;
3213#line 8 "featureselect.h"
3214int __SELECTED_FEATURE_Base ;
3215#line 11 "featureselect.h"
3216int __SELECTED_FEATURE_Keys ;
3217#line 14 "featureselect.h"
3218int __SELECTED_FEATURE_Encrypt ;
3219#line 17 "featureselect.h"
3220int __SELECTED_FEATURE_AutoResponder ;
3221#line 20 "featureselect.h"
3222int __SELECTED_FEATURE_AddressBook ;
3223#line 23 "featureselect.h"
3224int __SELECTED_FEATURE_Sign ;
3225#line 26 "featureselect.h"
3226int __SELECTED_FEATURE_Forward ;
3227#line 29 "featureselect.h"
3228int __SELECTED_FEATURE_Verify ;
3229#line 32 "featureselect.h"
3230int __SELECTED_FEATURE_Decrypt ;
3231#line 35 "featureselect.h"
3232int __GUIDSL_ROOT_PRODUCTION ;
3233#line 37 "featureselect.h"
3234int __GUIDSL_NON_TERMINAL_main ;
3235#line 9 "Email.h"
3236int isReadable(int msg ) ;
3237#line 12
3238int createEmail(int from , int to ) ;
3239#line 14 "Client.h"
3240void queue(int client , int msg ) ;
3241#line 17
3242int is_queue_empty(void) ;
3243#line 19
3244int get_queued_client(void) ;
3245#line 21
3246int get_queued_email(void) ;
3247#line 24
3248void mail(int client , int msg ) ;
3249#line 26
3250void outgoing(int client , int msg ) ;
3251#line 28
3252void deliver(int client , int msg ) ;
3253#line 30
3254void incoming(int client , int msg ) ;
3255#line 32
3256int createClient(char *name ) ;
3257#line 35
3258void sendEmail(int sender , int receiver ) ;
3259#line 40
3260int isKeyPairValid(int publicKey , int privateKey ) ;
3261#line 44
3262void generateKeyPair(int client , int seed ) ;
3263#line 45
3264void autoRespond(int client , int msg ) ;
3265#line 46
3266void sendToAddressBook(int client , int msg ) ;
3267#line 48
3268void sign(int client , int msg ) ;
3269#line 50
3270void verify(int client , int msg ) ;
3271#line 6 "Client.c"
3272int queue_empty = 1;
3273#line 9 "Client.c"
3274int queued_message ;
3275#line 12 "Client.c"
3276int queued_client ;
3277#line 13
3278void __utac_acc__EncryptDecrypt_spec__1(int msg ) ;
3279#line 18 "Client.c"
3280void mail(int client , int msg )
3281{ int __utac__ad__arg1 ;
3282 int tmp ;
3283
3284 {
3285 {
3286#line 728 "Client.c"
3287 __utac__ad__arg1 = msg;
3288#line 729
3289 __utac_acc__EncryptDecrypt_spec__1(__utac__ad__arg1);
3290#line 19 "Client.c"
3291 puts("mail sent");
3292#line 20
3293 tmp = getEmailTo(msg);
3294#line 20
3295 incoming(tmp, msg);
3296 }
3297#line 746 "Client.c"
3298 return;
3299}
3300}
3301#line 27 "Client.c"
3302void outgoing__wrappee__Keys(int client , int msg )
3303{ int tmp ;
3304
3305 {
3306 {
3307#line 28
3308 tmp = getClientId(client);
3309#line 28
3310 setEmailFrom(msg, tmp);
3311#line 29
3312 mail(client, msg);
3313 }
3314#line 768 "Client.c"
3315 return;
3316}
3317}
3318#line 33 "Client.c"
3319void outgoing__wrappee__AutoResponder(int client , int msg )
3320{ int receiver ;
3321 int tmp ;
3322 int pubkey ;
3323 int tmp___0 ;
3324
3325 {
3326 {
3327#line 36
3328 tmp = getEmailTo(msg);
3329#line 36
3330 receiver = tmp;
3331#line 37
3332 tmp___0 = findPublicKey(client, receiver);
3333#line 37
3334 pubkey = tmp___0;
3335 }
3336#line 38
3337 if (pubkey) {
3338 {
3339#line 39
3340 setEmailEncryptionKey(msg, pubkey);
3341#line 40
3342 setEmailIsEncrypted(msg, 1);
3343 }
3344 } else {
3345
3346 }
3347 {
3348#line 45
3349 outgoing__wrappee__Keys(client, msg);
3350 }
3351#line 803 "Client.c"
3352 return;
3353}
3354}
3355#line 52 "Client.c"
3356void outgoing__wrappee__AddressBook(int client , int msg )
3357{ int size ;
3358 int tmp ;
3359 int receiver ;
3360 int tmp___0 ;
3361 int second ;
3362 int tmp___1 ;
3363 int tmp___2 ;
3364
3365 {
3366 {
3367#line 54
3368 tmp = getClientAddressBookSize(client);
3369#line 54
3370 size = tmp;
3371 }
3372#line 56
3373 if (size) {
3374 {
3375#line 57
3376 sendToAddressBook(client, msg);
3377#line 58
3378 puts("sending to alias in address book\n");
3379#line 59
3380 tmp___0 = getEmailTo(msg);
3381#line 59
3382 receiver = tmp___0;
3383#line 61
3384 puts("sending to second receipient\n");
3385#line 62
3386 tmp___1 = getClientAddressBookAddress(client, 1);
3387#line 62
3388 second = tmp___1;
3389#line 63
3390 setEmailTo(msg, second);
3391#line 64
3392 outgoing__wrappee__AutoResponder(client, msg);
3393#line 67
3394 tmp___2 = getClientAddressBookAddress(client, 0);
3395#line 67
3396 setEmailTo(msg, tmp___2);
3397#line 68
3398 outgoing__wrappee__AutoResponder(client, msg);
3399 }
3400 } else {
3401 {
3402#line 70
3403 outgoing__wrappee__AutoResponder(client, msg);
3404 }
3405 }
3406#line 853 "Client.c"
3407 return;
3408}
3409}
3410#line 78 "Client.c"
3411void outgoing(int client , int msg )
3412{
3413
3414 {
3415 {
3416#line 79
3417 sign(client, msg);
3418#line 80
3419 outgoing__wrappee__AddressBook(client, msg);
3420 }
3421#line 875 "Client.c"
3422 return;
3423}
3424}
3425#line 87 "Client.c"
3426void deliver(int client , int msg )
3427{
3428
3429 {
3430 {
3431#line 88
3432 puts("mail delivered\n");
3433 }
3434#line 895 "Client.c"
3435 return;
3436}
3437}
3438#line 95 "Client.c"
3439void incoming__wrappee__Encrypt(int client , int msg )
3440{
3441
3442 {
3443 {
3444#line 96
3445 deliver(client, msg);
3446 }
3447#line 915 "Client.c"
3448 return;
3449}
3450}
3451#line 102 "Client.c"
3452void incoming__wrappee__Sign(int client , int msg )
3453{ int tmp ;
3454
3455 {
3456 {
3457#line 103
3458 incoming__wrappee__Encrypt(client, msg);
3459#line 104
3460 tmp = getClientAutoResponse(client);
3461 }
3462#line 104
3463 if (tmp) {
3464 {
3465#line 105
3466 autoRespond(client, msg);
3467 }
3468 } else {
3469
3470 }
3471#line 940 "Client.c"
3472 return;
3473}
3474}
3475#line 112 "Client.c"
3476void incoming__wrappee__Verify(int client , int msg )
3477{
3478
3479 {
3480 {
3481#line 113
3482 verify(client, msg);
3483#line 114
3484 incoming__wrappee__Sign(client, msg);
3485 }
3486#line 962 "Client.c"
3487 return;
3488}
3489}
3490#line 964
3491void __utac_acc__EncryptDecrypt_spec__2(int client , int msg ) ;
3492#line 119 "Client.c"
3493void incoming(int client , int msg )
3494{ int __utac__ad__arg1 ;
3495 int __utac__ad__arg2 ;
3496 int privkey ;
3497 int tmp ;
3498 int tmp___0 ;
3499 int tmp___1 ;
3500 int tmp___2 ;
3501
3502 {
3503 {
3504#line 975 "Client.c"
3505 __utac__ad__arg1 = client;
3506#line 976
3507 __utac__ad__arg2 = msg;
3508#line 977
3509 __utac_acc__EncryptDecrypt_spec__2(__utac__ad__arg1, __utac__ad__arg2);
3510#line 122 "Client.c"
3511 tmp = getClientPrivateKey(client);
3512#line 122
3513 privkey = tmp;
3514 }
3515#line 123
3516 if (privkey) {
3517 {
3518#line 131
3519 tmp___0 = isEncrypted(msg);
3520 }
3521#line 131
3522 if (tmp___0) {
3523 {
3524#line 131
3525 tmp___1 = getEmailEncryptionKey(msg);
3526#line 131
3527 tmp___2 = isKeyPairValid(tmp___1, privkey);
3528 }
3529#line 131
3530 if (tmp___2) {
3531 {
3532#line 128
3533 setEmailIsEncrypted(msg, 0);
3534#line 129
3535 setEmailEncryptionKey(msg, 0);
3536 }
3537 } else {
3538
3539 }
3540 } else {
3541
3542 }
3543 } else {
3544
3545 }
3546 {
3547#line 134
3548 incoming__wrappee__Verify(client, msg);
3549 }
3550#line 1006 "Client.c"
3551 return;
3552}
3553}
3554#line 138 "Client.c"
3555int createClient(char *name )
3556{ int retValue_acc ;
3557 int client ;
3558 int tmp ;
3559
3560 {
3561 {
3562#line 139
3563 tmp = initClient();
3564#line 139
3565 client = tmp;
3566#line 1028 "Client.c"
3567 retValue_acc = client;
3568 }
3569#line 1030
3570 return (retValue_acc);
3571#line 1037
3572 return (retValue_acc);
3573}
3574}
3575#line 146 "Client.c"
3576void sendEmail(int sender , int receiver )
3577{ int email ;
3578 int tmp ;
3579
3580 {
3581 {
3582#line 147
3583 tmp = createEmail(0, receiver);
3584#line 147
3585 email = tmp;
3586#line 148
3587 outgoing(sender, email);
3588 }
3589#line 1065 "Client.c"
3590 return;
3591}
3592}
3593#line 156 "Client.c"
3594void queue(int client , int msg )
3595{
3596
3597 {
3598#line 157
3599 queue_empty = 0;
3600#line 158
3601 queued_message = msg;
3602#line 159
3603 queued_client = client;
3604#line 1089 "Client.c"
3605 return;
3606}
3607}
3608#line 165 "Client.c"
3609int is_queue_empty(void)
3610{ int retValue_acc ;
3611
3612 {
3613#line 1107 "Client.c"
3614 retValue_acc = queue_empty;
3615#line 1109
3616 return (retValue_acc);
3617#line 1116
3618 return (retValue_acc);
3619}
3620}
3621#line 172 "Client.c"
3622int get_queued_client(void)
3623{ int retValue_acc ;
3624
3625 {
3626#line 1138 "Client.c"
3627 retValue_acc = queued_client;
3628#line 1140
3629 return (retValue_acc);
3630#line 1147
3631 return (retValue_acc);
3632}
3633}
3634#line 179 "Client.c"
3635int get_queued_email(void)
3636{ int retValue_acc ;
3637
3638 {
3639#line 1169 "Client.c"
3640 retValue_acc = queued_message;
3641#line 1171
3642 return (retValue_acc);
3643#line 1178
3644 return (retValue_acc);
3645}
3646}
3647#line 185 "Client.c"
3648int isKeyPairValid(int publicKey , int privateKey )
3649{ int retValue_acc ;
3650 char const * __restrict __cil_tmp4 ;
3651
3652 {
3653 {
3654#line 186
3655 __cil_tmp4 = (char const * __restrict )"keypair valid %d %d";
3656#line 186
3657 printf(__cil_tmp4, publicKey, privateKey);
3658 }
3659#line 187 "Client.c"
3660 if (! publicKey) {
3661#line 1203 "Client.c"
3662 retValue_acc = 0;
3663#line 1205
3664 return (retValue_acc);
3665 } else {
3666#line 187 "Client.c"
3667 if (! privateKey) {
3668#line 1203 "Client.c"
3669 retValue_acc = 0;
3670#line 1205
3671 return (retValue_acc);
3672 } else {
3673
3674 }
3675 }
3676#line 1210 "Client.c"
3677 retValue_acc = privateKey == publicKey;
3678#line 1212
3679 return (retValue_acc);
3680#line 1219
3681 return (retValue_acc);
3682}
3683}
3684#line 195 "Client.c"
3685void generateKeyPair(int client , int seed )
3686{
3687
3688 {
3689 {
3690#line 196
3691 setClientPrivateKey(client, seed);
3692 }
3693#line 1243 "Client.c"
3694 return;
3695}
3696}
3697#line 202 "Client.c"
3698void autoRespond(int client , int msg )
3699{ int sender ;
3700 int tmp ;
3701
3702 {
3703 {
3704#line 203
3705 puts("sending autoresponse\n");
3706#line 204
3707 tmp = getEmailFrom(msg);
3708#line 204
3709 sender = tmp;
3710#line 205
3711 setEmailTo(msg, sender);
3712#line 206
3713 queue(client, msg);
3714 }
3715#line 1385 "Client.c"
3716 return;
3717}
3718}
3719#line 211 "Client.c"
3720void sendToAddressBook(int client , int msg )
3721{
3722
3723 {
3724#line 1403 "Client.c"
3725 return;
3726}
3727}
3728#line 217 "Client.c"
3729void sign(int client , int msg )
3730{ int privkey ;
3731 int tmp ;
3732
3733 {
3734 {
3735#line 218
3736 tmp = getClientPrivateKey(client);
3737#line 218
3738 privkey = tmp;
3739 }
3740#line 219
3741 if (! privkey) {
3742#line 220
3743 return;
3744 } else {
3745
3746 }
3747 {
3748#line 221
3749 setEmailIsSigned(msg, 1);
3750#line 222
3751 setEmailSignKey(msg, privkey);
3752 }
3753#line 1433 "Client.c"
3754 return;
3755}
3756}
3757#line 227 "Client.c"
3758void verify(int client , int msg )
3759{ int tmp ;
3760 int tmp___0 ;
3761 int pubkey ;
3762 int tmp___1 ;
3763 int tmp___2 ;
3764 int tmp___3 ;
3765 int tmp___4 ;
3766
3767 {
3768 {
3769#line 232
3770 tmp = isReadable(msg);
3771 }
3772#line 232
3773 if (tmp) {
3774 {
3775#line 232
3776 tmp___0 = isSigned(msg);
3777 }
3778#line 232
3779 if (tmp___0) {
3780
3781 } else {
3782#line 233
3783 return;
3784 }
3785 } else {
3786#line 233
3787 return;
3788 }
3789 {
3790#line 232
3791 tmp___1 = getEmailFrom(msg);
3792#line 232
3793 tmp___2 = findPublicKey(client, tmp___1);
3794#line 232
3795 pubkey = tmp___2;
3796 }
3797#line 233
3798 if (pubkey) {
3799 {
3800#line 233
3801 tmp___3 = getEmailSignKey(msg);
3802#line 233
3803 tmp___4 = isKeyPairValid(tmp___3, pubkey);
3804 }
3805#line 233
3806 if (tmp___4) {
3807 {
3808#line 234
3809 setEmailIsSignatureVerified(msg, 1);
3810 }
3811 } else {
3812
3813 }
3814 } else {
3815
3816 }
3817#line 1464 "Client.c"
3818 return;
3819}
3820}
3821#line 1 "featureselect.o"
3822#pragma merger(0,"featureselect.i","")
3823#line 41 "featureselect.h"
3824int select_one(void) ;
3825#line 43
3826void select_features(void) ;
3827#line 45
3828void select_helpers(void) ;
3829#line 47
3830int valid_product(void) ;
3831#line 8 "featureselect.c"
3832int select_one(void)
3833{ int retValue_acc ;
3834 int choice = __VERIFIER_nondet_int();
3835
3836 {
3837#line 84 "featureselect.c"
3838 retValue_acc = choice;
3839#line 86
3840 return (retValue_acc);
3841#line 93
3842 return (retValue_acc);
3843}
3844}
3845#line 14 "featureselect.c"
3846void select_features(void)
3847{
3848
3849 {
3850#line 115 "featureselect.c"
3851 return;
3852}
3853}
3854#line 20 "featureselect.c"
3855void select_helpers(void)
3856{
3857
3858 {
3859#line 133 "featureselect.c"
3860 return;
3861}
3862}
3863#line 25 "featureselect.c"
3864int valid_product(void)
3865{ int retValue_acc ;
3866
3867 {
3868#line 151 "featureselect.c"
3869 retValue_acc = 1;
3870#line 153
3871 return (retValue_acc);
3872#line 160
3873 return (retValue_acc);
3874}
3875}
3876#line 1 "EncryptDecrypt_spec.o"
3877#pragma merger(0,"EncryptDecrypt_spec.i","")
3878#line 7 "EncryptDecrypt_spec.c"
3879int sent_encrypted = -1;
3880#line 11 "EncryptDecrypt_spec.c"
3881void __utac_acc__EncryptDecrypt_spec__1(int msg )
3882{ char const * __restrict __cil_tmp2 ;
3883
3884 {
3885 {
3886#line 13
3887 puts("before mail\n");
3888#line 14
3889 sent_encrypted = isEncrypted(msg);
3890#line 15
3891 __cil_tmp2 = (char const * __restrict )"sent_encrypted=%d\n";
3892#line 15
3893 printf(__cil_tmp2, sent_encrypted);
3894 }
3895#line 15
3896 return;
3897}
3898}
3899#line 19 "EncryptDecrypt_spec.c"
3900void __utac_acc__EncryptDecrypt_spec__2(int client , int msg )
3901{ int tmp ;
3902 int tmp___0 ;
3903 int tmp___1 ;
3904 char const * __restrict __cil_tmp6 ;
3905
3906 {
3907 {
3908#line 21
3909 puts("before decrypt\n");
3910#line 22
3911 __cil_tmp6 = (char const * __restrict )"sent_encrypted=%d\n";
3912#line 22
3913 printf(__cil_tmp6, sent_encrypted);
3914 }
3915#line 23
3916 if (sent_encrypted == 1) {
3917 {
3918#line 28
3919 tmp = getClientPrivateKey(client);
3920#line 28
3921 tmp___0 = getEmailEncryptionKey(msg);
3922#line 28
3923 tmp___1 = isKeyPairValid(tmp___0, tmp);
3924 }
3925#line 28
3926 if (tmp___1) {
3927
3928 } else {
3929 {
3930#line 26
3931 __automaton_fail();
3932 }
3933 }
3934 } else {
3935
3936 }
3937#line 26
3938 return;
3939}
3940}
3941#line 1 "Test.o"
3942#pragma merger(0,"Test.i","")
3943#line 2 "Test.h"
3944int bob ;
3945#line 5 "Test.h"
3946int rjh ;
3947#line 8 "Test.h"
3948int chuck ;
3949#line 11
3950void setup_bob(int bob___0 ) ;
3951#line 14
3952void setup_rjh(int rjh___0 ) ;
3953#line 17
3954void setup_chuck(int chuck___0 ) ;
3955#line 26
3956void rjhToBob(void) ;
3957#line 32
3958void setup(void) ;
3959#line 35
3960int main(void) ;
3961#line 39
3962void bobKeyAddChuck(void) ;
3963#line 45
3964void rjhKeyAddChuck(void) ;
3965#line 18 "Test.c"
3966void setup_bob__wrappee__Base(int bob___0 )
3967{
3968
3969 {
3970 {
3971#line 19
3972 setClientId(bob___0, bob___0);
3973 }
3974#line 1334 "Test.c"
3975 return;
3976}
3977}
3978#line 23 "Test.c"
3979void setup_bob(int bob___0 )
3980{
3981
3982 {
3983 {
3984#line 24
3985 setup_bob__wrappee__Base(bob___0);
3986#line 25
3987 setClientPrivateKey(bob___0, 123);
3988 }
3989#line 1356 "Test.c"
3990 return;
3991}
3992}
3993#line 33 "Test.c"
3994void setup_rjh__wrappee__Base(int rjh___0 )
3995{
3996
3997 {
3998 {
3999#line 34
4000 setClientId(rjh___0, rjh___0);
4001 }
4002#line 1376 "Test.c"
4003 return;
4004}
4005}
4006#line 40 "Test.c"
4007void setup_rjh(int rjh___0 )
4008{
4009
4010 {
4011 {
4012#line 42
4013 setup_rjh__wrappee__Base(rjh___0);
4014#line 43
4015 setClientPrivateKey(rjh___0, 456);
4016 }
4017#line 1398 "Test.c"
4018 return;
4019}
4020}
4021#line 50 "Test.c"
4022void setup_chuck__wrappee__Base(int chuck___0 )
4023{
4024
4025 {
4026 {
4027#line 51
4028 setClientId(chuck___0, chuck___0);
4029 }
4030#line 1418 "Test.c"
4031 return;
4032}
4033}
4034#line 57 "Test.c"
4035void setup_chuck(int chuck___0 )
4036{
4037
4038 {
4039 {
4040#line 58
4041 setup_chuck__wrappee__Base(chuck___0);
4042#line 59
4043 setClientPrivateKey(chuck___0, 789);
4044 }
4045#line 1440 "Test.c"
4046 return;
4047}
4048}
4049#line 69 "Test.c"
4050void bobToRjh(void)
4051{ int tmp ;
4052 int tmp___0 ;
4053 int tmp___1 ;
4054
4055 {
4056 {
4057#line 71
4058 puts("Please enter a subject and a message body.\n");
4059#line 72
4060 sendEmail(bob, rjh);
4061#line 73
4062 tmp___1 = is_queue_empty();
4063 }
4064#line 73
4065 if (tmp___1) {
4066
4067 } else {
4068 {
4069#line 74
4070 tmp = get_queued_email();
4071#line 74
4072 tmp___0 = get_queued_client();
4073#line 74
4074 outgoing(tmp___0, tmp);
4075 }
4076 }
4077#line 1467 "Test.c"
4078 return;
4079}
4080}
4081#line 81 "Test.c"
4082void rjhToBob(void)
4083{
4084
4085 {
4086 {
4087#line 83
4088 puts("Please enter a subject and a message body.\n");
4089#line 84
4090 sendEmail(rjh, bob);
4091 }
4092#line 1489 "Test.c"
4093 return;
4094}
4095}
4096#line 88 "Test.c"
4097#line 95 "Test.c"
4098void setup(void)
4099{ char const * __restrict __cil_tmp1 ;
4100 char const * __restrict __cil_tmp2 ;
4101 char const * __restrict __cil_tmp3 ;
4102
4103 {
4104 {
4105#line 96
4106 bob = 1;
4107#line 97
4108 setup_bob(bob);
4109#line 98
4110 __cil_tmp1 = (char const * __restrict )"bob: %d\n";
4111#line 98
4112 printf(__cil_tmp1, bob);
4113#line 100
4114 rjh = 2;
4115#line 101
4116 setup_rjh(rjh);
4117#line 102
4118 __cil_tmp2 = (char const * __restrict )"rjh: %d\n";
4119#line 102
4120 printf(__cil_tmp2, rjh);
4121#line 104
4122 chuck = 3;
4123#line 105
4124 setup_chuck(chuck);
4125#line 106
4126 __cil_tmp3 = (char const * __restrict )"chuck: %d\n";
4127#line 106
4128 printf(__cil_tmp3, chuck);
4129 }
4130#line 1560 "Test.c"
4131 return;
4132}
4133}
4134#line 112 "Test.c"
4135int main(void)
4136{ int retValue_acc ;
4137 int tmp ;
4138
4139 {
4140 {
4141#line 113
4142 select_helpers();
4143#line 114
4144 select_features();
4145#line 115
4146 tmp = valid_product();
4147 }
4148#line 115
4149 if (tmp) {
4150 {
4151#line 116
4152 setup();
4153#line 117
4154 test();
4155 }
4156 } else {
4157
4158 }
4159#line 1591 "Test.c"
4160 return (retValue_acc);
4161}
4162}
4163#line 125 "Test.c"
4164void bobKeyAdd(void)
4165{ int tmp ;
4166 int tmp___0 ;
4167 char const * __restrict __cil_tmp3 ;
4168 char const * __restrict __cil_tmp4 ;
4169
4170 {
4171 {
4172#line 126
4173 createClientKeyringEntry(bob);
4174#line 127
4175 setClientKeyringUser(bob, 0, 2);
4176#line 128
4177 setClientKeyringPublicKey(bob, 0, 456);
4178#line 129
4179 puts("bob added rjhs key");
4180#line 130
4181 tmp = getClientKeyringUser(bob, 0);
4182#line 130
4183 __cil_tmp3 = (char const * __restrict )"%d\n";
4184#line 130
4185 printf(__cil_tmp3, tmp);
4186#line 131
4187 tmp___0 = getClientKeyringPublicKey(bob, 0);
4188#line 131
4189 __cil_tmp4 = (char const * __restrict )"%d\n";
4190#line 131
4191 printf(__cil_tmp4, tmp___0);
4192 }
4193#line 1625 "Test.c"
4194 return;
4195}
4196}
4197#line 137 "Test.c"
4198void rjhKeyAdd(void)
4199{
4200
4201 {
4202 {
4203#line 138
4204 createClientKeyringEntry(rjh);
4205#line 139
4206 setClientKeyringUser(rjh, 0, 1);
4207#line 140
4208 setClientKeyringPublicKey(rjh, 0, 123);
4209 }
4210#line 1649 "Test.c"
4211 return;
4212}
4213}
4214#line 146 "Test.c"
4215void rjhKeyAddChuck(void)
4216{
4217
4218 {
4219 {
4220#line 147
4221 createClientKeyringEntry(rjh);
4222#line 148
4223 setClientKeyringUser(rjh, 0, 3);
4224#line 149
4225 setClientKeyringPublicKey(rjh, 0, 789);
4226 }
4227#line 1673 "Test.c"
4228 return;
4229}
4230}
4231#line 156 "Test.c"
4232void bobKeyAddChuck(void)
4233{
4234
4235 {
4236 {
4237#line 157
4238 createClientKeyringEntry(bob);
4239#line 158
4240 setClientKeyringUser(bob, 1, 3);
4241#line 159
4242 setClientKeyringPublicKey(bob, 1, 789);
4243 }
4244#line 1697 "Test.c"
4245 return;
4246}
4247}
4248#line 165 "Test.c"
4249void chuckKeyAdd(void)
4250{
4251
4252 {
4253 {
4254#line 166
4255 createClientKeyringEntry(chuck);
4256#line 167
4257 setClientKeyringUser(chuck, 0, 1);
4258#line 168
4259 setClientKeyringPublicKey(chuck, 0, 123);
4260 }
4261#line 1721 "Test.c"
4262 return;
4263}
4264}
4265#line 174 "Test.c"
4266void chuckKeyAddRjh(void)
4267{
4268
4269 {
4270 {
4271#line 175
4272 createClientKeyringEntry(chuck);
4273#line 176
4274 setClientKeyringUser(chuck, 0, 2);
4275#line 177
4276 setClientKeyringPublicKey(chuck, 0, 456);
4277 }
4278#line 1745 "Test.c"
4279 return;
4280}
4281}
4282#line 183 "Test.c"
4283void rjhDeletePrivateKey(void)
4284{
4285
4286 {
4287 {
4288#line 184
4289 setClientPrivateKey(rjh, 0);
4290 }
4291#line 1765 "Test.c"
4292 return;
4293}
4294}
4295#line 190 "Test.c"
4296void bobKeyChange(void)
4297{
4298
4299 {
4300 {
4301#line 191
4302 generateKeyPair(bob, 777);
4303 }
4304#line 1785 "Test.c"
4305 return;
4306}
4307}
4308#line 197 "Test.c"
4309void rjhKeyChange(void)
4310{
4311
4312 {
4313 {
4314#line 198
4315 generateKeyPair(rjh, 666);
4316 }
4317#line 1805 "Test.c"
4318 return;
4319}
4320}
4321#line 204 "Test.c"
4322void rjhSetAutoRespond(void)
4323{
4324
4325 {
4326 {
4327#line 205
4328 setClientAutoResponse(rjh, 1);
4329 }
4330#line 1825 "Test.c"
4331 return;
4332}
4333}
4334#line 210 "Test.c"
4335void bobSetAddressBook(void)
4336{
4337
4338 {
4339 {
4340#line 211
4341 setClientAddressBookSize(bob, 1);
4342#line 212
4343 setClientAddressBookAlias(bob, 0, rjh);
4344#line 213
4345 setClientAddressBookAddress(bob, 0, rjh);
4346#line 214
4347 setClientAddressBookAddress(bob, 1, chuck);
4348 }
4349#line 1851 "Test.c"
4350 return;
4351}
4352}
4353#line 1 "Email.o"
4354#pragma merger(0,"Email.i","")
4355#line 6 "Email.h"
4356void printMail(int msg ) ;
4357#line 15
4358int cloneEmail(int msg ) ;
4359#line 9 "Email.c"
4360void printMail__wrappee__Keys(int msg )
4361{ int tmp ;
4362 int tmp___0 ;
4363 int tmp___1 ;
4364 int tmp___2 ;
4365 char const * __restrict __cil_tmp6 ;
4366 char const * __restrict __cil_tmp7 ;
4367 char const * __restrict __cil_tmp8 ;
4368 char const * __restrict __cil_tmp9 ;
4369
4370 {
4371 {
4372#line 10
4373 tmp = getEmailId(msg);
4374#line 10
4375 __cil_tmp6 = (char const * __restrict )"ID:\n %i\n";
4376#line 10
4377 printf(__cil_tmp6, tmp);
4378#line 11
4379 tmp___0 = getEmailFrom(msg);
4380#line 11
4381 __cil_tmp7 = (char const * __restrict )"FROM:\n %i\n";
4382#line 11
4383 printf(__cil_tmp7, tmp___0);
4384#line 12
4385 tmp___1 = getEmailTo(msg);
4386#line 12
4387 __cil_tmp8 = (char const * __restrict )"TO:\n %i\n";
4388#line 12
4389 printf(__cil_tmp8, tmp___1);
4390#line 13
4391 tmp___2 = isReadable(msg);
4392#line 13
4393 __cil_tmp9 = (char const * __restrict )"IS_READABLE\n %i\n";
4394#line 13
4395 printf(__cil_tmp9, tmp___2);
4396 }
4397#line 601 "Email.c"
4398 return;
4399}
4400}
4401#line 17 "Email.c"
4402void printMail__wrappee__AddressBook(int msg )
4403{ int tmp ;
4404 int tmp___0 ;
4405 char const * __restrict __cil_tmp4 ;
4406 char const * __restrict __cil_tmp5 ;
4407
4408 {
4409 {
4410#line 18
4411 printMail__wrappee__Keys(msg);
4412#line 19
4413 tmp = isEncrypted(msg);
4414#line 19
4415 __cil_tmp4 = (char const * __restrict )"ENCRYPTED\n %d\n";
4416#line 19
4417 printf(__cil_tmp4, tmp);
4418#line 20
4419 tmp___0 = getEmailEncryptionKey(msg);
4420#line 20
4421 __cil_tmp5 = (char const * __restrict )"ENCRYPTION KEY\n %d\n";
4422#line 20
4423 printf(__cil_tmp5, tmp___0);
4424 }
4425#line 625 "Email.c"
4426 return;
4427}
4428}
4429#line 26 "Email.c"
4430void printMail__wrappee__Sign(int msg )
4431{ int tmp ;
4432 int tmp___0 ;
4433 char const * __restrict __cil_tmp4 ;
4434 char const * __restrict __cil_tmp5 ;
4435
4436 {
4437 {
4438#line 27
4439 printMail__wrappee__AddressBook(msg);
4440#line 28
4441 tmp = isSigned(msg);
4442#line 28
4443 __cil_tmp4 = (char const * __restrict )"SIGNED\n %i\n";
4444#line 28
4445 printf(__cil_tmp4, tmp);
4446#line 29
4447 tmp___0 = getEmailSignKey(msg);
4448#line 29
4449 __cil_tmp5 = (char const * __restrict )"SIGNATURE\n %i\n";
4450#line 29
4451 printf(__cil_tmp5, tmp___0);
4452 }
4453#line 649 "Email.c"
4454 return;
4455}
4456}
4457#line 33 "Email.c"
4458void printMail(int msg )
4459{ int tmp ;
4460 char const * __restrict __cil_tmp3 ;
4461
4462 {
4463 {
4464#line 34
4465 printMail__wrappee__Sign(msg);
4466#line 35
4467 tmp = isVerified(msg);
4468#line 35
4469 __cil_tmp3 = (char const * __restrict )"SIGNATURE VERIFIED\n %d\n";
4470#line 35
4471 printf(__cil_tmp3, tmp);
4472 }
4473#line 671 "Email.c"
4474 return;
4475}
4476}
4477#line 41 "Email.c"
4478int isReadable__wrappee__Keys(int msg )
4479{ int retValue_acc ;
4480
4481 {
4482#line 689 "Email.c"
4483 retValue_acc = 1;
4484#line 691
4485 return (retValue_acc);
4486#line 698
4487 return (retValue_acc);
4488}
4489}
4490#line 49 "Email.c"
4491int isReadable(int msg )
4492{ int retValue_acc ;
4493 int tmp ;
4494
4495 {
4496 {
4497#line 53
4498 tmp = isEncrypted(msg);
4499 }
4500#line 53 "Email.c"
4501 if (tmp) {
4502#line 727
4503 retValue_acc = 0;
4504#line 729
4505 return (retValue_acc);
4506 } else {
4507 {
4508#line 721 "Email.c"
4509 retValue_acc = isReadable__wrappee__Keys(msg);
4510 }
4511#line 723
4512 return (retValue_acc);
4513 }
4514#line 736 "Email.c"
4515 return (retValue_acc);
4516}
4517}
4518#line 57 "Email.c"
4519int cloneEmail(int msg )
4520{ int retValue_acc ;
4521
4522 {
4523#line 758 "Email.c"
4524 retValue_acc = msg;
4525#line 760
4526 return (retValue_acc);
4527#line 767
4528 return (retValue_acc);
4529}
4530}
4531#line 62 "Email.c"
4532int createEmail(int from , int to )
4533{ int retValue_acc ;
4534 int msg ;
4535
4536 {
4537 {
4538#line 63
4539 msg = 1;
4540#line 64
4541 setEmailFrom(msg, from);
4542#line 65
4543 setEmailTo(msg, to);
4544#line 797 "Email.c"
4545 retValue_acc = msg;
4546 }
4547#line 799
4548 return (retValue_acc);
4549#line 806
4550 return (retValue_acc);
4551}
4552}