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