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