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