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