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