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