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