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