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