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