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