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