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