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