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