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