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