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