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