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