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