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