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