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