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