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 "featureselect.o"
199#pragma merger(0,"featureselect.i","")
200#line 8 "featureselect.h"
201int select_one(void) ;
202#line 8 "featureselect.c"
203int select_one(void)
204{ int retValue_acc ;
205 int choice = __VERIFIER_nondet_int();
206
207 {
208#line 62 "featureselect.c"
209 retValue_acc = choice;
210#line 64
211 return (retValue_acc);
212#line 71
213 return (retValue_acc);
214}
215}
216#line 14 "featureselect.c"
217void select_features(void)
218{
219
220 {
221#line 93 "featureselect.c"
222 return;
223}
224}
225#line 20 "featureselect.c"
226void select_helpers(void)
227{
228
229 {
230#line 111 "featureselect.c"
231 return;
232}
233}
234#line 25 "featureselect.c"
235int valid_product(void)
236{ int retValue_acc ;
237
238 {
239#line 129 "featureselect.c"
240 retValue_acc = 1;
241#line 131
242 return (retValue_acc);
243#line 138
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 "Environment.o"
774#pragma merger(0,"Environment.i","")
775#line 4 "Environment.h"
776void lowerWaterLevel(void) ;
777#line 10
778int isMethaneLevelCritical(void) ;
779#line 12
780int getWaterLevel(void) ;
781#line 15
782void printEnvironment(void) ;
783#line 16
784int isLowWaterSensorDry(void) ;
785#line 9 "Environment.c"
786int waterLevel = 1;
787#line 12 "Environment.c"
788int methaneLevelCritical = 0;
789#line 15 "Environment.c"
790void lowerWaterLevel(void)
791{
792
793 {
794#line 19
795 if (waterLevel > 0) {
796#line 17
797 waterLevel = waterLevel - 1;
798 } else {
799
800 }
801#line 83 "Environment.c"
802 return;
803}
804}
805#line 22 "Environment.c"
806void waterRise(void)
807{
808
809 {
810#line 26
811 if (waterLevel < 2) {
812#line 24
813 waterLevel = waterLevel + 1;
814 } else {
815
816 }
817#line 106 "Environment.c"
818 return;
819}
820}
821#line 29 "Environment.c"
822void changeMethaneLevel(void)
823{
824
825 {
826#line 34
827 if (methaneLevelCritical) {
828#line 31
829 methaneLevelCritical = 0;
830 } else {
831#line 33
832 methaneLevelCritical = 1;
833 }
834#line 132 "Environment.c"
835 return;
836}
837}
838#line 38 "Environment.c"
839int isMethaneLevelCritical(void)
840{ int retValue_acc ;
841
842 {
843#line 150 "Environment.c"
844 retValue_acc = methaneLevelCritical;
845#line 152
846 return (retValue_acc);
847#line 159
848 return (retValue_acc);
849}
850}
851#line 45 "Environment.c"
852#line 44 "Environment.c"
853void printEnvironment(void)
854{
855
856 {
857 {
858#line 45
859 printf("Env(Water:%i", waterLevel);
860#line 46
861 printf(",Meth:");
862 }
863#line 47
864 if (methaneLevelCritical) {
865 {
866#line 48
867 printf("CRIT");
868 }
869 } else {
870 {
871#line 49
872 printf("OK");
873 }
874 }
875 {
876#line 51
877 printf(")");
878 }
879#line 191 "Environment.c"
880 return;
881}
882}
883#line 55 "Environment.c"
884int getWaterLevel(void)
885{ int retValue_acc ;
886
887 {
888#line 209 "Environment.c"
889 retValue_acc = waterLevel;
890#line 211
891 return (retValue_acc);
892#line 218
893 return (retValue_acc);
894}
895}
896#line 58 "Environment.c"
897int isLowWaterSensorDry(void)
898{ int retValue_acc ;
899
900 {
901#line 240 "Environment.c"
902 retValue_acc = waterLevel == 0;
903#line 242
904 return (retValue_acc);
905#line 249
906 return (retValue_acc);
907}
908}
909#line 1 "scenario.o"
910#pragma merger(0,"scenario.i","")
911#line 12 "scenario.c"
912void stopSystem(void) ;
913#line 1 "scenario.c"
914void test(void)
915{ int splverifierCounter ;
916 int tmp ;
917 int tmp___0 ;
918 int tmp___1 ;
919 int tmp___2 ;
920
921 {
922#line 2
923 splverifierCounter = 0;
924 {
925#line 3
926 while (1) {
927 while_4_continue: ;
928#line 3
929 if (splverifierCounter < 4) {
930
931 } else {
932 goto while_4_break;
933 }
934 {
935#line 7
936 tmp = __VERIFIER_nondet_int();
937 }
938#line 7
939 if (tmp) {
940 {
941#line 5
942 waterRise();
943 }
944 } else {
945
946 }
947 {
948#line 7
949 tmp___0 = __VERIFIER_nondet_int();
950 }
951#line 7
952 if (tmp___0) {
953 {
954#line 8
955 changeMethaneLevel();
956 }
957 } else {
958
959 }
960 {
961#line 10
962 tmp___2 = __VERIFIER_nondet_int();
963 }
964#line 10
965 if (tmp___2) {
966
967 } else {
968 {
969#line 12
970 tmp___1 = __VERIFIER_nondet_int();
971 }
972#line 12
973 if (tmp___1) {
974 {
975#line 12
976 stopSystem();
977 }
978 } else {
979
980 }
981 }
982 {
983#line 14
984 timeShift();
985 }
986 }
987 while_4_break: ;
988 }
989 {
990#line 16
991 cleanup();
992 }
993#line 76 "scenario.c"
994 return;
995}
996}
997#line 1 "MinePump.o"
998#pragma merger(0,"MinePump.i","")
999#line 6 "MinePump.h"
1000void activatePump(void) ;
1001#line 8
1002void deactivatePump(void) ;
1003#line 10
1004int isPumpRunning(void) ;
1005#line 7 "MinePump.c"
1006int pumpRunning = 0;
1007#line 9 "MinePump.c"
1008int systemActive = 1;
1009#line 10
1010void __utac_acc__Specification4_spec__1(void) ;
1011#line 16
1012void processEnvironment(void) ;
1013#line 12 "MinePump.c"
1014void timeShift(void)
1015{
1016
1017 {
1018#line 15
1019 if (pumpRunning) {
1020 {
1021#line 16
1022 lowerWaterLevel();
1023 }
1024 } else {
1025
1026 }
1027#line 15
1028 if (systemActive) {
1029 {
1030#line 16
1031 processEnvironment();
1032 }
1033 } else {
1034
1035 }
1036 {
1037#line 99 "MinePump.c"
1038 __utac_acc__Specification4_spec__1();
1039 }
1040#line 105
1041 return;
1042}
1043}
1044#line 19 "MinePump.c"
1045void processEnvironment__wrappee__base(void)
1046{
1047
1048 {
1049#line 123 "MinePump.c"
1050 return;
1051}
1052}
1053#line 28 "MinePump.c"
1054int isLowWaterLevel(void) ;
1055#line 23 "MinePump.c"
1056void processEnvironment__wrappee__methaneQuery(void)
1057{ int tmp ;
1058
1059 {
1060#line 28
1061 if (pumpRunning) {
1062 {
1063#line 28
1064 tmp = isLowWaterLevel();
1065 }
1066#line 28
1067 if (tmp) {
1068 {
1069#line 25
1070 deactivatePump();
1071 }
1072 } else {
1073 {
1074#line 27
1075 processEnvironment__wrappee__base();
1076 }
1077 }
1078 } else {
1079 {
1080#line 27
1081 processEnvironment__wrappee__base();
1082 }
1083 }
1084#line 149 "MinePump.c"
1085 return;
1086}
1087}
1088#line 35 "MinePump.c"
1089int isMethaneAlarm(void) ;
1090#line 30 "MinePump.c"
1091void processEnvironment(void)
1092{ int tmp ;
1093
1094 {
1095#line 35
1096 if (pumpRunning) {
1097 {
1098#line 35
1099 tmp = isMethaneAlarm();
1100 }
1101#line 35
1102 if (tmp) {
1103 {
1104#line 32
1105 deactivatePump();
1106 }
1107 } else {
1108 {
1109#line 34
1110 processEnvironment__wrappee__methaneQuery();
1111 }
1112 }
1113 } else {
1114 {
1115#line 34
1116 processEnvironment__wrappee__methaneQuery();
1117 }
1118 }
1119#line 175 "MinePump.c"
1120 return;
1121}
1122}
1123#line 39 "MinePump.c"
1124void activatePump__wrappee__lowWaterSensor(void)
1125{
1126
1127 {
1128#line 40
1129 pumpRunning = 1;
1130#line 195 "MinePump.c"
1131 return;
1132}
1133}
1134#line 42 "MinePump.c"
1135void activatePump(void)
1136{ int tmp ;
1137
1138 {
1139 {
1140#line 47
1141 tmp = isMethaneAlarm();
1142 }
1143#line 47
1144 if (tmp) {
1145
1146 } else {
1147 {
1148#line 44
1149 activatePump__wrappee__lowWaterSensor();
1150 }
1151 }
1152#line 219 "MinePump.c"
1153 return;
1154}
1155}
1156#line 51 "MinePump.c"
1157void deactivatePump(void)
1158{
1159
1160 {
1161#line 52
1162 pumpRunning = 0;
1163#line 239 "MinePump.c"
1164 return;
1165}
1166}
1167#line 56 "MinePump.c"
1168int isMethaneAlarm(void)
1169{ int retValue_acc ;
1170
1171 {
1172 {
1173#line 257 "MinePump.c"
1174 retValue_acc = isMethaneLevelCritical();
1175 }
1176#line 259
1177 return (retValue_acc);
1178#line 266
1179 return (retValue_acc);
1180}
1181}
1182#line 61 "MinePump.c"
1183int isPumpRunning(void)
1184{ int retValue_acc ;
1185
1186 {
1187#line 288 "MinePump.c"
1188 retValue_acc = pumpRunning;
1189#line 290
1190 return (retValue_acc);
1191#line 297
1192 return (retValue_acc);
1193}
1194}
1195#line 66 "MinePump.c"
1196void printPump(void)
1197{
1198
1199 {
1200 {
1201#line 67
1202 printf("Pump(System:");
1203 }
1204#line 68
1205 if (systemActive) {
1206 {
1207#line 69
1208 printf("On");
1209 }
1210 } else {
1211 {
1212#line 70
1213 printf("Off");
1214 }
1215 }
1216 {
1217#line 72
1218 printf(",Pump:");
1219 }
1220#line 73
1221 if (pumpRunning) {
1222 {
1223#line 74
1224 printf("On");
1225 }
1226 } else {
1227 {
1228#line 75
1229 printf("Off");
1230 }
1231 }
1232 {
1233#line 77
1234 printf(") ");
1235#line 78
1236 printEnvironment();
1237#line 79
1238 printf("\n");
1239 }
1240#line 337 "MinePump.c"
1241 return;
1242}
1243}
1244#line 81 "MinePump.c"
1245int isLowWaterLevel(void)
1246{ int retValue_acc ;
1247 int tmp ;
1248 int tmp___0 ;
1249
1250 {
1251 {
1252#line 355 "MinePump.c"
1253 tmp = isLowWaterSensorDry();
1254 }
1255#line 355
1256 if (tmp) {
1257#line 355
1258 tmp___0 = 0;
1259 } else {
1260#line 355
1261 tmp___0 = 1;
1262 }
1263#line 355
1264 retValue_acc = tmp___0;
1265#line 357
1266 return (retValue_acc);
1267#line 364
1268 return (retValue_acc);
1269}
1270}
1271#line 84 "MinePump.c"
1272void stopSystem(void)
1273{
1274
1275 {
1276#line 89
1277 if (pumpRunning) {
1278 {
1279#line 86
1280 deactivatePump();
1281 }
1282 } else {
1283
1284 }
1285#line 89
1286 systemActive = 0;
1287#line 393 "MinePump.c"
1288 return;
1289}
1290}
1291#line 1 "Specification4_spec.o"
1292#pragma merger(0,"Specification4_spec.i","")
1293#line 4 "wsllib.h"
1294void __automaton_fail(void) ;
1295#line 11 "Specification4_spec.c"
1296void __utac_acc__Specification4_spec__1(void)
1297{ int tmp ;
1298 int tmp___0 ;
1299
1300 {
1301 {
1302#line 17
1303 tmp = getWaterLevel();
1304 }
1305#line 17
1306 if (tmp == 0) {
1307 {
1308#line 17
1309 tmp___0 = isPumpRunning();
1310 }
1311#line 17
1312 if (tmp___0) {
1313 {
1314#line 14
1315 __automaton_fail();
1316 }
1317 } else {
1318
1319 }
1320 } else {
1321
1322 }
1323#line 14
1324 return;
1325}
1326}
1327#line 1 "wsllib_check.o"
1328#pragma merger(0,"wsllib_check.i","")
1329#line 3 "wsllib_check.c"
1330void __automaton_fail(void)
1331{
1332
1333 {
1334 goto ERROR;
1335 ERROR: ;
1336#line 53 "wsllib_check.c"
1337 return;
1338}
1339}