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