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