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