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