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