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