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