1extern int __VERIFIER_nondet_int(void);
2extern int printf (__const char *__restrict __format, ...);
3
4
5
6#line 2 "libacc.c"
7struct JoinPoint {
8 void **(*fp)(struct JoinPoint * ) ;
9 void **args ;
10 int argsCount ;
11 char const **argsType ;
12 void *(*arg)(int , struct JoinPoint * ) ;
13 char const *(*argType)(int , struct JoinPoint * ) ;
14 void **retValue ;
15 char const *retType ;
16 char const *funcName ;
17 char const *targetName ;
18 char const *fileName ;
19 char const *kind ;
20 void *excep_return ;
21};
22#line 18 "libacc.c"
23struct __UTAC__CFLOW_FUNC {
24 int (*func)(int , int ) ;
25 int val ;
26 struct __UTAC__CFLOW_FUNC *next ;
27};
28#line 18 "libacc.c"
29struct __UTAC__EXCEPTION {
30 void *jumpbuf ;
31 unsigned long long prtValue ;
32 int pops ;
33 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
34};
35#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
36typedef unsigned long size_t;
37#line 76 "libacc.c"
38struct __ACC__ERR {
39 void *v ;
40 struct __ACC__ERR *next ;
41};
42#line 1 "Environment.o"
43#pragma merger(0,"Environment.i","")
44#line 4 "Environment.h"
45void lowerWaterLevel(void) ;
46#line 6
47void waterRise(void) ;
48#line 8
49void changeMethaneLevel(void) ;
50#line 10
51int isMethaneLevelCritical(void) ;
52#line 12
53int getWaterLevel(void) ;
54#line 15
55void printEnvironment(void) ;
56#line 16
57int isHighWaterSensorDry(void) ;
58#line 9 "Environment.c"
59int waterLevel = 1;
60#line 12 "Environment.c"
61int methaneLevelCritical = 0;
62#line 15 "Environment.c"
63void lowerWaterLevel(void)
64{
65
66 {
67#line 19
68 if (waterLevel > 0) {
69#line 17
70 waterLevel = waterLevel - 1;
71 } else {
72
73 }
74#line 83 "Environment.c"
75 return;
76}
77}
78#line 22 "Environment.c"
79void waterRise(void)
80{
81
82 {
83#line 26
84 if (waterLevel < 2) {
85#line 24
86 waterLevel = waterLevel + 1;
87 } else {
88
89 }
90#line 106 "Environment.c"
91 return;
92}
93}
94#line 29 "Environment.c"
95void changeMethaneLevel(void)
96{
97
98 {
99#line 34
100 if (methaneLevelCritical) {
101#line 31
102 methaneLevelCritical = 0;
103 } else {
104#line 33
105 methaneLevelCritical = 1;
106 }
107#line 132 "Environment.c"
108 return;
109}
110}
111#line 38 "Environment.c"
112int isMethaneLevelCritical(void)
113{ int retValue_acc ;
114
115 {
116#line 150 "Environment.c"
117 retValue_acc = methaneLevelCritical;
118#line 152
119 return (retValue_acc);
120#line 159
121 return (retValue_acc);
122}
123}
124#line 45 "Environment.c"
125#line 44 "Environment.c"
126void printEnvironment(void)
127{
128
129 {
130 {
131#line 45
132 printf("Env(Water:%i", waterLevel);
133#line 46
134 printf(",Meth:");
135 }
136#line 47
137 if (methaneLevelCritical) {
138 {
139#line 48
140 printf("CRIT");
141 }
142 } else {
143 {
144#line 49
145 printf("OK");
146 }
147 }
148 {
149#line 51
150 printf(")");
151 }
152#line 191 "Environment.c"
153 return;
154}
155}
156#line 55 "Environment.c"
157int getWaterLevel(void)
158{ int retValue_acc ;
159
160 {
161#line 209 "Environment.c"
162 retValue_acc = waterLevel;
163#line 211
164 return (retValue_acc);
165#line 218
166 return (retValue_acc);
167}
168}
169#line 58 "Environment.c"
170int isHighWaterSensorDry(void)
171{ int retValue_acc ;
172
173 {
174#line 65 "Environment.c"
175 if (waterLevel < 2) {
176#line 243
177 retValue_acc = 1;
178#line 245
179 return (retValue_acc);
180 } else {
181#line 251 "Environment.c"
182 retValue_acc = 0;
183#line 253
184 return (retValue_acc);
185 }
186#line 260 "Environment.c"
187 return (retValue_acc);
188}
189}
190#line 1 "Test.o"
191#pragma merger(0,"Test.i","")
192#line 8 "Test.c"
193int cleanupTimeShifts = 4;
194#line 11 "Test.c"
195#line 20 "Test.c"
196void timeShift(void) ;
197#line 17 "Test.c"
198void cleanup(void)
199{ int i ;
200 int __cil_tmp2 ;
201
202 {
203 {
204#line 20
205 timeShift();
206#line 22
207 i = 0;
208 }
209 {
210#line 22
211 while (1) {
212 while_0_continue: ;
213 {
214#line 22
215 __cil_tmp2 = cleanupTimeShifts - 1;
216#line 22
217 if (i < __cil_tmp2) {
218
219 } else {
220 goto while_0_break;
221 }
222 }
223 {
224#line 23
225 timeShift();
226#line 22
227 i = i + 1;
228 }
229 }
230 while_0_break: ;
231 }
232#line 1111 "Test.c"
233 return;
234}
235}
236#line 57 "Test.c"
237void printPump(void) ;
238#line 56 "Test.c"
239void Specification2(void)
240{
241
242 {
243 {
244#line 57
245 timeShift();
246#line 57
247 printPump();
248#line 58
249 timeShift();
250#line 58
251 printPump();
252#line 59
253 timeShift();
254#line 59
255 printPump();
256#line 60
257 waterRise();
258#line 60
259 printPump();
260#line 61
261 timeShift();
262#line 61
263 printPump();
264#line 62
265 changeMethaneLevel();
266#line 62
267 printPump();
268#line 63
269 timeShift();
270#line 63
271 printPump();
272#line 64
273 cleanup();
274 }
275#line 1159 "Test.c"
276 return;
277}
278}
279#line 67 "Test.c"
280void setup(void)
281{
282
283 {
284#line 1177 "Test.c"
285 return;
286}
287}
288#line 77 "Test.c"
289void test(void) ;
290#line 74 "Test.c"
291void runTest(void)
292{
293
294 {
295 {
296#line 77
297 test();
298 }
299#line 1197 "Test.c"
300 return;
301}
302}
303#line 83 "Test.c"
304void select_helpers(void) ;
305#line 84
306void select_features(void) ;
307#line 85
308int valid_product(void) ;
309#line 82 "Test.c"
310int main(void)
311{ int retValue_acc ;
312 int tmp ;
313
314 {
315 {
316#line 83
317 select_helpers();
318#line 84
319 select_features();
320#line 85
321 tmp = valid_product();
322 }
323#line 85
324 if (tmp) {
325 {
326#line 86
327 setup();
328#line 87
329 runTest();
330 }
331 } else {
332
333 }
334#line 1226 "Test.c"
335 retValue_acc = 0;
336#line 1228
337 return (retValue_acc);
338#line 1235
339 return (retValue_acc);
340}
341}
342#line 1 "libacc.o"
343#pragma merger(0,"libacc.i","")
344#line 73 "/usr/include/assert.h"
345extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
346 char const *__file ,
347 unsigned int __line ,
348 char const *__function ) ;
349#line 471 "/usr/include/stdlib.h"
350extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
351#line 488
352extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
353#line 32 "libacc.c"
354void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
355 int ) ,
356 int val )
357{ struct __UTAC__EXCEPTION *excep ;
358 struct __UTAC__CFLOW_FUNC *cf ;
359 void *tmp ;
360 unsigned long __cil_tmp7 ;
361 unsigned long __cil_tmp8 ;
362 unsigned long __cil_tmp9 ;
363 unsigned long __cil_tmp10 ;
364 unsigned long __cil_tmp11 ;
365 unsigned long __cil_tmp12 ;
366 unsigned long __cil_tmp13 ;
367 unsigned long __cil_tmp14 ;
368 int (**mem_15)(int , int ) ;
369 int *mem_16 ;
370 struct __UTAC__CFLOW_FUNC **mem_17 ;
371 struct __UTAC__CFLOW_FUNC **mem_18 ;
372 struct __UTAC__CFLOW_FUNC **mem_19 ;
373
374 {
375 {
376#line 33
377 excep = (struct __UTAC__EXCEPTION *)exception;
378#line 34
379 tmp = malloc(24UL);
380#line 34
381 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
382#line 36
383 mem_15 = (int (**)(int , int ))cf;
384#line 36
385 *mem_15 = cflow_func;
386#line 37
387 __cil_tmp7 = (unsigned long )cf;
388#line 37
389 __cil_tmp8 = __cil_tmp7 + 8;
390#line 37
391 mem_16 = (int *)__cil_tmp8;
392#line 37
393 *mem_16 = val;
394#line 38
395 __cil_tmp9 = (unsigned long )cf;
396#line 38
397 __cil_tmp10 = __cil_tmp9 + 16;
398#line 38
399 __cil_tmp11 = (unsigned long )excep;
400#line 38
401 __cil_tmp12 = __cil_tmp11 + 24;
402#line 38
403 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
404#line 38
405 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
406#line 38
407 *mem_17 = *mem_18;
408#line 39
409 __cil_tmp13 = (unsigned long )excep;
410#line 39
411 __cil_tmp14 = __cil_tmp13 + 24;
412#line 39
413 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
414#line 39
415 *mem_19 = cf;
416 }
417#line 654 "libacc.c"
418 return;
419}
420}
421#line 44 "libacc.c"
422void __utac__exception__cf_handler_free(void *exception )
423{ struct __UTAC__EXCEPTION *excep ;
424 struct __UTAC__CFLOW_FUNC *cf ;
425 struct __UTAC__CFLOW_FUNC *tmp ;
426 unsigned long __cil_tmp5 ;
427 unsigned long __cil_tmp6 ;
428 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
429 unsigned long __cil_tmp8 ;
430 unsigned long __cil_tmp9 ;
431 unsigned long __cil_tmp10 ;
432 unsigned long __cil_tmp11 ;
433 void *__cil_tmp12 ;
434 unsigned long __cil_tmp13 ;
435 unsigned long __cil_tmp14 ;
436 struct __UTAC__CFLOW_FUNC **mem_15 ;
437 struct __UTAC__CFLOW_FUNC **mem_16 ;
438 struct __UTAC__CFLOW_FUNC **mem_17 ;
439
440 {
441#line 45
442 excep = (struct __UTAC__EXCEPTION *)exception;
443#line 46
444 __cil_tmp5 = (unsigned long )excep;
445#line 46
446 __cil_tmp6 = __cil_tmp5 + 24;
447#line 46
448 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
449#line 46
450 cf = *mem_15;
451 {
452#line 49
453 while (1) {
454 while_1_continue: ;
455 {
456#line 49
457 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
458#line 49
459 __cil_tmp8 = (unsigned long )__cil_tmp7;
460#line 49
461 __cil_tmp9 = (unsigned long )cf;
462#line 49
463 if (__cil_tmp9 != __cil_tmp8) {
464
465 } else {
466 goto while_1_break;
467 }
468 }
469 {
470#line 50
471 tmp = cf;
472#line 51
473 __cil_tmp10 = (unsigned long )cf;
474#line 51
475 __cil_tmp11 = __cil_tmp10 + 16;
476#line 51
477 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
478#line 51
479 cf = *mem_16;
480#line 52
481 __cil_tmp12 = (void *)tmp;
482#line 52
483 free(__cil_tmp12);
484 }
485 }
486 while_1_break: ;
487 }
488#line 55
489 __cil_tmp13 = (unsigned long )excep;
490#line 55
491 __cil_tmp14 = __cil_tmp13 + 24;
492#line 55
493 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
494#line 55
495 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
496#line 694 "libacc.c"
497 return;
498}
499}
500#line 59 "libacc.c"
501void __utac__exception__cf_handler_reset(void *exception )
502{ struct __UTAC__EXCEPTION *excep ;
503 struct __UTAC__CFLOW_FUNC *cf ;
504 unsigned long __cil_tmp5 ;
505 unsigned long __cil_tmp6 ;
506 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
507 unsigned long __cil_tmp8 ;
508 unsigned long __cil_tmp9 ;
509 int (*__cil_tmp10)(int , int ) ;
510 unsigned long __cil_tmp11 ;
511 unsigned long __cil_tmp12 ;
512 int __cil_tmp13 ;
513 unsigned long __cil_tmp14 ;
514 unsigned long __cil_tmp15 ;
515 struct __UTAC__CFLOW_FUNC **mem_16 ;
516 int (**mem_17)(int , int ) ;
517 int *mem_18 ;
518 struct __UTAC__CFLOW_FUNC **mem_19 ;
519
520 {
521#line 60
522 excep = (struct __UTAC__EXCEPTION *)exception;
523#line 61
524 __cil_tmp5 = (unsigned long )excep;
525#line 61
526 __cil_tmp6 = __cil_tmp5 + 24;
527#line 61
528 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
529#line 61
530 cf = *mem_16;
531 {
532#line 64
533 while (1) {
534 while_2_continue: ;
535 {
536#line 64
537 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
538#line 64
539 __cil_tmp8 = (unsigned long )__cil_tmp7;
540#line 64
541 __cil_tmp9 = (unsigned long )cf;
542#line 64
543 if (__cil_tmp9 != __cil_tmp8) {
544
545 } else {
546 goto while_2_break;
547 }
548 }
549 {
550#line 65
551 mem_17 = (int (**)(int , int ))cf;
552#line 65
553 __cil_tmp10 = *mem_17;
554#line 65
555 __cil_tmp11 = (unsigned long )cf;
556#line 65
557 __cil_tmp12 = __cil_tmp11 + 8;
558#line 65
559 mem_18 = (int *)__cil_tmp12;
560#line 65
561 __cil_tmp13 = *mem_18;
562#line 65
563 (*__cil_tmp10)(4, __cil_tmp13);
564#line 66
565 __cil_tmp14 = (unsigned long )cf;
566#line 66
567 __cil_tmp15 = __cil_tmp14 + 16;
568#line 66
569 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
570#line 66
571 cf = *mem_19;
572 }
573 }
574 while_2_break: ;
575 }
576 {
577#line 69
578 __utac__exception__cf_handler_free(exception);
579 }
580#line 732 "libacc.c"
581 return;
582}
583}
584#line 80 "libacc.c"
585void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
586#line 80 "libacc.c"
587static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
588#line 79 "libacc.c"
589void *__utac__error_stack_mgt(void *env , int mode , int count )
590{ void *retValue_acc ;
591 struct __ACC__ERR *new ;
592 void *tmp ;
593 struct __ACC__ERR *temp ;
594 struct __ACC__ERR *next ;
595 void *excep ;
596 unsigned long __cil_tmp10 ;
597 unsigned long __cil_tmp11 ;
598 unsigned long __cil_tmp12 ;
599 unsigned long __cil_tmp13 ;
600 void *__cil_tmp14 ;
601 unsigned long __cil_tmp15 ;
602 unsigned long __cil_tmp16 ;
603 void *__cil_tmp17 ;
604 void **mem_18 ;
605 struct __ACC__ERR **mem_19 ;
606 struct __ACC__ERR **mem_20 ;
607 void **mem_21 ;
608 struct __ACC__ERR **mem_22 ;
609 void **mem_23 ;
610 void **mem_24 ;
611
612 {
613#line 82 "libacc.c"
614 if (count == 0) {
615#line 758 "libacc.c"
616 return (retValue_acc);
617 } else {
618
619 }
620#line 86 "libacc.c"
621 if (mode == 0) {
622 {
623#line 87
624 tmp = malloc(16UL);
625#line 87
626 new = (struct __ACC__ERR *)tmp;
627#line 88
628 mem_18 = (void **)new;
629#line 88
630 *mem_18 = env;
631#line 89
632 __cil_tmp10 = (unsigned long )new;
633#line 89
634 __cil_tmp11 = __cil_tmp10 + 8;
635#line 89
636 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
637#line 89
638 *mem_19 = head;
639#line 90
640 head = new;
641#line 776 "libacc.c"
642 retValue_acc = (void *)new;
643 }
644#line 778
645 return (retValue_acc);
646 } else {
647
648 }
649#line 94 "libacc.c"
650 if (mode == 1) {
651#line 95
652 temp = head;
653 {
654#line 98
655 while (1) {
656 while_3_continue: ;
657#line 98
658 if (count > 1) {
659
660 } else {
661 goto while_3_break;
662 }
663 {
664#line 99
665 __cil_tmp12 = (unsigned long )temp;
666#line 99
667 __cil_tmp13 = __cil_tmp12 + 8;
668#line 99
669 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
670#line 99
671 next = *mem_20;
672#line 100
673 mem_21 = (void **)temp;
674#line 100
675 excep = *mem_21;
676#line 101
677 __cil_tmp14 = (void *)temp;
678#line 101
679 free(__cil_tmp14);
680#line 102
681 __utac__exception__cf_handler_reset(excep);
682#line 103
683 temp = next;
684#line 104
685 count = count - 1;
686 }
687 }
688 while_3_break: ;
689 }
690 {
691#line 107
692 __cil_tmp15 = (unsigned long )temp;
693#line 107
694 __cil_tmp16 = __cil_tmp15 + 8;
695#line 107
696 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
697#line 107
698 head = *mem_22;
699#line 108
700 mem_23 = (void **)temp;
701#line 108
702 excep = *mem_23;
703#line 109
704 __cil_tmp17 = (void *)temp;
705#line 109
706 free(__cil_tmp17);
707#line 110
708 __utac__exception__cf_handler_reset(excep);
709#line 820 "libacc.c"
710 retValue_acc = excep;
711 }
712#line 822
713 return (retValue_acc);
714 } else {
715
716 }
717#line 114
718 if (mode == 2) {
719#line 118 "libacc.c"
720 if (head) {
721#line 831
722 mem_24 = (void **)head;
723#line 831
724 retValue_acc = *mem_24;
725#line 833
726 return (retValue_acc);
727 } else {
728#line 837 "libacc.c"
729 retValue_acc = (void *)0;
730#line 839
731 return (retValue_acc);
732 }
733 } else {
734
735 }
736#line 846 "libacc.c"
737 return (retValue_acc);
738}
739}
740#line 122 "libacc.c"
741void *__utac__get_this_arg(int i , struct JoinPoint *this )
742{ void *retValue_acc ;
743 unsigned long __cil_tmp4 ;
744 unsigned long __cil_tmp5 ;
745 int __cil_tmp6 ;
746 int __cil_tmp7 ;
747 unsigned long __cil_tmp8 ;
748 unsigned long __cil_tmp9 ;
749 void **__cil_tmp10 ;
750 void **__cil_tmp11 ;
751 int *mem_12 ;
752 void ***mem_13 ;
753
754 {
755#line 123
756 if (i > 0) {
757 {
758#line 123
759 __cil_tmp4 = (unsigned long )this;
760#line 123
761 __cil_tmp5 = __cil_tmp4 + 16;
762#line 123
763 mem_12 = (int *)__cil_tmp5;
764#line 123
765 __cil_tmp6 = *mem_12;
766#line 123
767 if (i <= __cil_tmp6) {
768
769 } else {
770 {
771#line 123
772 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
773 123U, "__utac__get_this_arg");
774 }
775 }
776 }
777 } else {
778 {
779#line 123
780 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
781 123U, "__utac__get_this_arg");
782 }
783 }
784#line 870 "libacc.c"
785 __cil_tmp7 = i - 1;
786#line 870
787 __cil_tmp8 = (unsigned long )this;
788#line 870
789 __cil_tmp9 = __cil_tmp8 + 8;
790#line 870
791 mem_13 = (void ***)__cil_tmp9;
792#line 870
793 __cil_tmp10 = *mem_13;
794#line 870
795 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
796#line 870
797 retValue_acc = *__cil_tmp11;
798#line 872
799 return (retValue_acc);
800#line 879
801 return (retValue_acc);
802}
803}
804#line 129 "libacc.c"
805char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
806{ char const *retValue_acc ;
807 unsigned long __cil_tmp4 ;
808 unsigned long __cil_tmp5 ;
809 int __cil_tmp6 ;
810 int __cil_tmp7 ;
811 unsigned long __cil_tmp8 ;
812 unsigned long __cil_tmp9 ;
813 char const **__cil_tmp10 ;
814 char const **__cil_tmp11 ;
815 int *mem_12 ;
816 char const ***mem_13 ;
817
818 {
819#line 131
820 if (i > 0) {
821 {
822#line 131
823 __cil_tmp4 = (unsigned long )this;
824#line 131
825 __cil_tmp5 = __cil_tmp4 + 16;
826#line 131
827 mem_12 = (int *)__cil_tmp5;
828#line 131
829 __cil_tmp6 = *mem_12;
830#line 131
831 if (i <= __cil_tmp6) {
832
833 } else {
834 {
835#line 131
836 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
837 131U, "__utac__get_this_argtype");
838 }
839 }
840 }
841 } else {
842 {
843#line 131
844 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
845 131U, "__utac__get_this_argtype");
846 }
847 }
848#line 903 "libacc.c"
849 __cil_tmp7 = i - 1;
850#line 903
851 __cil_tmp8 = (unsigned long )this;
852#line 903
853 __cil_tmp9 = __cil_tmp8 + 24;
854#line 903
855 mem_13 = (char const ***)__cil_tmp9;
856#line 903
857 __cil_tmp10 = *mem_13;
858#line 903
859 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
860#line 903
861 retValue_acc = *__cil_tmp11;
862#line 905
863 return (retValue_acc);
864#line 912
865 return (retValue_acc);
866}
867}
868#line 1 "wsllib_check.o"
869#pragma merger(0,"wsllib_check.i","")
870#line 3 "wsllib_check.c"
871void __automaton_fail(void)
872{
873
874 {
875 goto ERROR;
876 ERROR: ;
877#line 53 "wsllib_check.c"
878 return;
879}
880}
881#line 1 "scenario.o"
882#pragma merger(0,"scenario.i","")
883#line 1 "scenario.c"
884void test(void)
885{ int splverifierCounter ;
886 int tmp ;
887 int tmp___0 ;
888 int tmp___1 ;
889 int tmp___2 ;
890
891 {
892#line 2
893 splverifierCounter = 0;
894 {
895#line 3
896 while (1) {
897 while_4_continue: ;
898#line 3
899 if (splverifierCounter < 4) {
900
901 } else {
902 goto while_4_break;
903 }
904 {
905#line 7
906 tmp = __VERIFIER_nondet_int();
907 }
908#line 7
909 if (tmp) {
910 {
911#line 5
912 waterRise();
913 }
914 } else {
915
916 }
917 {
918#line 7
919 tmp___0 = __VERIFIER_nondet_int();
920 }
921#line 7
922 if (tmp___0) {
923 {
924#line 8
925 changeMethaneLevel();
926 }
927 } else {
928
929 }
930 {
931#line 10
932 tmp___2 = __VERIFIER_nondet_int();
933 }
934#line 10
935 if (tmp___2) {
936
937 } else {
938 {
939#line 12
940 tmp___1 = __VERIFIER_nondet_int();
941 }
942#line 12
943 if (tmp___1) {
944
945 } else {
946
947 }
948 }
949 {
950#line 13
951 timeShift();
952 }
953 }
954 while_4_break: ;
955 }
956 {
957#line 15
958 cleanup();
959 }
960#line 74 "scenario.c"
961 return;
962}
963}
964#line 1 "MinePump.o"
965#pragma merger(0,"MinePump.i","")
966#line 6 "MinePump.h"
967void activatePump(void) ;
968#line 8
969void deactivatePump(void) ;
970#line 10
971int isPumpRunning(void) ;
972#line 7 "MinePump.c"
973int pumpRunning = 0;
974#line 9 "MinePump.c"
975int systemActive = 1;
976#line 10
977void __utac_acc__Specification3_spec__1(void) ;
978#line 16
979void processEnvironment(void) ;
980#line 12 "MinePump.c"
981void timeShift(void)
982{
983
984 {
985#line 15
986 if (pumpRunning) {
987 {
988#line 16
989 lowerWaterLevel();
990 }
991 } else {
992
993 }
994#line 15
995 if (systemActive) {
996 {
997#line 16
998 processEnvironment();
999 }
1000 } else {
1001
1002 }
1003 {
1004#line 97 "MinePump.c"
1005 __utac_acc__Specification3_spec__1();
1006 }
1007#line 103
1008 return;
1009}
1010}
1011#line 19 "MinePump.c"
1012void processEnvironment__wrappee__base(void)
1013{
1014
1015 {
1016#line 121 "MinePump.c"
1017 return;
1018}
1019}
1020#line 28 "MinePump.c"
1021int isHighWaterLevel(void) ;
1022#line 23 "MinePump.c"
1023void processEnvironment(void)
1024{ int tmp ;
1025
1026 {
1027#line 28
1028 if (! pumpRunning) {
1029 {
1030#line 28
1031 tmp = isHighWaterLevel();
1032 }
1033#line 28
1034 if (tmp) {
1035 {
1036#line 25
1037 activatePump();
1038 }
1039 } else {
1040 {
1041#line 27
1042 processEnvironment__wrappee__base();
1043 }
1044 }
1045 } else {
1046 {
1047#line 27
1048 processEnvironment__wrappee__base();
1049 }
1050 }
1051#line 147 "MinePump.c"
1052 return;
1053}
1054}
1055#line 32 "MinePump.c"
1056void activatePump(void)
1057{
1058
1059 {
1060#line 33
1061 pumpRunning = 1;
1062#line 167 "MinePump.c"
1063 return;
1064}
1065}
1066#line 37 "MinePump.c"
1067void deactivatePump(void)
1068{
1069
1070 {
1071#line 38
1072 pumpRunning = 0;
1073#line 187 "MinePump.c"
1074 return;
1075}
1076}
1077#line 42 "MinePump.c"
1078int isMethaneAlarm(void)
1079{ int retValue_acc ;
1080
1081 {
1082 {
1083#line 205 "MinePump.c"
1084 retValue_acc = isMethaneLevelCritical();
1085 }
1086#line 207
1087 return (retValue_acc);
1088#line 214
1089 return (retValue_acc);
1090}
1091}
1092#line 47 "MinePump.c"
1093int isPumpRunning(void)
1094{ int retValue_acc ;
1095
1096 {
1097#line 236 "MinePump.c"
1098 retValue_acc = pumpRunning;
1099#line 238
1100 return (retValue_acc);
1101#line 245
1102 return (retValue_acc);
1103}
1104}
1105#line 52 "MinePump.c"
1106void printPump(void)
1107{
1108
1109 {
1110 {
1111#line 53
1112 printf("Pump(System:");
1113 }
1114#line 54
1115 if (systemActive) {
1116 {
1117#line 55
1118 printf("On");
1119 }
1120 } else {
1121 {
1122#line 56
1123 printf("Off");
1124 }
1125 }
1126 {
1127#line 58
1128 printf(",Pump:");
1129 }
1130#line 59
1131 if (pumpRunning) {
1132 {
1133#line 60
1134 printf("On");
1135 }
1136 } else {
1137 {
1138#line 61
1139 printf("Off");
1140 }
1141 }
1142 {
1143#line 63
1144 printf(") ");
1145#line 64
1146 printEnvironment();
1147#line 65
1148 printf("\n");
1149 }
1150#line 285 "MinePump.c"
1151 return;
1152}
1153}
1154#line 67 "MinePump.c"
1155int isHighWaterLevel(void)
1156{ int retValue_acc ;
1157 int tmp ;
1158 int tmp___0 ;
1159
1160 {
1161 {
1162#line 303 "MinePump.c"
1163 tmp = isHighWaterSensorDry();
1164 }
1165#line 303
1166 if (tmp) {
1167#line 303
1168 tmp___0 = 0;
1169 } else {
1170#line 303
1171 tmp___0 = 1;
1172 }
1173#line 303
1174 retValue_acc = tmp___0;
1175#line 305
1176 return (retValue_acc);
1177#line 312
1178 return (retValue_acc);
1179}
1180}
1181#line 1 "Specification3_spec.o"
1182#pragma merger(0,"Specification3_spec.i","")
1183#line 11 "Specification3_spec.c"
1184void __utac_acc__Specification3_spec__1(void)
1185{ int tmp ;
1186 int tmp___0 ;
1187 int tmp___1 ;
1188
1189 {
1190 {
1191#line 19
1192 tmp = isMethaneLevelCritical();
1193 }
1194#line 19
1195 if (tmp) {
1196
1197 } else {
1198 {
1199#line 19
1200 tmp___0 = getWaterLevel();
1201 }
1202#line 19
1203 if (tmp___0 == 2) {
1204 {
1205#line 19
1206 tmp___1 = isPumpRunning();
1207 }
1208#line 19
1209 if (tmp___1) {
1210
1211 } else {
1212 {
1213#line 16
1214 __automaton_fail();
1215 }
1216 }
1217 } else {
1218
1219 }
1220 }
1221#line 16
1222 return;
1223}
1224}
1225#line 1 "featureselect.o"
1226#pragma merger(0,"featureselect.i","")
1227#line 8 "featureselect.h"
1228int select_one(void) ;
1229#line 8 "featureselect.c"
1230int select_one(void)
1231{ int retValue_acc ;
1232 int choice = __VERIFIER_nondet_int();
1233
1234 {
1235#line 62 "featureselect.c"
1236 retValue_acc = choice;
1237#line 64
1238 return (retValue_acc);
1239#line 71
1240 return (retValue_acc);
1241}
1242}
1243#line 14 "featureselect.c"
1244void select_features(void)
1245{
1246
1247 {
1248#line 93 "featureselect.c"
1249 return;
1250}
1251}
1252#line 20 "featureselect.c"
1253void select_helpers(void)
1254{
1255
1256 {
1257#line 111 "featureselect.c"
1258 return;
1259}
1260}
1261#line 25 "featureselect.c"
1262int valid_product(void)
1263{ int retValue_acc ;
1264
1265 {
1266#line 129 "featureselect.c"
1267 retValue_acc = 1;
1268#line 131
1269 return (retValue_acc);
1270#line 138
1271 return (retValue_acc);
1272}
1273}