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