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