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