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