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 "MinePump.o"
369#pragma merger(0,"MinePump.i","")
370#line 6 "MinePump.h"
371void activatePump(void) ;
372#line 8
373void deactivatePump(void) ;
374#line 10
375int isPumpRunning(void) ;
376#line 7 "MinePump.c"
377int pumpRunning = 0;
378#line 9 "MinePump.c"
379int systemActive = 1;
380#line 10
381void __utac_acc__Specification1_spec__1(void) ;
382#line 16
383void processEnvironment(void) ;
384#line 12 "MinePump.c"
385void timeShift(void)
386{
387
388 {
389#line 15
390 if (pumpRunning) {
391 {
392#line 16
393 lowerWaterLevel();
394 }
395 } else {
396
397 }
398#line 15
399 if (systemActive) {
400 {
401#line 16
402 processEnvironment();
403 }
404 } else {
405
406 }
407 {
408#line 95 "MinePump.c"
409 __utac_acc__Specification1_spec__1();
410 }
411#line 101
412 return;
413}
414}
415#line 19 "MinePump.c"
416void processEnvironment(void)
417{
418
419 {
420#line 119 "MinePump.c"
421 return;
422}
423}
424#line 24 "MinePump.c"
425void activatePump(void)
426{
427
428 {
429#line 25
430 pumpRunning = 1;
431#line 139 "MinePump.c"
432 return;
433}
434}
435#line 29 "MinePump.c"
436void deactivatePump(void)
437{
438
439 {
440#line 30
441 pumpRunning = 0;
442#line 159 "MinePump.c"
443 return;
444}
445}
446#line 34 "MinePump.c"
447int isMethaneAlarm(void)
448{ int retValue_acc ;
449
450 {
451 {
452#line 177 "MinePump.c"
453 retValue_acc = isMethaneLevelCritical();
454 }
455#line 179
456 return (retValue_acc);
457#line 186
458 return (retValue_acc);
459}
460}
461#line 39 "MinePump.c"
462int isPumpRunning(void)
463{ int retValue_acc ;
464
465 {
466#line 208 "MinePump.c"
467 retValue_acc = pumpRunning;
468#line 210
469 return (retValue_acc);
470#line 217
471 return (retValue_acc);
472}
473}
474#line 44 "MinePump.c"
475void printPump(void)
476{
477
478 {
479 {
480#line 45
481 printf("Pump(System:");
482 }
483#line 46
484 if (systemActive) {
485 {
486#line 47
487 printf("On");
488 }
489 } else {
490 {
491#line 48
492 printf("Off");
493 }
494 }
495 {
496#line 50
497 printf(",Pump:");
498 }
499#line 51
500 if (pumpRunning) {
501 {
502#line 52
503 printf("On");
504 }
505 } else {
506 {
507#line 53
508 printf("Off");
509 }
510 }
511 {
512#line 55
513 printf(") ");
514#line 56
515 printEnvironment();
516#line 57
517 printf("\n");
518 }
519#line 257 "MinePump.c"
520 return;
521}
522}
523#line 1 "scenario.o"
524#pragma merger(0,"scenario.i","")
525#line 1 "scenario.c"
526void test(void)
527{ int splverifierCounter ;
528 int tmp ;
529 int tmp___0 ;
530 int tmp___1 ;
531 int tmp___2 ;
532
533 {
534#line 2
535 splverifierCounter = 0;
536 {
537#line 3
538 while (1) {
539 while_1_continue: ;
540#line 3
541 if (splverifierCounter < 4) {
542
543 } else {
544 goto while_1_break;
545 }
546 {
547#line 7
548 tmp = __VERIFIER_nondet_int();
549 }
550#line 7
551 if (tmp) {
552 {
553#line 5
554 waterRise();
555 }
556 } else {
557
558 }
559 {
560#line 7
561 tmp___0 = __VERIFIER_nondet_int();
562 }
563#line 7
564 if (tmp___0) {
565 {
566#line 8
567 changeMethaneLevel();
568 }
569 } else {
570
571 }
572 {
573#line 10
574 tmp___2 = __VERIFIER_nondet_int();
575 }
576#line 10
577 if (tmp___2) {
578
579 } else {
580 {
581#line 12
582 tmp___1 = __VERIFIER_nondet_int();
583 }
584#line 12
585 if (tmp___1) {
586
587 } else {
588
589 }
590 }
591 {
592#line 13
593 timeShift();
594 }
595 }
596 while_1_break: ;
597 }
598 {
599#line 15
600 cleanup();
601 }
602#line 74 "scenario.c"
603 return;
604}
605}
606#line 1 "Specification1_spec.o"
607#pragma merger(0,"Specification1_spec.i","")
608#line 4 "wsllib.h"
609void __automaton_fail(void) ;
610#line 11 "Specification1_spec.c"
611void __utac_acc__Specification1_spec__1(void)
612{ int tmp ;
613 int tmp___0 ;
614
615 {
616 {
617#line 17
618 tmp = isMethaneLevelCritical();
619 }
620#line 17
621 if (tmp) {
622 {
623#line 17
624 tmp___0 = isPumpRunning();
625 }
626#line 17
627 if (tmp___0) {
628 {
629#line 14
630 __automaton_fail();
631 }
632 } else {
633
634 }
635 } else {
636
637 }
638#line 14
639 return;
640}
641}
642#line 1 "wsllib_check.o"
643#pragma merger(0,"wsllib_check.i","")
644#line 3 "wsllib_check.c"
645void __automaton_fail(void)
646{
647
648 {
649 goto ERROR;
650 ERROR: ;
651#line 53 "wsllib_check.c"
652 return;
653}
654}
655#line 1 "libacc.o"
656#pragma merger(0,"libacc.i","")
657#line 73 "/usr/include/assert.h"
658extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
659 char const *__file ,
660 unsigned int __line ,
661 char const *__function ) ;
662#line 471 "/usr/include/stdlib.h"
663extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
664#line 488
665extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
666#line 32 "libacc.c"
667void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
668 int ) ,
669 int val )
670{ struct __UTAC__EXCEPTION *excep ;
671 struct __UTAC__CFLOW_FUNC *cf ;
672 void *tmp ;
673 unsigned long __cil_tmp7 ;
674 unsigned long __cil_tmp8 ;
675 unsigned long __cil_tmp9 ;
676 unsigned long __cil_tmp10 ;
677 unsigned long __cil_tmp11 ;
678 unsigned long __cil_tmp12 ;
679 unsigned long __cil_tmp13 ;
680 unsigned long __cil_tmp14 ;
681 int (**mem_15)(int , int ) ;
682 int *mem_16 ;
683 struct __UTAC__CFLOW_FUNC **mem_17 ;
684 struct __UTAC__CFLOW_FUNC **mem_18 ;
685 struct __UTAC__CFLOW_FUNC **mem_19 ;
686
687 {
688 {
689#line 33
690 excep = (struct __UTAC__EXCEPTION *)exception;
691#line 34
692 tmp = malloc(24UL);
693#line 34
694 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
695#line 36
696 mem_15 = (int (**)(int , int ))cf;
697#line 36
698 *mem_15 = cflow_func;
699#line 37
700 __cil_tmp7 = (unsigned long )cf;
701#line 37
702 __cil_tmp8 = __cil_tmp7 + 8;
703#line 37
704 mem_16 = (int *)__cil_tmp8;
705#line 37
706 *mem_16 = val;
707#line 38
708 __cil_tmp9 = (unsigned long )cf;
709#line 38
710 __cil_tmp10 = __cil_tmp9 + 16;
711#line 38
712 __cil_tmp11 = (unsigned long )excep;
713#line 38
714 __cil_tmp12 = __cil_tmp11 + 24;
715#line 38
716 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
717#line 38
718 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
719#line 38
720 *mem_17 = *mem_18;
721#line 39
722 __cil_tmp13 = (unsigned long )excep;
723#line 39
724 __cil_tmp14 = __cil_tmp13 + 24;
725#line 39
726 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
727#line 39
728 *mem_19 = cf;
729 }
730#line 654 "libacc.c"
731 return;
732}
733}
734#line 44 "libacc.c"
735void __utac__exception__cf_handler_free(void *exception )
736{ struct __UTAC__EXCEPTION *excep ;
737 struct __UTAC__CFLOW_FUNC *cf ;
738 struct __UTAC__CFLOW_FUNC *tmp ;
739 unsigned long __cil_tmp5 ;
740 unsigned long __cil_tmp6 ;
741 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
742 unsigned long __cil_tmp8 ;
743 unsigned long __cil_tmp9 ;
744 unsigned long __cil_tmp10 ;
745 unsigned long __cil_tmp11 ;
746 void *__cil_tmp12 ;
747 unsigned long __cil_tmp13 ;
748 unsigned long __cil_tmp14 ;
749 struct __UTAC__CFLOW_FUNC **mem_15 ;
750 struct __UTAC__CFLOW_FUNC **mem_16 ;
751 struct __UTAC__CFLOW_FUNC **mem_17 ;
752
753 {
754#line 45
755 excep = (struct __UTAC__EXCEPTION *)exception;
756#line 46
757 __cil_tmp5 = (unsigned long )excep;
758#line 46
759 __cil_tmp6 = __cil_tmp5 + 24;
760#line 46
761 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
762#line 46
763 cf = *mem_15;
764 {
765#line 49
766 while (1) {
767 while_2_continue: ;
768 {
769#line 49
770 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
771#line 49
772 __cil_tmp8 = (unsigned long )__cil_tmp7;
773#line 49
774 __cil_tmp9 = (unsigned long )cf;
775#line 49
776 if (__cil_tmp9 != __cil_tmp8) {
777
778 } else {
779 goto while_2_break;
780 }
781 }
782 {
783#line 50
784 tmp = cf;
785#line 51
786 __cil_tmp10 = (unsigned long )cf;
787#line 51
788 __cil_tmp11 = __cil_tmp10 + 16;
789#line 51
790 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
791#line 51
792 cf = *mem_16;
793#line 52
794 __cil_tmp12 = (void *)tmp;
795#line 52
796 free(__cil_tmp12);
797 }
798 }
799 while_2_break: ;
800 }
801#line 55
802 __cil_tmp13 = (unsigned long )excep;
803#line 55
804 __cil_tmp14 = __cil_tmp13 + 24;
805#line 55
806 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
807#line 55
808 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
809#line 694 "libacc.c"
810 return;
811}
812}
813#line 59 "libacc.c"
814void __utac__exception__cf_handler_reset(void *exception )
815{ struct __UTAC__EXCEPTION *excep ;
816 struct __UTAC__CFLOW_FUNC *cf ;
817 unsigned long __cil_tmp5 ;
818 unsigned long __cil_tmp6 ;
819 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
820 unsigned long __cil_tmp8 ;
821 unsigned long __cil_tmp9 ;
822 int (*__cil_tmp10)(int , int ) ;
823 unsigned long __cil_tmp11 ;
824 unsigned long __cil_tmp12 ;
825 int __cil_tmp13 ;
826 unsigned long __cil_tmp14 ;
827 unsigned long __cil_tmp15 ;
828 struct __UTAC__CFLOW_FUNC **mem_16 ;
829 int (**mem_17)(int , int ) ;
830 int *mem_18 ;
831 struct __UTAC__CFLOW_FUNC **mem_19 ;
832
833 {
834#line 60
835 excep = (struct __UTAC__EXCEPTION *)exception;
836#line 61
837 __cil_tmp5 = (unsigned long )excep;
838#line 61
839 __cil_tmp6 = __cil_tmp5 + 24;
840#line 61
841 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
842#line 61
843 cf = *mem_16;
844 {
845#line 64
846 while (1) {
847 while_3_continue: ;
848 {
849#line 64
850 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
851#line 64
852 __cil_tmp8 = (unsigned long )__cil_tmp7;
853#line 64
854 __cil_tmp9 = (unsigned long )cf;
855#line 64
856 if (__cil_tmp9 != __cil_tmp8) {
857
858 } else {
859 goto while_3_break;
860 }
861 }
862 {
863#line 65
864 mem_17 = (int (**)(int , int ))cf;
865#line 65
866 __cil_tmp10 = *mem_17;
867#line 65
868 __cil_tmp11 = (unsigned long )cf;
869#line 65
870 __cil_tmp12 = __cil_tmp11 + 8;
871#line 65
872 mem_18 = (int *)__cil_tmp12;
873#line 65
874 __cil_tmp13 = *mem_18;
875#line 65
876 (*__cil_tmp10)(4, __cil_tmp13);
877#line 66
878 __cil_tmp14 = (unsigned long )cf;
879#line 66
880 __cil_tmp15 = __cil_tmp14 + 16;
881#line 66
882 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
883#line 66
884 cf = *mem_19;
885 }
886 }
887 while_3_break: ;
888 }
889 {
890#line 69
891 __utac__exception__cf_handler_free(exception);
892 }
893#line 732 "libacc.c"
894 return;
895}
896}
897#line 80 "libacc.c"
898void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
899#line 80 "libacc.c"
900static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
901#line 79 "libacc.c"
902void *__utac__error_stack_mgt(void *env , int mode , int count )
903{ void *retValue_acc ;
904 struct __ACC__ERR *new ;
905 void *tmp ;
906 struct __ACC__ERR *temp ;
907 struct __ACC__ERR *next ;
908 void *excep ;
909 unsigned long __cil_tmp10 ;
910 unsigned long __cil_tmp11 ;
911 unsigned long __cil_tmp12 ;
912 unsigned long __cil_tmp13 ;
913 void *__cil_tmp14 ;
914 unsigned long __cil_tmp15 ;
915 unsigned long __cil_tmp16 ;
916 void *__cil_tmp17 ;
917 void **mem_18 ;
918 struct __ACC__ERR **mem_19 ;
919 struct __ACC__ERR **mem_20 ;
920 void **mem_21 ;
921 struct __ACC__ERR **mem_22 ;
922 void **mem_23 ;
923 void **mem_24 ;
924
925 {
926#line 82 "libacc.c"
927 if (count == 0) {
928#line 758 "libacc.c"
929 return (retValue_acc);
930 } else {
931
932 }
933#line 86 "libacc.c"
934 if (mode == 0) {
935 {
936#line 87
937 tmp = malloc(16UL);
938#line 87
939 new = (struct __ACC__ERR *)tmp;
940#line 88
941 mem_18 = (void **)new;
942#line 88
943 *mem_18 = env;
944#line 89
945 __cil_tmp10 = (unsigned long )new;
946#line 89
947 __cil_tmp11 = __cil_tmp10 + 8;
948#line 89
949 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
950#line 89
951 *mem_19 = head;
952#line 90
953 head = new;
954#line 776 "libacc.c"
955 retValue_acc = (void *)new;
956 }
957#line 778
958 return (retValue_acc);
959 } else {
960
961 }
962#line 94 "libacc.c"
963 if (mode == 1) {
964#line 95
965 temp = head;
966 {
967#line 98
968 while (1) {
969 while_4_continue: ;
970#line 98
971 if (count > 1) {
972
973 } else {
974 goto while_4_break;
975 }
976 {
977#line 99
978 __cil_tmp12 = (unsigned long )temp;
979#line 99
980 __cil_tmp13 = __cil_tmp12 + 8;
981#line 99
982 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
983#line 99
984 next = *mem_20;
985#line 100
986 mem_21 = (void **)temp;
987#line 100
988 excep = *mem_21;
989#line 101
990 __cil_tmp14 = (void *)temp;
991#line 101
992 free(__cil_tmp14);
993#line 102
994 __utac__exception__cf_handler_reset(excep);
995#line 103
996 temp = next;
997#line 104
998 count = count - 1;
999 }
1000 }
1001 while_4_break: ;
1002 }
1003 {
1004#line 107
1005 __cil_tmp15 = (unsigned long )temp;
1006#line 107
1007 __cil_tmp16 = __cil_tmp15 + 8;
1008#line 107
1009 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
1010#line 107
1011 head = *mem_22;
1012#line 108
1013 mem_23 = (void **)temp;
1014#line 108
1015 excep = *mem_23;
1016#line 109
1017 __cil_tmp17 = (void *)temp;
1018#line 109
1019 free(__cil_tmp17);
1020#line 110
1021 __utac__exception__cf_handler_reset(excep);
1022#line 820 "libacc.c"
1023 retValue_acc = excep;
1024 }
1025#line 822
1026 return (retValue_acc);
1027 } else {
1028
1029 }
1030#line 114
1031 if (mode == 2) {
1032#line 118 "libacc.c"
1033 if (head) {
1034#line 831
1035 mem_24 = (void **)head;
1036#line 831
1037 retValue_acc = *mem_24;
1038#line 833
1039 return (retValue_acc);
1040 } else {
1041#line 837 "libacc.c"
1042 retValue_acc = (void *)0;
1043#line 839
1044 return (retValue_acc);
1045 }
1046 } else {
1047
1048 }
1049#line 846 "libacc.c"
1050 return (retValue_acc);
1051}
1052}
1053#line 122 "libacc.c"
1054void *__utac__get_this_arg(int i , struct JoinPoint *this )
1055{ void *retValue_acc ;
1056 unsigned long __cil_tmp4 ;
1057 unsigned long __cil_tmp5 ;
1058 int __cil_tmp6 ;
1059 int __cil_tmp7 ;
1060 unsigned long __cil_tmp8 ;
1061 unsigned long __cil_tmp9 ;
1062 void **__cil_tmp10 ;
1063 void **__cil_tmp11 ;
1064 int *mem_12 ;
1065 void ***mem_13 ;
1066
1067 {
1068#line 123
1069 if (i > 0) {
1070 {
1071#line 123
1072 __cil_tmp4 = (unsigned long )this;
1073#line 123
1074 __cil_tmp5 = __cil_tmp4 + 16;
1075#line 123
1076 mem_12 = (int *)__cil_tmp5;
1077#line 123
1078 __cil_tmp6 = *mem_12;
1079#line 123
1080 if (i <= __cil_tmp6) {
1081
1082 } else {
1083 {
1084#line 123
1085 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1086 123U, "__utac__get_this_arg");
1087 }
1088 }
1089 }
1090 } else {
1091 {
1092#line 123
1093 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1094 123U, "__utac__get_this_arg");
1095 }
1096 }
1097#line 870 "libacc.c"
1098 __cil_tmp7 = i - 1;
1099#line 870
1100 __cil_tmp8 = (unsigned long )this;
1101#line 870
1102 __cil_tmp9 = __cil_tmp8 + 8;
1103#line 870
1104 mem_13 = (void ***)__cil_tmp9;
1105#line 870
1106 __cil_tmp10 = *mem_13;
1107#line 870
1108 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1109#line 870
1110 retValue_acc = *__cil_tmp11;
1111#line 872
1112 return (retValue_acc);
1113#line 879
1114 return (retValue_acc);
1115}
1116}
1117#line 129 "libacc.c"
1118char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
1119{ char const *retValue_acc ;
1120 unsigned long __cil_tmp4 ;
1121 unsigned long __cil_tmp5 ;
1122 int __cil_tmp6 ;
1123 int __cil_tmp7 ;
1124 unsigned long __cil_tmp8 ;
1125 unsigned long __cil_tmp9 ;
1126 char const **__cil_tmp10 ;
1127 char const **__cil_tmp11 ;
1128 int *mem_12 ;
1129 char const ***mem_13 ;
1130
1131 {
1132#line 131
1133 if (i > 0) {
1134 {
1135#line 131
1136 __cil_tmp4 = (unsigned long )this;
1137#line 131
1138 __cil_tmp5 = __cil_tmp4 + 16;
1139#line 131
1140 mem_12 = (int *)__cil_tmp5;
1141#line 131
1142 __cil_tmp6 = *mem_12;
1143#line 131
1144 if (i <= __cil_tmp6) {
1145
1146 } else {
1147 {
1148#line 131
1149 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1150 131U, "__utac__get_this_argtype");
1151 }
1152 }
1153 }
1154 } else {
1155 {
1156#line 131
1157 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1158 131U, "__utac__get_this_argtype");
1159 }
1160 }
1161#line 903 "libacc.c"
1162 __cil_tmp7 = i - 1;
1163#line 903
1164 __cil_tmp8 = (unsigned long )this;
1165#line 903
1166 __cil_tmp9 = __cil_tmp8 + 24;
1167#line 903
1168 mem_13 = (char const ***)__cil_tmp9;
1169#line 903
1170 __cil_tmp10 = *mem_13;
1171#line 903
1172 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1173#line 903
1174 retValue_acc = *__cil_tmp11;
1175#line 905
1176 return (retValue_acc);
1177#line 912
1178 return (retValue_acc);
1179}
1180}