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