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