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