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