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