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