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