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