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