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