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