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