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