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