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