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