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