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