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