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