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