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