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