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