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