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