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