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 35
67void setClientPrivateKey(int handle , int value ) ;
68#line 39
69int createClientKeyringEntry(int handle ) ;
70#line 41
71int getClientKeyringUser(int handle , int index ) ;
72#line 43
73void setClientKeyringUser(int handle , int index , int value ) ;
74#line 45
75int getClientKeyringPublicKey(int handle , int index ) ;
76#line 47
77void setClientKeyringPublicKey(int handle , int index , int value ) ;
78#line 51
79void setClientForwardReceiver(int handle , 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 62
163void bobSetAddressBook(void) ;
164#line 63
165void rjhEnableForwarding(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 1334 "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 1356 "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 1376 "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 1398 "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 1418 "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 1440 "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 1467 "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 1489 "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 1560 "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 1591 "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 1625 "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 1649 "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 1673 "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 1697 "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 1721 "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 1745 "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 1765 "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 1785 "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 1805 "Test.c"
519 return;
520}
521}
522#line 203 "Test.c"
523void bobSetAddressBook(void)
524{
525
526 {
527 {
528#line 204
529 setClientAddressBookSize(bob, 1);
530#line 205
531 setClientAddressBookAlias(bob, 0, rjh);
532#line 206
533 setClientAddressBookAddress(bob, 0, rjh);
534#line 207
535 setClientAddressBookAddress(bob, 1, chuck);
536 }
537#line 1831 "Test.c"
538 return;
539}
540}
541#line 213 "Test.c"
542void rjhEnableForwarding(void)
543{
544
545 {
546 {
547#line 214
548 setClientForwardReceiver(rjh, chuck);
549 }
550#line 1851 "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 31
577void setClientAutoResponse(int handle , int value ) ;
578#line 33
579int getClientPrivateKey(int handle ) ;
580#line 37
581int getClientKeyringSize(int handle ) ;
582#line 49
583int getClientForwardReceiver(int handle ) ;
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 "Client.o"
2197#pragma merger(0,"Client.i","")
2198#line 10 "EmailLib.h"
2199int getEmailFrom(int handle ) ;
2200#line 12
2201void setEmailFrom(int handle , int value ) ;
2202#line 14
2203int getEmailTo(int handle ) ;
2204#line 16
2205void setEmailTo(int handle , int value ) ;
2206#line 26
2207int isEncrypted(int handle ) ;
2208#line 28
2209void setEmailIsEncrypted(int handle , int value ) ;
2210#line 30
2211int getEmailEncryptionKey(int handle ) ;
2212#line 32
2213void setEmailEncryptionKey(int handle , int value ) ;
2214#line 34
2215int isSigned(int handle ) ;
2216#line 36
2217void setEmailIsSigned(int handle , int value ) ;
2218#line 38
2219int getEmailSignKey(int handle ) ;
2220#line 40
2221void setEmailSignKey(int handle , int value ) ;
2222#line 44
2223void setEmailIsSignatureVerified(int handle , int value ) ;
2224#line 6 "Email.h"
2225void printMail(int msg ) ;
2226#line 9
2227int isReadable(int msg ) ;
2228#line 12
2229int createEmail(int from , int to ) ;
2230#line 14 "Client.h"
2231void queue(int client , int msg ) ;
2232#line 24
2233void mail(int client , int msg ) ;
2234#line 28
2235void deliver(int client , int msg ) ;
2236#line 30
2237void incoming(int client , int msg ) ;
2238#line 32
2239int createClient(char *name ) ;
2240#line 40
2241int isKeyPairValid(int publicKey , int privateKey ) ;
2242#line 45
2243void sendToAddressBook(int client , int msg ) ;
2244#line 47
2245void sign(int client , int msg ) ;
2246#line 49
2247void forward(int client , int msg ) ;
2248#line 51
2249void verify(int client , int msg ) ;
2250#line 6 "Client.c"
2251int queue_empty = 1;
2252#line 9 "Client.c"
2253int queued_message ;
2254#line 12 "Client.c"
2255int queued_client ;
2256#line 13
2257void __utac_acc__SignForward_spec__1(int client , int msg ) ;
2258#line 18 "Client.c"
2259void mail(int client , int msg )
2260{ int __utac__ad__arg1 ;
2261 int __utac__ad__arg2 ;
2262 int tmp ;
2263
2264 {
2265 {
2266#line 728 "Client.c"
2267 __utac__ad__arg1 = client;
2268#line 729
2269 __utac__ad__arg2 = msg;
2270#line 730
2271 __utac_acc__SignForward_spec__1(__utac__ad__arg1, __utac__ad__arg2);
2272#line 19 "Client.c"
2273 puts("mail sent");
2274#line 20
2275 tmp = getEmailTo(msg);
2276#line 20
2277 incoming(tmp, msg);
2278 }
2279#line 747 "Client.c"
2280 return;
2281}
2282}
2283#line 27 "Client.c"
2284void outgoing__wrappee__Keys(int client , int msg )
2285{ int tmp ;
2286
2287 {
2288 {
2289#line 28
2290 tmp = getClientId(client);
2291#line 28
2292 setEmailFrom(msg, tmp);
2293#line 29
2294 mail(client, msg);
2295 }
2296#line 769 "Client.c"
2297 return;
2298}
2299}
2300#line 33 "Client.c"
2301void outgoing__wrappee__Encrypt(int client , int msg )
2302{ int receiver ;
2303 int tmp ;
2304 int pubkey ;
2305 int tmp___0 ;
2306
2307 {
2308 {
2309#line 36
2310 tmp = getEmailTo(msg);
2311#line 36
2312 receiver = tmp;
2313#line 37
2314 tmp___0 = findPublicKey(client, receiver);
2315#line 37
2316 pubkey = tmp___0;
2317 }
2318#line 38
2319 if (pubkey) {
2320 {
2321#line 39
2322 setEmailEncryptionKey(msg, pubkey);
2323#line 40
2324 setEmailIsEncrypted(msg, 1);
2325 }
2326 } else {
2327
2328 }
2329 {
2330#line 45
2331 outgoing__wrappee__Keys(client, msg);
2332 }
2333#line 804 "Client.c"
2334 return;
2335}
2336}
2337#line 52 "Client.c"
2338void outgoing__wrappee__AddressBook(int client , int msg )
2339{ int size ;
2340 int tmp ;
2341 int receiver ;
2342 int tmp___0 ;
2343 int second ;
2344 int tmp___1 ;
2345 int tmp___2 ;
2346
2347 {
2348 {
2349#line 54
2350 tmp = getClientAddressBookSize(client);
2351#line 54
2352 size = tmp;
2353 }
2354#line 56
2355 if (size) {
2356 {
2357#line 57
2358 sendToAddressBook(client, msg);
2359#line 58
2360 puts("sending to alias in address book\n");
2361#line 59
2362 tmp___0 = getEmailTo(msg);
2363#line 59
2364 receiver = tmp___0;
2365#line 61
2366 puts("sending to second receipient\n");
2367#line 62
2368 tmp___1 = getClientAddressBookAddress(client, 1);
2369#line 62
2370 second = tmp___1;
2371#line 63
2372 setEmailTo(msg, second);
2373#line 64
2374 outgoing__wrappee__Encrypt(client, msg);
2375#line 67
2376 tmp___2 = getClientAddressBookAddress(client, 0);
2377#line 67
2378 setEmailTo(msg, tmp___2);
2379#line 68
2380 outgoing__wrappee__Encrypt(client, msg);
2381 }
2382 } else {
2383 {
2384#line 70
2385 outgoing__wrappee__Encrypt(client, msg);
2386 }
2387 }
2388#line 854 "Client.c"
2389 return;
2390}
2391}
2392#line 78 "Client.c"
2393void outgoing(int client , int msg )
2394{
2395
2396 {
2397 {
2398#line 79
2399 sign(client, msg);
2400#line 80
2401 outgoing__wrappee__AddressBook(client, msg);
2402 }
2403#line 876 "Client.c"
2404 return;
2405}
2406}
2407#line 87 "Client.c"
2408void deliver(int client , int msg )
2409{
2410
2411 {
2412 {
2413#line 88
2414 puts("mail delivered\n");
2415 }
2416#line 896 "Client.c"
2417 return;
2418}
2419}
2420#line 95 "Client.c"
2421void incoming__wrappee__Sign(int client , int msg )
2422{
2423
2424 {
2425 {
2426#line 96
2427 deliver(client, msg);
2428 }
2429#line 916 "Client.c"
2430 return;
2431}
2432}
2433#line 102 "Client.c"
2434void incoming__wrappee__Forward(int client , int msg )
2435{ int fwreceiver ;
2436 int tmp ;
2437
2438 {
2439 {
2440#line 103
2441 incoming__wrappee__Sign(client, msg);
2442#line 104
2443 tmp = getClientForwardReceiver(client);
2444#line 104
2445 fwreceiver = tmp;
2446 }
2447#line 105
2448 if (fwreceiver) {
2449 {
2450#line 107
2451 setEmailTo(msg, fwreceiver);
2452#line 108
2453 forward(client, msg);
2454 }
2455 } else {
2456
2457 }
2458#line 947 "Client.c"
2459 return;
2460}
2461}
2462#line 116 "Client.c"
2463void incoming__wrappee__Verify(int client , int msg )
2464{
2465
2466 {
2467 {
2468#line 117
2469 verify(client, msg);
2470#line 118
2471 incoming__wrappee__Forward(client, msg);
2472 }
2473#line 969 "Client.c"
2474 return;
2475}
2476}
2477#line 123 "Client.c"
2478void incoming(int client , int msg )
2479{ int privkey ;
2480 int tmp ;
2481 int tmp___0 ;
2482 int tmp___1 ;
2483 int tmp___2 ;
2484
2485 {
2486 {
2487#line 126
2488 tmp = getClientPrivateKey(client);
2489#line 126
2490 privkey = tmp;
2491 }
2492#line 127
2493 if (privkey) {
2494 {
2495#line 135
2496 tmp___0 = isEncrypted(msg);
2497 }
2498#line 135
2499 if (tmp___0) {
2500 {
2501#line 135
2502 tmp___1 = getEmailEncryptionKey(msg);
2503#line 135
2504 tmp___2 = isKeyPairValid(tmp___1, privkey);
2505 }
2506#line 135
2507 if (tmp___2) {
2508 {
2509#line 132
2510 setEmailIsEncrypted(msg, 0);
2511#line 133
2512 setEmailEncryptionKey(msg, 0);
2513 }
2514 } else {
2515
2516 }
2517 } else {
2518
2519 }
2520 } else {
2521
2522 }
2523 {
2524#line 138
2525 incoming__wrappee__Verify(client, msg);
2526 }
2527#line 1003 "Client.c"
2528 return;
2529}
2530}
2531#line 142 "Client.c"
2532int createClient(char *name )
2533{ int retValue_acc ;
2534 int client ;
2535 int tmp ;
2536
2537 {
2538 {
2539#line 143
2540 tmp = initClient();
2541#line 143
2542 client = tmp;
2543#line 1025 "Client.c"
2544 retValue_acc = client;
2545 }
2546#line 1027
2547 return (retValue_acc);
2548#line 1034
2549 return (retValue_acc);
2550}
2551}
2552#line 150 "Client.c"
2553void sendEmail(int sender , int receiver )
2554{ int email ;
2555 int tmp ;
2556
2557 {
2558 {
2559#line 151
2560 tmp = createEmail(0, receiver);
2561#line 151
2562 email = tmp;
2563#line 152
2564 outgoing(sender, email);
2565 }
2566#line 1062 "Client.c"
2567 return;
2568}
2569}
2570#line 160 "Client.c"
2571void queue(int client , int msg )
2572{
2573
2574 {
2575#line 161
2576 queue_empty = 0;
2577#line 162
2578 queued_message = msg;
2579#line 163
2580 queued_client = client;
2581#line 1086 "Client.c"
2582 return;
2583}
2584}
2585#line 169 "Client.c"
2586int is_queue_empty(void)
2587{ int retValue_acc ;
2588
2589 {
2590#line 1104 "Client.c"
2591 retValue_acc = queue_empty;
2592#line 1106
2593 return (retValue_acc);
2594#line 1113
2595 return (retValue_acc);
2596}
2597}
2598#line 176 "Client.c"
2599int get_queued_client(void)
2600{ int retValue_acc ;
2601
2602 {
2603#line 1135 "Client.c"
2604 retValue_acc = queued_client;
2605#line 1137
2606 return (retValue_acc);
2607#line 1144
2608 return (retValue_acc);
2609}
2610}
2611#line 183 "Client.c"
2612int get_queued_email(void)
2613{ int retValue_acc ;
2614
2615 {
2616#line 1166 "Client.c"
2617 retValue_acc = queued_message;
2618#line 1168
2619 return (retValue_acc);
2620#line 1175
2621 return (retValue_acc);
2622}
2623}
2624#line 189 "Client.c"
2625int isKeyPairValid(int publicKey , int privateKey )
2626{ int retValue_acc ;
2627 char const * __restrict __cil_tmp4 ;
2628
2629 {
2630 {
2631#line 190
2632 __cil_tmp4 = (char const * __restrict )"keypair valid %d %d";
2633#line 190
2634 printf(__cil_tmp4, publicKey, privateKey);
2635 }
2636#line 191 "Client.c"
2637 if (! publicKey) {
2638#line 1200 "Client.c"
2639 retValue_acc = 0;
2640#line 1202
2641 return (retValue_acc);
2642 } else {
2643#line 191 "Client.c"
2644 if (! privateKey) {
2645#line 1200 "Client.c"
2646 retValue_acc = 0;
2647#line 1202
2648 return (retValue_acc);
2649 } else {
2650
2651 }
2652 }
2653#line 1207 "Client.c"
2654 retValue_acc = privateKey == publicKey;
2655#line 1209
2656 return (retValue_acc);
2657#line 1216
2658 return (retValue_acc);
2659}
2660}
2661#line 199 "Client.c"
2662void generateKeyPair(int client , int seed )
2663{
2664
2665 {
2666 {
2667#line 200
2668 setClientPrivateKey(client, seed);
2669 }
2670#line 1240 "Client.c"
2671 return;
2672}
2673}
2674#line 205 "Client.c"
2675void sendToAddressBook(int client , int msg )
2676{
2677
2678 {
2679#line 1258 "Client.c"
2680 return;
2681}
2682}
2683#line 211 "Client.c"
2684void sign(int client , int msg )
2685{ int privkey ;
2686 int tmp ;
2687
2688 {
2689 {
2690#line 212
2691 tmp = getClientPrivateKey(client);
2692#line 212
2693 privkey = tmp;
2694 }
2695#line 213
2696 if (! privkey) {
2697#line 214
2698 return;
2699 } else {
2700
2701 }
2702 {
2703#line 215
2704 setEmailIsSigned(msg, 1);
2705#line 216
2706 setEmailSignKey(msg, privkey);
2707 }
2708#line 1288 "Client.c"
2709 return;
2710}
2711}
2712#line 221 "Client.c"
2713void forward(int client , int msg )
2714{
2715
2716 {
2717 {
2718#line 222
2719 puts("Forwarding message.\n");
2720#line 223
2721 printMail(msg);
2722#line 224
2723 queue(client, msg);
2724 }
2725#line 1312 "Client.c"
2726 return;
2727}
2728}
2729#line 230 "Client.c"
2730void verify(int client , int msg )
2731{ int tmp ;
2732 int tmp___0 ;
2733 int pubkey ;
2734 int tmp___1 ;
2735 int tmp___2 ;
2736 int tmp___3 ;
2737 int tmp___4 ;
2738
2739 {
2740 {
2741#line 235
2742 tmp = isReadable(msg);
2743 }
2744#line 235
2745 if (tmp) {
2746 {
2747#line 235
2748 tmp___0 = isSigned(msg);
2749 }
2750#line 235
2751 if (tmp___0) {
2752
2753 } else {
2754#line 236
2755 return;
2756 }
2757 } else {
2758#line 236
2759 return;
2760 }
2761 {
2762#line 235
2763 tmp___1 = getEmailFrom(msg);
2764#line 235
2765 tmp___2 = findPublicKey(client, tmp___1);
2766#line 235
2767 pubkey = tmp___2;
2768 }
2769#line 236
2770 if (pubkey) {
2771 {
2772#line 236
2773 tmp___3 = getEmailSignKey(msg);
2774#line 236
2775 tmp___4 = isKeyPairValid(tmp___3, pubkey);
2776 }
2777#line 236
2778 if (tmp___4) {
2779 {
2780#line 237
2781 setEmailIsSignatureVerified(msg, 1);
2782 }
2783 } else {
2784
2785 }
2786 } else {
2787
2788 }
2789#line 1343 "Client.c"
2790 return;
2791}
2792}
2793#line 1 "EmailLib.o"
2794#pragma merger(0,"EmailLib.i","")
2795#line 4 "EmailLib.h"
2796int initEmail(void) ;
2797#line 6
2798int getEmailId(int handle ) ;
2799#line 8
2800void setEmailId(int handle , int value ) ;
2801#line 18
2802char *getEmailSubject(int handle ) ;
2803#line 20
2804void setEmailSubject(int handle , char *value ) ;
2805#line 22
2806char *getEmailBody(int handle ) ;
2807#line 24
2808void setEmailBody(int handle , char *value ) ;
2809#line 42
2810int isVerified(int handle ) ;
2811#line 5 "EmailLib.c"
2812int __ste_Email_counter = 0;
2813#line 7 "EmailLib.c"
2814int initEmail(void)
2815{ int retValue_acc ;
2816
2817 {
2818#line 12 "EmailLib.c"
2819 if (__ste_Email_counter < 2) {
2820#line 670
2821 __ste_Email_counter = __ste_Email_counter + 1;
2822#line 670
2823 retValue_acc = __ste_Email_counter;
2824#line 672
2825 return (retValue_acc);
2826 } else {
2827#line 678 "EmailLib.c"
2828 retValue_acc = -1;
2829#line 680
2830 return (retValue_acc);
2831 }
2832#line 687 "EmailLib.c"
2833 return (retValue_acc);
2834}
2835}
2836#line 15 "EmailLib.c"
2837int __ste_email_id0 = 0;
2838#line 17 "EmailLib.c"
2839int __ste_email_id1 = 0;
2840#line 19 "EmailLib.c"
2841int getEmailId(int handle )
2842{ int retValue_acc ;
2843
2844 {
2845#line 26 "EmailLib.c"
2846 if (handle == 1) {
2847#line 716
2848 retValue_acc = __ste_email_id0;
2849#line 718
2850 return (retValue_acc);
2851 } else {
2852#line 720
2853 if (handle == 2) {
2854#line 725
2855 retValue_acc = __ste_email_id1;
2856#line 727
2857 return (retValue_acc);
2858 } else {
2859#line 733 "EmailLib.c"
2860 retValue_acc = 0;
2861#line 735
2862 return (retValue_acc);
2863 }
2864 }
2865#line 742 "EmailLib.c"
2866 return (retValue_acc);
2867}
2868}
2869#line 29 "EmailLib.c"
2870void setEmailId(int handle , int value )
2871{
2872
2873 {
2874#line 35
2875 if (handle == 1) {
2876#line 31
2877 __ste_email_id0 = value;
2878 } else {
2879#line 32
2880 if (handle == 2) {
2881#line 33
2882 __ste_email_id1 = value;
2883 } else {
2884
2885 }
2886 }
2887#line 773 "EmailLib.c"
2888 return;
2889}
2890}
2891#line 37 "EmailLib.c"
2892int __ste_email_from0 = 0;
2893#line 39 "EmailLib.c"
2894int __ste_email_from1 = 0;
2895#line 41 "EmailLib.c"
2896int getEmailFrom(int handle )
2897{ int retValue_acc ;
2898
2899 {
2900#line 48 "EmailLib.c"
2901 if (handle == 1) {
2902#line 798
2903 retValue_acc = __ste_email_from0;
2904#line 800
2905 return (retValue_acc);
2906 } else {
2907#line 802
2908 if (handle == 2) {
2909#line 807
2910 retValue_acc = __ste_email_from1;
2911#line 809
2912 return (retValue_acc);
2913 } else {
2914#line 815 "EmailLib.c"
2915 retValue_acc = 0;
2916#line 817
2917 return (retValue_acc);
2918 }
2919 }
2920#line 824 "EmailLib.c"
2921 return (retValue_acc);
2922}
2923}
2924#line 51 "EmailLib.c"
2925void setEmailFrom(int handle , int value )
2926{
2927
2928 {
2929#line 57
2930 if (handle == 1) {
2931#line 53
2932 __ste_email_from0 = value;
2933 } else {
2934#line 54
2935 if (handle == 2) {
2936#line 55
2937 __ste_email_from1 = value;
2938 } else {
2939
2940 }
2941 }
2942#line 855 "EmailLib.c"
2943 return;
2944}
2945}
2946#line 59 "EmailLib.c"
2947int __ste_email_to0 = 0;
2948#line 61 "EmailLib.c"
2949int __ste_email_to1 = 0;
2950#line 63 "EmailLib.c"
2951int getEmailTo(int handle )
2952{ int retValue_acc ;
2953
2954 {
2955#line 70 "EmailLib.c"
2956 if (handle == 1) {
2957#line 880
2958 retValue_acc = __ste_email_to0;
2959#line 882
2960 return (retValue_acc);
2961 } else {
2962#line 884
2963 if (handle == 2) {
2964#line 889
2965 retValue_acc = __ste_email_to1;
2966#line 891
2967 return (retValue_acc);
2968 } else {
2969#line 897 "EmailLib.c"
2970 retValue_acc = 0;
2971#line 899
2972 return (retValue_acc);
2973 }
2974 }
2975#line 906 "EmailLib.c"
2976 return (retValue_acc);
2977}
2978}
2979#line 73 "EmailLib.c"
2980void setEmailTo(int handle , int value )
2981{
2982
2983 {
2984#line 79
2985 if (handle == 1) {
2986#line 75
2987 __ste_email_to0 = value;
2988 } else {
2989#line 76
2990 if (handle == 2) {
2991#line 77
2992 __ste_email_to1 = value;
2993 } else {
2994
2995 }
2996 }
2997#line 937 "EmailLib.c"
2998 return;
2999}
3000}
3001#line 81 "EmailLib.c"
3002char *__ste_email_subject0 ;
3003#line 83 "EmailLib.c"
3004char *__ste_email_subject1 ;
3005#line 85 "EmailLib.c"
3006char *getEmailSubject(int handle )
3007{ char *retValue_acc ;
3008 void *__cil_tmp3 ;
3009
3010 {
3011#line 92 "EmailLib.c"
3012 if (handle == 1) {
3013#line 962
3014 retValue_acc = __ste_email_subject0;
3015#line 964
3016 return (retValue_acc);
3017 } else {
3018#line 966
3019 if (handle == 2) {
3020#line 971
3021 retValue_acc = __ste_email_subject1;
3022#line 973
3023 return (retValue_acc);
3024 } else {
3025#line 979 "EmailLib.c"
3026 __cil_tmp3 = (void *)0;
3027#line 979
3028 retValue_acc = (char *)__cil_tmp3;
3029#line 981
3030 return (retValue_acc);
3031 }
3032 }
3033#line 988 "EmailLib.c"
3034 return (retValue_acc);
3035}
3036}
3037#line 95 "EmailLib.c"
3038void setEmailSubject(int handle , char *value )
3039{
3040
3041 {
3042#line 101
3043 if (handle == 1) {
3044#line 97
3045 __ste_email_subject0 = value;
3046 } else {
3047#line 98
3048 if (handle == 2) {
3049#line 99
3050 __ste_email_subject1 = value;
3051 } else {
3052
3053 }
3054 }
3055#line 1019 "EmailLib.c"
3056 return;
3057}
3058}
3059#line 103 "EmailLib.c"
3060char *__ste_email_body0 = (char *)0;
3061#line 105 "EmailLib.c"
3062char *__ste_email_body1 = (char *)0;
3063#line 107 "EmailLib.c"
3064char *getEmailBody(int handle )
3065{ char *retValue_acc ;
3066 void *__cil_tmp3 ;
3067
3068 {
3069#line 114 "EmailLib.c"
3070 if (handle == 1) {
3071#line 1044
3072 retValue_acc = __ste_email_body0;
3073#line 1046
3074 return (retValue_acc);
3075 } else {
3076#line 1048
3077 if (handle == 2) {
3078#line 1053
3079 retValue_acc = __ste_email_body1;
3080#line 1055
3081 return (retValue_acc);
3082 } else {
3083#line 1061 "EmailLib.c"
3084 __cil_tmp3 = (void *)0;
3085#line 1061
3086 retValue_acc = (char *)__cil_tmp3;
3087#line 1063
3088 return (retValue_acc);
3089 }
3090 }
3091#line 1070 "EmailLib.c"
3092 return (retValue_acc);
3093}
3094}
3095#line 117 "EmailLib.c"
3096void setEmailBody(int handle , char *value )
3097{
3098
3099 {
3100#line 123
3101 if (handle == 1) {
3102#line 119
3103 __ste_email_body0 = value;
3104 } else {
3105#line 120
3106 if (handle == 2) {
3107#line 121
3108 __ste_email_body1 = value;
3109 } else {
3110
3111 }
3112 }
3113#line 1101 "EmailLib.c"
3114 return;
3115}
3116}
3117#line 125 "EmailLib.c"
3118int __ste_email_isEncrypted0 = 0;
3119#line 127 "EmailLib.c"
3120int __ste_email_isEncrypted1 = 0;
3121#line 129 "EmailLib.c"
3122int isEncrypted(int handle )
3123{ int retValue_acc ;
3124
3125 {
3126#line 136 "EmailLib.c"
3127 if (handle == 1) {
3128#line 1126
3129 retValue_acc = __ste_email_isEncrypted0;
3130#line 1128
3131 return (retValue_acc);
3132 } else {
3133#line 1130
3134 if (handle == 2) {
3135#line 1135
3136 retValue_acc = __ste_email_isEncrypted1;
3137#line 1137
3138 return (retValue_acc);
3139 } else {
3140#line 1143 "EmailLib.c"
3141 retValue_acc = 0;
3142#line 1145
3143 return (retValue_acc);
3144 }
3145 }
3146#line 1152 "EmailLib.c"
3147 return (retValue_acc);
3148}
3149}
3150#line 139 "EmailLib.c"
3151void setEmailIsEncrypted(int handle , int value )
3152{
3153
3154 {
3155#line 145
3156 if (handle == 1) {
3157#line 141
3158 __ste_email_isEncrypted0 = value;
3159 } else {
3160#line 142
3161 if (handle == 2) {
3162#line 143
3163 __ste_email_isEncrypted1 = value;
3164 } else {
3165
3166 }
3167 }
3168#line 1183 "EmailLib.c"
3169 return;
3170}
3171}
3172#line 147 "EmailLib.c"
3173int __ste_email_encryptionKey0 = 0;
3174#line 149 "EmailLib.c"
3175int __ste_email_encryptionKey1 = 0;
3176#line 151 "EmailLib.c"
3177int getEmailEncryptionKey(int handle )
3178{ int retValue_acc ;
3179
3180 {
3181#line 158 "EmailLib.c"
3182 if (handle == 1) {
3183#line 1208
3184 retValue_acc = __ste_email_encryptionKey0;
3185#line 1210
3186 return (retValue_acc);
3187 } else {
3188#line 1212
3189 if (handle == 2) {
3190#line 1217
3191 retValue_acc = __ste_email_encryptionKey1;
3192#line 1219
3193 return (retValue_acc);
3194 } else {
3195#line 1225 "EmailLib.c"
3196 retValue_acc = 0;
3197#line 1227
3198 return (retValue_acc);
3199 }
3200 }
3201#line 1234 "EmailLib.c"
3202 return (retValue_acc);
3203}
3204}
3205#line 161 "EmailLib.c"
3206void setEmailEncryptionKey(int handle , int value )
3207{
3208
3209 {
3210#line 167
3211 if (handle == 1) {
3212#line 163
3213 __ste_email_encryptionKey0 = value;
3214 } else {
3215#line 164
3216 if (handle == 2) {
3217#line 165
3218 __ste_email_encryptionKey1 = value;
3219 } else {
3220
3221 }
3222 }
3223#line 1265 "EmailLib.c"
3224 return;
3225}
3226}
3227#line 169 "EmailLib.c"
3228int __ste_email_isSigned0 = 0;
3229#line 171 "EmailLib.c"
3230int __ste_email_isSigned1 = 0;
3231#line 173 "EmailLib.c"
3232int isSigned(int handle )
3233{ int retValue_acc ;
3234
3235 {
3236#line 180 "EmailLib.c"
3237 if (handle == 1) {
3238#line 1290
3239 retValue_acc = __ste_email_isSigned0;
3240#line 1292
3241 return (retValue_acc);
3242 } else {
3243#line 1294
3244 if (handle == 2) {
3245#line 1299
3246 retValue_acc = __ste_email_isSigned1;
3247#line 1301
3248 return (retValue_acc);
3249 } else {
3250#line 1307 "EmailLib.c"
3251 retValue_acc = 0;
3252#line 1309
3253 return (retValue_acc);
3254 }
3255 }
3256#line 1316 "EmailLib.c"
3257 return (retValue_acc);
3258}
3259}
3260#line 183 "EmailLib.c"
3261void setEmailIsSigned(int handle , int value )
3262{
3263
3264 {
3265#line 189
3266 if (handle == 1) {
3267#line 185
3268 __ste_email_isSigned0 = value;
3269 } else {
3270#line 186
3271 if (handle == 2) {
3272#line 187
3273 __ste_email_isSigned1 = value;
3274 } else {
3275
3276 }
3277 }
3278#line 1347 "EmailLib.c"
3279 return;
3280}
3281}
3282#line 191 "EmailLib.c"
3283int __ste_email_signKey0 = 0;
3284#line 193 "EmailLib.c"
3285int __ste_email_signKey1 = 0;
3286#line 195 "EmailLib.c"
3287int getEmailSignKey(int handle )
3288{ int retValue_acc ;
3289
3290 {
3291#line 202 "EmailLib.c"
3292 if (handle == 1) {
3293#line 1372
3294 retValue_acc = __ste_email_signKey0;
3295#line 1374
3296 return (retValue_acc);
3297 } else {
3298#line 1376
3299 if (handle == 2) {
3300#line 1381
3301 retValue_acc = __ste_email_signKey1;
3302#line 1383
3303 return (retValue_acc);
3304 } else {
3305#line 1389 "EmailLib.c"
3306 retValue_acc = 0;
3307#line 1391
3308 return (retValue_acc);
3309 }
3310 }
3311#line 1398 "EmailLib.c"
3312 return (retValue_acc);
3313}
3314}
3315#line 205 "EmailLib.c"
3316void setEmailSignKey(int handle , int value )
3317{
3318
3319 {
3320#line 211
3321 if (handle == 1) {
3322#line 207
3323 __ste_email_signKey0 = value;
3324 } else {
3325#line 208
3326 if (handle == 2) {
3327#line 209
3328 __ste_email_signKey1 = value;
3329 } else {
3330
3331 }
3332 }
3333#line 1429 "EmailLib.c"
3334 return;
3335}
3336}
3337#line 213 "EmailLib.c"
3338int __ste_email_isSignatureVerified0 ;
3339#line 215 "EmailLib.c"
3340int __ste_email_isSignatureVerified1 ;
3341#line 217 "EmailLib.c"
3342int isVerified(int handle )
3343{ int retValue_acc ;
3344
3345 {
3346#line 224 "EmailLib.c"
3347 if (handle == 1) {
3348#line 1454
3349 retValue_acc = __ste_email_isSignatureVerified0;
3350#line 1456
3351 return (retValue_acc);
3352 } else {
3353#line 1458
3354 if (handle == 2) {
3355#line 1463
3356 retValue_acc = __ste_email_isSignatureVerified1;
3357#line 1465
3358 return (retValue_acc);
3359 } else {
3360#line 1471 "EmailLib.c"
3361 retValue_acc = 0;
3362#line 1473
3363 return (retValue_acc);
3364 }
3365 }
3366#line 1480 "EmailLib.c"
3367 return (retValue_acc);
3368}
3369}
3370#line 227 "EmailLib.c"
3371void setEmailIsSignatureVerified(int handle , int value )
3372{
3373
3374 {
3375#line 233
3376 if (handle == 1) {
3377#line 229
3378 __ste_email_isSignatureVerified0 = value;
3379 } else {
3380#line 230
3381 if (handle == 2) {
3382#line 231
3383 __ste_email_isSignatureVerified1 = value;
3384 } else {
3385
3386 }
3387 }
3388#line 1511 "EmailLib.c"
3389 return;
3390}
3391}
3392#line 1 "scenario.o"
3393#pragma merger(0,"scenario.i","")
3394#line 1 "scenario.c"
3395void test(void)
3396{ int op1 ;
3397 int op2 ;
3398 int op3 ;
3399 int op4 ;
3400 int op5 ;
3401 int op6 ;
3402 int op7 ;
3403 int op8 ;
3404 int op9 ;
3405 int op10 ;
3406 int op11 ;
3407 int splverifierCounter ;
3408 int tmp ;
3409 int tmp___0 ;
3410 int tmp___1 ;
3411 int tmp___2 ;
3412 int tmp___3 ;
3413 int tmp___4 ;
3414 int tmp___5 ;
3415 int tmp___6 ;
3416 int tmp___7 ;
3417 int tmp___8 ;
3418 int tmp___9 ;
3419
3420 {
3421#line 2
3422 op1 = 0;
3423#line 3
3424 op2 = 0;
3425#line 4
3426 op3 = 0;
3427#line 5
3428 op4 = 0;
3429#line 6
3430 op5 = 0;
3431#line 7
3432 op6 = 0;
3433#line 8
3434 op7 = 0;
3435#line 9
3436 op8 = 0;
3437#line 10
3438 op9 = 0;
3439#line 11
3440 op10 = 0;
3441#line 12
3442 op11 = 0;
3443#line 13
3444 splverifierCounter = 0;
3445 {
3446#line 14
3447 while (1) {
3448 while_0_continue: ;
3449#line 14
3450 if (splverifierCounter < 4) {
3451
3452 } else {
3453 goto while_0_break;
3454 }
3455#line 15
3456 splverifierCounter = splverifierCounter + 1;
3457#line 16
3458 if (! op1) {
3459 {
3460#line 16
3461 tmp___9 = __VERIFIER_nondet_int();
3462 }
3463#line 16
3464 if (tmp___9) {
3465 {
3466#line 17
3467 bobKeyAdd();
3468#line 18
3469 op1 = 1;
3470 }
3471 } else {
3472 goto _L___8;
3473 }
3474 } else {
3475 _L___8:
3476#line 19
3477 if (! op2) {
3478 {
3479#line 19
3480 tmp___8 = __VERIFIER_nondet_int();
3481 }
3482#line 19
3483 if (tmp___8) {
3484#line 21
3485 op2 = 1;
3486 } else {
3487 goto _L___7;
3488 }
3489 } else {
3490 _L___7:
3491#line 22
3492 if (! op3) {
3493 {
3494#line 22
3495 tmp___7 = __VERIFIER_nondet_int();
3496 }
3497#line 22
3498 if (tmp___7) {
3499 {
3500#line 24
3501 rjhDeletePrivateKey();
3502#line 25
3503 op3 = 1;
3504 }
3505 } else {
3506 goto _L___6;
3507 }
3508 } else {
3509 _L___6:
3510#line 26
3511 if (! op4) {
3512 {
3513#line 26
3514 tmp___6 = __VERIFIER_nondet_int();
3515 }
3516#line 26
3517 if (tmp___6) {
3518 {
3519#line 28
3520 rjhKeyAdd();
3521#line 29
3522 op4 = 1;
3523 }
3524 } else {
3525 goto _L___5;
3526 }
3527 } else {
3528 _L___5:
3529#line 30
3530 if (! op5) {
3531 {
3532#line 30
3533 tmp___5 = __VERIFIER_nondet_int();
3534 }
3535#line 30
3536 if (tmp___5) {
3537 {
3538#line 32
3539 chuckKeyAddRjh();
3540#line 33
3541 op5 = 1;
3542 }
3543 } else {
3544 goto _L___4;
3545 }
3546 } else {
3547 _L___4:
3548#line 34
3549 if (! op6) {
3550 {
3551#line 34
3552 tmp___4 = __VERIFIER_nondet_int();
3553 }
3554#line 34
3555 if (tmp___4) {
3556 {
3557#line 36
3558 rjhEnableForwarding();
3559#line 37
3560 op6 = 1;
3561 }
3562 } else {
3563 goto _L___3;
3564 }
3565 } else {
3566 _L___3:
3567#line 38
3568 if (! op7) {
3569 {
3570#line 38
3571 tmp___3 = __VERIFIER_nondet_int();
3572 }
3573#line 38
3574 if (tmp___3) {
3575 {
3576#line 40
3577 rjhKeyChange();
3578#line 41
3579 op7 = 1;
3580 }
3581 } else {
3582 goto _L___2;
3583 }
3584 } else {
3585 _L___2:
3586#line 42
3587 if (! op8) {
3588 {
3589#line 42
3590 tmp___2 = __VERIFIER_nondet_int();
3591 }
3592#line 42
3593 if (tmp___2) {
3594 {
3595#line 44
3596 bobSetAddressBook();
3597#line 45
3598 op8 = 1;
3599 }
3600 } else {
3601 goto _L___1;
3602 }
3603 } else {
3604 _L___1:
3605#line 46
3606 if (! op9) {
3607 {
3608#line 46
3609 tmp___1 = __VERIFIER_nondet_int();
3610 }
3611#line 46
3612 if (tmp___1) {
3613 {
3614#line 48
3615 chuckKeyAdd();
3616#line 49
3617 op9 = 1;
3618 }
3619 } else {
3620 goto _L___0;
3621 }
3622 } else {
3623 _L___0:
3624#line 50
3625 if (! op10) {
3626 {
3627#line 50
3628 tmp___0 = __VERIFIER_nondet_int();
3629 }
3630#line 50
3631 if (tmp___0) {
3632 {
3633#line 52
3634 bobKeyChange();
3635#line 53
3636 op10 = 1;
3637 }
3638 } else {
3639 goto _L;
3640 }
3641 } else {
3642 _L:
3643#line 54
3644 if (! op11) {
3645 {
3646#line 54
3647 tmp = __VERIFIER_nondet_int();
3648 }
3649#line 54
3650 if (tmp) {
3651 {
3652#line 56
3653 chuckKeyAdd();
3654#line 57
3655 op11 = 1;
3656 }
3657 } else {
3658 goto while_0_break;
3659 }
3660 } else {
3661 goto while_0_break;
3662 }
3663 }
3664 }
3665 }
3666 }
3667 }
3668 }
3669 }
3670 }
3671 }
3672 }
3673 }
3674 while_0_break: ;
3675 }
3676 {
3677#line 61
3678 bobToRjh();
3679 }
3680#line 169 "scenario.c"
3681 return;
3682}
3683}
3684#line 1 "featureselect.o"
3685#pragma merger(0,"featureselect.i","")
3686#line 41 "featureselect.h"
3687int select_one(void) ;
3688#line 8 "featureselect.c"
3689int select_one(void)
3690{ int retValue_acc ;
3691 int choice = __VERIFIER_nondet_int();
3692
3693 {
3694#line 84 "featureselect.c"
3695 retValue_acc = choice;
3696#line 86
3697 return (retValue_acc);
3698#line 93
3699 return (retValue_acc);
3700}
3701}
3702#line 14 "featureselect.c"
3703void select_features(void)
3704{
3705
3706 {
3707#line 115 "featureselect.c"
3708 return;
3709}
3710}
3711#line 20 "featureselect.c"
3712void select_helpers(void)
3713{
3714
3715 {
3716#line 133 "featureselect.c"
3717 return;
3718}
3719}
3720#line 25 "featureselect.c"
3721int valid_product(void)
3722{ int retValue_acc ;
3723
3724 {
3725#line 151 "featureselect.c"
3726 retValue_acc = 1;
3727#line 153
3728 return (retValue_acc);
3729#line 160
3730 return (retValue_acc);
3731}
3732}
3733#line 1 "SignForward_spec.o"
3734#pragma merger(0,"SignForward_spec.i","")
3735#line 13 "SignForward_spec.c"
3736void __utac_acc__SignForward_spec__1(int client , int msg )
3737{ int tmp ;
3738 int tmp___0 ;
3739
3740 {
3741 {
3742#line 15
3743 puts("before mail\n");
3744#line 16
3745 tmp___0 = isSigned(msg);
3746 }
3747#line 16
3748 if (tmp___0) {
3749 {
3750#line 20
3751 tmp = getClientPrivateKey(client);
3752 }
3753#line 20
3754 if (tmp == 0) {
3755 {
3756#line 18
3757 __automaton_fail();
3758 }
3759 } else {
3760
3761 }
3762 } else {
3763
3764 }
3765#line 18
3766 return;
3767}
3768}
3769#line 1 "Util.o"
3770#pragma merger(0,"Util.i","")
3771#line 1 "Util.h"
3772int prompt(char *msg ) ;
3773#line 9 "Util.c"
3774int prompt(char *msg )
3775{ int retValue_acc ;
3776 int retval ;
3777 char const * __restrict __cil_tmp4 ;
3778
3779 {
3780 {
3781#line 10
3782 __cil_tmp4 = (char const * __restrict )"%s\n";
3783#line 10
3784 printf(__cil_tmp4, msg);
3785#line 518 "Util.c"
3786 retValue_acc = retval;
3787 }
3788#line 520
3789 return (retValue_acc);
3790#line 527
3791 return (retValue_acc);
3792}
3793}
3794#line 1 "Email.o"
3795#pragma merger(0,"Email.i","")
3796#line 15 "Email.h"
3797int cloneEmail(int msg ) ;
3798#line 9 "Email.c"
3799void printMail__wrappee__Keys(int msg )
3800{ int tmp ;
3801 int tmp___0 ;
3802 int tmp___1 ;
3803 int tmp___2 ;
3804 char const * __restrict __cil_tmp6 ;
3805 char const * __restrict __cil_tmp7 ;
3806 char const * __restrict __cil_tmp8 ;
3807 char const * __restrict __cil_tmp9 ;
3808
3809 {
3810 {
3811#line 10
3812 tmp = getEmailId(msg);
3813#line 10
3814 __cil_tmp6 = (char const * __restrict )"ID:\n %i\n";
3815#line 10
3816 printf(__cil_tmp6, tmp);
3817#line 11
3818 tmp___0 = getEmailFrom(msg);
3819#line 11
3820 __cil_tmp7 = (char const * __restrict )"FROM:\n %i\n";
3821#line 11
3822 printf(__cil_tmp7, tmp___0);
3823#line 12
3824 tmp___1 = getEmailTo(msg);
3825#line 12
3826 __cil_tmp8 = (char const * __restrict )"TO:\n %i\n";
3827#line 12
3828 printf(__cil_tmp8, tmp___1);
3829#line 13
3830 tmp___2 = isReadable(msg);
3831#line 13
3832 __cil_tmp9 = (char const * __restrict )"IS_READABLE\n %i\n";
3833#line 13
3834 printf(__cil_tmp9, tmp___2);
3835 }
3836#line 601 "Email.c"
3837 return;
3838}
3839}
3840#line 17 "Email.c"
3841void printMail__wrappee__AddressBook(int msg )
3842{ int tmp ;
3843 int tmp___0 ;
3844 char const * __restrict __cil_tmp4 ;
3845 char const * __restrict __cil_tmp5 ;
3846
3847 {
3848 {
3849#line 18
3850 printMail__wrappee__Keys(msg);
3851#line 19
3852 tmp = isEncrypted(msg);
3853#line 19
3854 __cil_tmp4 = (char const * __restrict )"ENCRYPTED\n %d\n";
3855#line 19
3856 printf(__cil_tmp4, tmp);
3857#line 20
3858 tmp___0 = getEmailEncryptionKey(msg);
3859#line 20
3860 __cil_tmp5 = (char const * __restrict )"ENCRYPTION KEY\n %d\n";
3861#line 20
3862 printf(__cil_tmp5, tmp___0);
3863 }
3864#line 625 "Email.c"
3865 return;
3866}
3867}
3868#line 26 "Email.c"
3869void printMail__wrappee__Forward(int msg )
3870{ int tmp ;
3871 int tmp___0 ;
3872 char const * __restrict __cil_tmp4 ;
3873 char const * __restrict __cil_tmp5 ;
3874
3875 {
3876 {
3877#line 27
3878 printMail__wrappee__AddressBook(msg);
3879#line 28
3880 tmp = isSigned(msg);
3881#line 28
3882 __cil_tmp4 = (char const * __restrict )"SIGNED\n %i\n";
3883#line 28
3884 printf(__cil_tmp4, tmp);
3885#line 29
3886 tmp___0 = getEmailSignKey(msg);
3887#line 29
3888 __cil_tmp5 = (char const * __restrict )"SIGNATURE\n %i\n";
3889#line 29
3890 printf(__cil_tmp5, tmp___0);
3891 }
3892#line 649 "Email.c"
3893 return;
3894}
3895}
3896#line 33 "Email.c"
3897void printMail(int msg )
3898{ int tmp ;
3899 char const * __restrict __cil_tmp3 ;
3900
3901 {
3902 {
3903#line 34
3904 printMail__wrappee__Forward(msg);
3905#line 35
3906 tmp = isVerified(msg);
3907#line 35
3908 __cil_tmp3 = (char const * __restrict )"SIGNATURE VERIFIED\n %d\n";
3909#line 35
3910 printf(__cil_tmp3, tmp);
3911 }
3912#line 671 "Email.c"
3913 return;
3914}
3915}
3916#line 41 "Email.c"
3917int isReadable__wrappee__Keys(int msg )
3918{ int retValue_acc ;
3919
3920 {
3921#line 689 "Email.c"
3922 retValue_acc = 1;
3923#line 691
3924 return (retValue_acc);
3925#line 698
3926 return (retValue_acc);
3927}
3928}
3929#line 49 "Email.c"
3930int isReadable(int msg )
3931{ int retValue_acc ;
3932 int tmp ;
3933
3934 {
3935 {
3936#line 53
3937 tmp = isEncrypted(msg);
3938 }
3939#line 53 "Email.c"
3940 if (tmp) {
3941#line 727
3942 retValue_acc = 0;
3943#line 729
3944 return (retValue_acc);
3945 } else {
3946 {
3947#line 721 "Email.c"
3948 retValue_acc = isReadable__wrappee__Keys(msg);
3949 }
3950#line 723
3951 return (retValue_acc);
3952 }
3953#line 736 "Email.c"
3954 return (retValue_acc);
3955}
3956}
3957#line 57 "Email.c"
3958int cloneEmail(int msg )
3959{ int retValue_acc ;
3960
3961 {
3962#line 758 "Email.c"
3963 retValue_acc = msg;
3964#line 760
3965 return (retValue_acc);
3966#line 767
3967 return (retValue_acc);
3968}
3969}
3970#line 62 "Email.c"
3971int createEmail(int from , int to )
3972{ int retValue_acc ;
3973 int msg ;
3974
3975 {
3976 {
3977#line 63
3978 msg = 1;
3979#line 64
3980 setEmailFrom(msg, from);
3981#line 65
3982 setEmailTo(msg, to);
3983#line 797 "Email.c"
3984 retValue_acc = msg;
3985 }
3986#line 799
3987 return (retValue_acc);
3988#line 806
3989 return (retValue_acc);
3990}
3991}
3992#line 1 "libacc.o"
3993#pragma merger(0,"libacc.i","")
3994#line 73 "/usr/include/assert.h"
3995extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
3996 char const *__file ,
3997 unsigned int __line ,
3998 char const *__function ) ;
3999#line 471 "/usr/include/stdlib.h"
4000extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
4001#line 488
4002extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
4003#line 32 "libacc.c"
4004void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
4005 int ) ,
4006 int val )
4007{ struct __UTAC__EXCEPTION *excep ;
4008 struct __UTAC__CFLOW_FUNC *cf ;
4009 void *tmp ;
4010 unsigned long __cil_tmp7 ;
4011 unsigned long __cil_tmp8 ;
4012 unsigned long __cil_tmp9 ;
4013 unsigned long __cil_tmp10 ;
4014 unsigned long __cil_tmp11 ;
4015 unsigned long __cil_tmp12 ;
4016 unsigned long __cil_tmp13 ;
4017 unsigned long __cil_tmp14 ;
4018 int (**mem_15)(int , int ) ;
4019 int *mem_16 ;
4020 struct __UTAC__CFLOW_FUNC **mem_17 ;
4021 struct __UTAC__CFLOW_FUNC **mem_18 ;
4022 struct __UTAC__CFLOW_FUNC **mem_19 ;
4023
4024 {
4025 {
4026#line 33
4027 excep = (struct __UTAC__EXCEPTION *)exception;
4028#line 34
4029 tmp = malloc(24UL);
4030#line 34
4031 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
4032#line 36
4033 mem_15 = (int (**)(int , int ))cf;
4034#line 36
4035 *mem_15 = cflow_func;
4036#line 37
4037 __cil_tmp7 = (unsigned long )cf;
4038#line 37
4039 __cil_tmp8 = __cil_tmp7 + 8;
4040#line 37
4041 mem_16 = (int *)__cil_tmp8;
4042#line 37
4043 *mem_16 = val;
4044#line 38
4045 __cil_tmp9 = (unsigned long )cf;
4046#line 38
4047 __cil_tmp10 = __cil_tmp9 + 16;
4048#line 38
4049 __cil_tmp11 = (unsigned long )excep;
4050#line 38
4051 __cil_tmp12 = __cil_tmp11 + 24;
4052#line 38
4053 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
4054#line 38
4055 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
4056#line 38
4057 *mem_17 = *mem_18;
4058#line 39
4059 __cil_tmp13 = (unsigned long )excep;
4060#line 39
4061 __cil_tmp14 = __cil_tmp13 + 24;
4062#line 39
4063 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
4064#line 39
4065 *mem_19 = cf;
4066 }
4067#line 654 "libacc.c"
4068 return;
4069}
4070}
4071#line 44 "libacc.c"
4072void __utac__exception__cf_handler_free(void *exception )
4073{ struct __UTAC__EXCEPTION *excep ;
4074 struct __UTAC__CFLOW_FUNC *cf ;
4075 struct __UTAC__CFLOW_FUNC *tmp ;
4076 unsigned long __cil_tmp5 ;
4077 unsigned long __cil_tmp6 ;
4078 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
4079 unsigned long __cil_tmp8 ;
4080 unsigned long __cil_tmp9 ;
4081 unsigned long __cil_tmp10 ;
4082 unsigned long __cil_tmp11 ;
4083 void *__cil_tmp12 ;
4084 unsigned long __cil_tmp13 ;
4085 unsigned long __cil_tmp14 ;
4086 struct __UTAC__CFLOW_FUNC **mem_15 ;
4087 struct __UTAC__CFLOW_FUNC **mem_16 ;
4088 struct __UTAC__CFLOW_FUNC **mem_17 ;
4089
4090 {
4091#line 45
4092 excep = (struct __UTAC__EXCEPTION *)exception;
4093#line 46
4094 __cil_tmp5 = (unsigned long )excep;
4095#line 46
4096 __cil_tmp6 = __cil_tmp5 + 24;
4097#line 46
4098 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
4099#line 46
4100 cf = *mem_15;
4101 {
4102#line 49
4103 while (1) {
4104 while_1_continue: ;
4105 {
4106#line 49
4107 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
4108#line 49
4109 __cil_tmp8 = (unsigned long )__cil_tmp7;
4110#line 49
4111 __cil_tmp9 = (unsigned long )cf;
4112#line 49
4113 if (__cil_tmp9 != __cil_tmp8) {
4114
4115 } else {
4116 goto while_1_break;
4117 }
4118 }
4119 {
4120#line 50
4121 tmp = cf;
4122#line 51
4123 __cil_tmp10 = (unsigned long )cf;
4124#line 51
4125 __cil_tmp11 = __cil_tmp10 + 16;
4126#line 51
4127 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
4128#line 51
4129 cf = *mem_16;
4130#line 52
4131 __cil_tmp12 = (void *)tmp;
4132#line 52
4133 free(__cil_tmp12);
4134 }
4135 }
4136 while_1_break: ;
4137 }
4138#line 55
4139 __cil_tmp13 = (unsigned long )excep;
4140#line 55
4141 __cil_tmp14 = __cil_tmp13 + 24;
4142#line 55
4143 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
4144#line 55
4145 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
4146#line 694 "libacc.c"
4147 return;
4148}
4149}
4150#line 59 "libacc.c"
4151void __utac__exception__cf_handler_reset(void *exception )
4152{ struct __UTAC__EXCEPTION *excep ;
4153 struct __UTAC__CFLOW_FUNC *cf ;
4154 unsigned long __cil_tmp5 ;
4155 unsigned long __cil_tmp6 ;
4156 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
4157 unsigned long __cil_tmp8 ;
4158 unsigned long __cil_tmp9 ;
4159 int (*__cil_tmp10)(int , int ) ;
4160 unsigned long __cil_tmp11 ;
4161 unsigned long __cil_tmp12 ;
4162 int __cil_tmp13 ;
4163 unsigned long __cil_tmp14 ;
4164 unsigned long __cil_tmp15 ;
4165 struct __UTAC__CFLOW_FUNC **mem_16 ;
4166 int (**mem_17)(int , int ) ;
4167 int *mem_18 ;
4168 struct __UTAC__CFLOW_FUNC **mem_19 ;
4169
4170 {
4171#line 60
4172 excep = (struct __UTAC__EXCEPTION *)exception;
4173#line 61
4174 __cil_tmp5 = (unsigned long )excep;
4175#line 61
4176 __cil_tmp6 = __cil_tmp5 + 24;
4177#line 61
4178 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
4179#line 61
4180 cf = *mem_16;
4181 {
4182#line 64
4183 while (1) {
4184 while_2_continue: ;
4185 {
4186#line 64
4187 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
4188#line 64
4189 __cil_tmp8 = (unsigned long )__cil_tmp7;
4190#line 64
4191 __cil_tmp9 = (unsigned long )cf;
4192#line 64
4193 if (__cil_tmp9 != __cil_tmp8) {
4194
4195 } else {
4196 goto while_2_break;
4197 }
4198 }
4199 {
4200#line 65
4201 mem_17 = (int (**)(int , int ))cf;
4202#line 65
4203 __cil_tmp10 = *mem_17;
4204#line 65
4205 __cil_tmp11 = (unsigned long )cf;
4206#line 65
4207 __cil_tmp12 = __cil_tmp11 + 8;
4208#line 65
4209 mem_18 = (int *)__cil_tmp12;
4210#line 65
4211 __cil_tmp13 = *mem_18;
4212#line 65
4213 (*__cil_tmp10)(4, __cil_tmp13);
4214#line 66
4215 __cil_tmp14 = (unsigned long )cf;
4216#line 66
4217 __cil_tmp15 = __cil_tmp14 + 16;
4218#line 66
4219 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
4220#line 66
4221 cf = *mem_19;
4222 }
4223 }
4224 while_2_break: ;
4225 }
4226 {
4227#line 69
4228 __utac__exception__cf_handler_free(exception);
4229 }
4230#line 732 "libacc.c"
4231 return;
4232}
4233}
4234#line 80 "libacc.c"
4235void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
4236#line 80 "libacc.c"
4237static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
4238#line 79 "libacc.c"
4239void *__utac__error_stack_mgt(void *env , int mode , int count )
4240{ void *retValue_acc ;
4241 struct __ACC__ERR *new ;
4242 void *tmp ;
4243 struct __ACC__ERR *temp ;
4244 struct __ACC__ERR *next ;
4245 void *excep ;
4246 unsigned long __cil_tmp10 ;
4247 unsigned long __cil_tmp11 ;
4248 unsigned long __cil_tmp12 ;
4249 unsigned long __cil_tmp13 ;
4250 void *__cil_tmp14 ;
4251 unsigned long __cil_tmp15 ;
4252 unsigned long __cil_tmp16 ;
4253 void *__cil_tmp17 ;
4254 void **mem_18 ;
4255 struct __ACC__ERR **mem_19 ;
4256 struct __ACC__ERR **mem_20 ;
4257 void **mem_21 ;
4258 struct __ACC__ERR **mem_22 ;
4259 void **mem_23 ;
4260 void **mem_24 ;
4261
4262 {
4263#line 82 "libacc.c"
4264 if (count == 0) {
4265#line 758 "libacc.c"
4266 return (retValue_acc);
4267 } else {
4268
4269 }
4270#line 86 "libacc.c"
4271 if (mode == 0) {
4272 {
4273#line 87
4274 tmp = malloc(16UL);
4275#line 87
4276 new = (struct __ACC__ERR *)tmp;
4277#line 88
4278 mem_18 = (void **)new;
4279#line 88
4280 *mem_18 = env;
4281#line 89
4282 __cil_tmp10 = (unsigned long )new;
4283#line 89
4284 __cil_tmp11 = __cil_tmp10 + 8;
4285#line 89
4286 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
4287#line 89
4288 *mem_19 = head;
4289#line 90
4290 head = new;
4291#line 776 "libacc.c"
4292 retValue_acc = (void *)new;
4293 }
4294#line 778
4295 return (retValue_acc);
4296 } else {
4297
4298 }
4299#line 94 "libacc.c"
4300 if (mode == 1) {
4301#line 95
4302 temp = head;
4303 {
4304#line 98
4305 while (1) {
4306 while_3_continue: ;
4307#line 98
4308 if (count > 1) {
4309
4310 } else {
4311 goto while_3_break;
4312 }
4313 {
4314#line 99
4315 __cil_tmp12 = (unsigned long )temp;
4316#line 99
4317 __cil_tmp13 = __cil_tmp12 + 8;
4318#line 99
4319 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
4320#line 99
4321 next = *mem_20;
4322#line 100
4323 mem_21 = (void **)temp;
4324#line 100
4325 excep = *mem_21;
4326#line 101
4327 __cil_tmp14 = (void *)temp;
4328#line 101
4329 free(__cil_tmp14);
4330#line 102
4331 __utac__exception__cf_handler_reset(excep);
4332#line 103
4333 temp = next;
4334#line 104
4335 count = count - 1;
4336 }
4337 }
4338 while_3_break: ;
4339 }
4340 {
4341#line 107
4342 __cil_tmp15 = (unsigned long )temp;
4343#line 107
4344 __cil_tmp16 = __cil_tmp15 + 8;
4345#line 107
4346 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
4347#line 107
4348 head = *mem_22;
4349#line 108
4350 mem_23 = (void **)temp;
4351#line 108
4352 excep = *mem_23;
4353#line 109
4354 __cil_tmp17 = (void *)temp;
4355#line 109
4356 free(__cil_tmp17);
4357#line 110
4358 __utac__exception__cf_handler_reset(excep);
4359#line 820 "libacc.c"
4360 retValue_acc = excep;
4361 }
4362#line 822
4363 return (retValue_acc);
4364 } else {
4365
4366 }
4367#line 114
4368 if (mode == 2) {
4369#line 118 "libacc.c"
4370 if (head) {
4371#line 831
4372 mem_24 = (void **)head;
4373#line 831
4374 retValue_acc = *mem_24;
4375#line 833
4376 return (retValue_acc);
4377 } else {
4378#line 837 "libacc.c"
4379 retValue_acc = (void *)0;
4380#line 839
4381 return (retValue_acc);
4382 }
4383 } else {
4384
4385 }
4386#line 846 "libacc.c"
4387 return (retValue_acc);
4388}
4389}
4390#line 122 "libacc.c"
4391void *__utac__get_this_arg(int i , struct JoinPoint *this )
4392{ void *retValue_acc ;
4393 unsigned long __cil_tmp4 ;
4394 unsigned long __cil_tmp5 ;
4395 int __cil_tmp6 ;
4396 int __cil_tmp7 ;
4397 unsigned long __cil_tmp8 ;
4398 unsigned long __cil_tmp9 ;
4399 void **__cil_tmp10 ;
4400 void **__cil_tmp11 ;
4401 int *mem_12 ;
4402 void ***mem_13 ;
4403
4404 {
4405#line 123
4406 if (i > 0) {
4407 {
4408#line 123
4409 __cil_tmp4 = (unsigned long )this;
4410#line 123
4411 __cil_tmp5 = __cil_tmp4 + 16;
4412#line 123
4413 mem_12 = (int *)__cil_tmp5;
4414#line 123
4415 __cil_tmp6 = *mem_12;
4416#line 123
4417 if (i <= __cil_tmp6) {
4418
4419 } else {
4420 {
4421#line 123
4422 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4423 123U, "__utac__get_this_arg");
4424 }
4425 }
4426 }
4427 } else {
4428 {
4429#line 123
4430 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4431 123U, "__utac__get_this_arg");
4432 }
4433 }
4434#line 870 "libacc.c"
4435 __cil_tmp7 = i - 1;
4436#line 870
4437 __cil_tmp8 = (unsigned long )this;
4438#line 870
4439 __cil_tmp9 = __cil_tmp8 + 8;
4440#line 870
4441 mem_13 = (void ***)__cil_tmp9;
4442#line 870
4443 __cil_tmp10 = *mem_13;
4444#line 870
4445 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4446#line 870
4447 retValue_acc = *__cil_tmp11;
4448#line 872
4449 return (retValue_acc);
4450#line 879
4451 return (retValue_acc);
4452}
4453}
4454#line 129 "libacc.c"
4455char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
4456{ char const *retValue_acc ;
4457 unsigned long __cil_tmp4 ;
4458 unsigned long __cil_tmp5 ;
4459 int __cil_tmp6 ;
4460 int __cil_tmp7 ;
4461 unsigned long __cil_tmp8 ;
4462 unsigned long __cil_tmp9 ;
4463 char const **__cil_tmp10 ;
4464 char const **__cil_tmp11 ;
4465 int *mem_12 ;
4466 char const ***mem_13 ;
4467
4468 {
4469#line 131
4470 if (i > 0) {
4471 {
4472#line 131
4473 __cil_tmp4 = (unsigned long )this;
4474#line 131
4475 __cil_tmp5 = __cil_tmp4 + 16;
4476#line 131
4477 mem_12 = (int *)__cil_tmp5;
4478#line 131
4479 __cil_tmp6 = *mem_12;
4480#line 131
4481 if (i <= __cil_tmp6) {
4482
4483 } else {
4484 {
4485#line 131
4486 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4487 131U, "__utac__get_this_argtype");
4488 }
4489 }
4490 }
4491 } else {
4492 {
4493#line 131
4494 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4495 131U, "__utac__get_this_argtype");
4496 }
4497 }
4498#line 903 "libacc.c"
4499 __cil_tmp7 = i - 1;
4500#line 903
4501 __cil_tmp8 = (unsigned long )this;
4502#line 903
4503 __cil_tmp9 = __cil_tmp8 + 24;
4504#line 903
4505 mem_13 = (char const ***)__cil_tmp9;
4506#line 903
4507 __cil_tmp10 = *mem_13;
4508#line 903
4509 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4510#line 903
4511 retValue_acc = *__cil_tmp11;
4512#line 905
4513 return (retValue_acc);
4514#line 912
4515 return (retValue_acc);
4516}
4517}