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