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