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