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