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