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