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