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