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