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