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