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