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