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