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