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