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