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