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