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