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