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