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