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