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