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