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