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