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