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