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