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