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