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