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