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