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