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