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