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