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