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