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