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