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