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