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