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