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