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