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