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