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