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