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