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 "Test.o"
717#pragma merger(0,"Test.i","")
718#line 8 "Test.c"
719int cleanupTimeShifts = 4;
720#line 11 "Test.c"
721#line 20 "Test.c"
722void timeShift(void) ;
723#line 17 "Test.c"
724void cleanup(void)
725{ int i ;
726 int __cil_tmp2 ;
727
728 {
729 {
730#line 20
731 timeShift();
732#line 22
733 i = 0;
734 }
735 {
736#line 22
737 while (1) {
738 while_3_continue: ;
739 {
740#line 22
741 __cil_tmp2 = cleanupTimeShifts - 1;
742#line 22
743 if (i < __cil_tmp2) {
744
745 } else {
746 goto while_3_break;
747 }
748 }
749 {
750#line 23
751 timeShift();
752#line 22
753 i = i + 1;
754 }
755 }
756 while_3_break: ;
757 }
758#line 1111 "Test.c"
759 return;
760}
761}
762#line 57 "Test.c"
763void printPump(void) ;
764#line 56 "Test.c"
765void Specification2(void)
766{
767
768 {
769 {
770#line 57
771 timeShift();
772#line 57
773 printPump();
774#line 58
775 timeShift();
776#line 58
777 printPump();
778#line 59
779 timeShift();
780#line 59
781 printPump();
782#line 60
783 waterRise();
784#line 60
785 printPump();
786#line 61
787 timeShift();
788#line 61
789 printPump();
790#line 62
791 changeMethaneLevel();
792#line 62
793 printPump();
794#line 63
795 timeShift();
796#line 63
797 printPump();
798#line 64
799 cleanup();
800 }
801#line 1159 "Test.c"
802 return;
803}
804}
805#line 67 "Test.c"
806void setup(void)
807{
808
809 {
810#line 1177 "Test.c"
811 return;
812}
813}
814#line 1179
815void __utac_acc__Specification2_spec__1(void) ;
816#line 77 "Test.c"
817void test(void) ;
818#line 74 "Test.c"
819void runTest(void)
820{
821
822 {
823 {
824#line 1190 "Test.c"
825 __utac_acc__Specification2_spec__1();
826#line 77 "Test.c"
827 test();
828 }
829#line 1205 "Test.c"
830 return;
831}
832}
833#line 83 "Test.c"
834void select_helpers(void) ;
835#line 84
836void select_features(void) ;
837#line 85
838int valid_product(void) ;
839#line 82 "Test.c"
840int main(void)
841{ int retValue_acc ;
842 int tmp ;
843
844 {
845 {
846#line 83
847 select_helpers();
848#line 84
849 select_features();
850#line 85
851 tmp = valid_product();
852 }
853#line 85
854 if (tmp) {
855 {
856#line 86
857 setup();
858#line 87
859 runTest();
860 }
861 } else {
862
863 }
864#line 1234 "Test.c"
865 retValue_acc = 0;
866#line 1236
867 return (retValue_acc);
868#line 1243
869 return (retValue_acc);
870}
871}
872#line 1 "featureselect.o"
873#pragma merger(0,"featureselect.i","")
874#line 8 "featureselect.h"
875int select_one(void) ;
876#line 8 "featureselect.c"
877int select_one(void)
878{ int retValue_acc ;
879 int choice = __VERIFIER_nondet_int();
880
881 {
882#line 62 "featureselect.c"
883 retValue_acc = choice;
884#line 64
885 return (retValue_acc);
886#line 71
887 return (retValue_acc);
888}
889}
890#line 14 "featureselect.c"
891void select_features(void)
892{
893
894 {
895#line 93 "featureselect.c"
896 return;
897}
898}
899#line 20 "featureselect.c"
900void select_helpers(void)
901{
902
903 {
904#line 111 "featureselect.c"
905 return;
906}
907}
908#line 25 "featureselect.c"
909int valid_product(void)
910{ int retValue_acc ;
911
912 {
913#line 129 "featureselect.c"
914 retValue_acc = 1;
915#line 131
916 return (retValue_acc);
917#line 138
918 return (retValue_acc);
919}
920}
921#line 1 "Specification2_spec.o"
922#pragma merger(0,"Specification2_spec.i","")
923#line 4 "wsllib.h"
924void __automaton_fail(void) ;
925#line 10 "MinePump.h"
926int isPumpRunning(void) ;
927#line 7 "Specification2_spec.c"
928int methAndRunningLastTime ;
929#line 11 "Specification2_spec.c"
930void __utac_acc__Specification2_spec__1(void)
931{
932
933 {
934#line 13
935 methAndRunningLastTime = 0;
936#line 13
937 return;
938}
939}
940#line 17 "Specification2_spec.c"
941__inline void __utac_acc__Specification2_spec__2(void)
942{ int tmp ;
943 int tmp___0 ;
944
945 {
946 {
947#line 27
948 tmp = isMethaneLevelCritical();
949 }
950#line 27
951 if (tmp) {
952 {
953#line 27
954 tmp___0 = isPumpRunning();
955 }
956#line 27
957 if (tmp___0) {
958#line 24
959 if (methAndRunningLastTime) {
960 {
961#line 21
962 __automaton_fail();
963 }
964 } else {
965#line 23
966 methAndRunningLastTime = 1;
967 }
968 } else {
969#line 26
970 methAndRunningLastTime = 0;
971 }
972 } else {
973#line 26
974 methAndRunningLastTime = 0;
975 }
976#line 26
977 return;
978}
979}
980#line 1 "scenario.o"
981#pragma merger(0,"scenario.i","")
982#line 12 "scenario.c"
983void stopSystem(void) ;
984#line 1 "scenario.c"
985void test(void)
986{ int splverifierCounter ;
987 int tmp ;
988 int tmp___0 ;
989 int tmp___1 ;
990 int tmp___2 ;
991
992 {
993#line 2
994 splverifierCounter = 0;
995 {
996#line 3
997 while (1) {
998 while_4_continue: ;
999#line 3
1000 if (splverifierCounter < 4) {
1001
1002 } else {
1003 goto while_4_break;
1004 }
1005 {
1006#line 7
1007 tmp = __VERIFIER_nondet_int();
1008 }
1009#line 7
1010 if (tmp) {
1011 {
1012#line 5
1013 waterRise();
1014 }
1015 } else {
1016
1017 }
1018 {
1019#line 7
1020 tmp___0 = __VERIFIER_nondet_int();
1021 }
1022#line 7
1023 if (tmp___0) {
1024 {
1025#line 8
1026 changeMethaneLevel();
1027 }
1028 } else {
1029
1030 }
1031 {
1032#line 10
1033 tmp___2 = __VERIFIER_nondet_int();
1034 }
1035#line 10
1036 if (tmp___2) {
1037
1038 } else {
1039 {
1040#line 12
1041 tmp___1 = __VERIFIER_nondet_int();
1042 }
1043#line 12
1044 if (tmp___1) {
1045 {
1046#line 12
1047 stopSystem();
1048 }
1049 } else {
1050
1051 }
1052 }
1053 {
1054#line 14
1055 timeShift();
1056 }
1057 }
1058 while_4_break: ;
1059 }
1060 {
1061#line 16
1062 cleanup();
1063 }
1064#line 76 "scenario.c"
1065 return;
1066}
1067}
1068#line 1 "MinePump.o"
1069#pragma merger(0,"MinePump.i","")
1070#line 6 "MinePump.h"
1071void activatePump(void) ;
1072#line 8
1073void deactivatePump(void) ;
1074#line 7 "MinePump.c"
1075int pumpRunning = 0;
1076#line 9 "MinePump.c"
1077int systemActive = 1;
1078#line 16
1079void processEnvironment(void) ;
1080#line 12 "MinePump.c"
1081void timeShift(void)
1082{
1083
1084 {
1085#line 15
1086 if (pumpRunning) {
1087 {
1088#line 16
1089 lowerWaterLevel();
1090 }
1091 } else {
1092
1093 }
1094#line 15
1095 if (systemActive) {
1096 {
1097#line 16
1098 processEnvironment();
1099 }
1100 } else {
1101
1102 }
1103 {
1104#line 99 "MinePump.c"
1105 __utac_acc__Specification2_spec__2();
1106 }
1107#line 105
1108 return;
1109}
1110}
1111#line 19 "MinePump.c"
1112void processEnvironment__wrappee__base(void)
1113{
1114
1115 {
1116#line 123 "MinePump.c"
1117 return;
1118}
1119}
1120#line 28 "MinePump.c"
1121int isHighWaterLevel(void) ;
1122#line 23 "MinePump.c"
1123void processEnvironment(void)
1124{ int tmp ;
1125
1126 {
1127#line 28
1128 if (! pumpRunning) {
1129 {
1130#line 28
1131 tmp = isHighWaterLevel();
1132 }
1133#line 28
1134 if (tmp) {
1135 {
1136#line 25
1137 activatePump();
1138 }
1139 } else {
1140 {
1141#line 27
1142 processEnvironment__wrappee__base();
1143 }
1144 }
1145 } else {
1146 {
1147#line 27
1148 processEnvironment__wrappee__base();
1149 }
1150 }
1151#line 149 "MinePump.c"
1152 return;
1153}
1154}
1155#line 32 "MinePump.c"
1156void activatePump__wrappee__highWaterSensor(void)
1157{
1158
1159 {
1160#line 33
1161 pumpRunning = 1;
1162#line 169 "MinePump.c"
1163 return;
1164}
1165}
1166#line 40 "MinePump.c"
1167int isMethaneAlarm(void) ;
1168#line 35 "MinePump.c"
1169void activatePump(void)
1170{ int tmp ;
1171
1172 {
1173 {
1174#line 40
1175 tmp = isMethaneAlarm();
1176 }
1177#line 40
1178 if (tmp) {
1179
1180 } else {
1181 {
1182#line 37
1183 activatePump__wrappee__highWaterSensor();
1184 }
1185 }
1186#line 193 "MinePump.c"
1187 return;
1188}
1189}
1190#line 44 "MinePump.c"
1191void deactivatePump(void)
1192{
1193
1194 {
1195#line 45
1196 pumpRunning = 0;
1197#line 213 "MinePump.c"
1198 return;
1199}
1200}
1201#line 49 "MinePump.c"
1202int isMethaneAlarm(void)
1203{ int retValue_acc ;
1204
1205 {
1206 {
1207#line 231 "MinePump.c"
1208 retValue_acc = isMethaneLevelCritical();
1209 }
1210#line 233
1211 return (retValue_acc);
1212#line 240
1213 return (retValue_acc);
1214}
1215}
1216#line 54 "MinePump.c"
1217int isPumpRunning(void)
1218{ int retValue_acc ;
1219
1220 {
1221#line 262 "MinePump.c"
1222 retValue_acc = pumpRunning;
1223#line 264
1224 return (retValue_acc);
1225#line 271
1226 return (retValue_acc);
1227}
1228}
1229#line 59 "MinePump.c"
1230void printPump(void)
1231{
1232
1233 {
1234 {
1235#line 60
1236 printf("Pump(System:");
1237 }
1238#line 61
1239 if (systemActive) {
1240 {
1241#line 62
1242 printf("On");
1243 }
1244 } else {
1245 {
1246#line 63
1247 printf("Off");
1248 }
1249 }
1250 {
1251#line 65
1252 printf(",Pump:");
1253 }
1254#line 66
1255 if (pumpRunning) {
1256 {
1257#line 67
1258 printf("On");
1259 }
1260 } else {
1261 {
1262#line 68
1263 printf("Off");
1264 }
1265 }
1266 {
1267#line 70
1268 printf(") ");
1269#line 71
1270 printEnvironment();
1271#line 72
1272 printf("\n");
1273 }
1274#line 311 "MinePump.c"
1275 return;
1276}
1277}
1278#line 74 "MinePump.c"
1279int isHighWaterLevel(void)
1280{ int retValue_acc ;
1281 int tmp ;
1282 int tmp___0 ;
1283
1284 {
1285 {
1286#line 329 "MinePump.c"
1287 tmp = isHighWaterSensorDry();
1288 }
1289#line 329
1290 if (tmp) {
1291#line 329
1292 tmp___0 = 0;
1293 } else {
1294#line 329
1295 tmp___0 = 1;
1296 }
1297#line 329
1298 retValue_acc = tmp___0;
1299#line 331
1300 return (retValue_acc);
1301#line 338
1302 return (retValue_acc);
1303}
1304}
1305#line 77 "MinePump.c"
1306void stopSystem(void)
1307{
1308
1309 {
1310#line 82
1311 if (pumpRunning) {
1312 {
1313#line 79
1314 deactivatePump();
1315 }
1316 } else {
1317
1318 }
1319#line 82
1320 systemActive = 0;
1321#line 367 "MinePump.c"
1322 return;
1323}
1324}
1325#line 1 "wsllib_check.o"
1326#pragma merger(0,"wsllib_check.i","")
1327#line 3 "wsllib_check.c"
1328void __automaton_fail(void)
1329{
1330
1331 {
1332 goto ERROR;
1333 ERROR: ;
1334#line 53 "wsllib_check.c"
1335 return;
1336}
1337}