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