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