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