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