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