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