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