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