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