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