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