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