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