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 "Environment.o"
43#pragma merger(0,"Environment.i","")
44#line 4 "Environment.h"
45void lowerWaterLevel(void) ;
46#line 6
47void waterRise(void) ;
48#line 8
49void changeMethaneLevel(void) ;
50#line 10
51int isMethaneLevelCritical(void) ;
52#line 12
53int getWaterLevel(void) ;
54#line 15
55void printEnvironment(void) ;
56#line 16
57int isHighWaterSensorDry(void) ;
58#line 17
59int isLowWaterSensorDry(void) ;
60#line 9 "Environment.c"
61int waterLevel = 1;
62#line 12 "Environment.c"
63int methaneLevelCritical = 0;
64#line 15 "Environment.c"
65void lowerWaterLevel(void)
66{
67
68 {
69#line 19
70 if (waterLevel > 0) {
71#line 17
72 waterLevel = waterLevel - 1;
73 } else {
74
75 }
76#line 85 "Environment.c"
77 return;
78}
79}
80#line 22 "Environment.c"
81void waterRise(void)
82{
83
84 {
85#line 26
86 if (waterLevel < 2) {
87#line 24
88 waterLevel = waterLevel + 1;
89 } else {
90
91 }
92#line 108 "Environment.c"
93 return;
94}
95}
96#line 29 "Environment.c"
97void changeMethaneLevel(void)
98{
99
100 {
101#line 34
102 if (methaneLevelCritical) {
103#line 31
104 methaneLevelCritical = 0;
105 } else {
106#line 33
107 methaneLevelCritical = 1;
108 }
109#line 134 "Environment.c"
110 return;
111}
112}
113#line 38 "Environment.c"
114int isMethaneLevelCritical(void)
115{ int retValue_acc ;
116
117 {
118#line 152 "Environment.c"
119 retValue_acc = methaneLevelCritical;
120#line 154
121 return (retValue_acc);
122#line 161
123 return (retValue_acc);
124}
125}
126#line 45 "Environment.c"
127#line 44 "Environment.c"
128void printEnvironment(void)
129{
130
131 {
132 {
133#line 45
134 printf("Env(Water:%i", waterLevel);
135#line 46
136 printf(",Meth:");
137 }
138#line 47
139 if (methaneLevelCritical) {
140 {
141#line 48
142 printf("CRIT");
143 }
144 } else {
145 {
146#line 49
147 printf("OK");
148 }
149 }
150 {
151#line 51
152 printf(")");
153 }
154#line 193 "Environment.c"
155 return;
156}
157}
158#line 55 "Environment.c"
159int getWaterLevel(void)
160{ int retValue_acc ;
161
162 {
163#line 211 "Environment.c"
164 retValue_acc = waterLevel;
165#line 213
166 return (retValue_acc);
167#line 220
168 return (retValue_acc);
169}
170}
171#line 58 "Environment.c"
172int isHighWaterSensorDry(void)
173{ int retValue_acc ;
174
175 {
176#line 65 "Environment.c"
177 if (waterLevel < 2) {
178#line 245
179 retValue_acc = 1;
180#line 247
181 return (retValue_acc);
182 } else {
183#line 253 "Environment.c"
184 retValue_acc = 0;
185#line 255
186 return (retValue_acc);
187 }
188#line 262 "Environment.c"
189 return (retValue_acc);
190}
191}
192#line 67 "Environment.c"
193int isLowWaterSensorDry(void)
194{ int retValue_acc ;
195
196 {
197#line 284 "Environment.c"
198 retValue_acc = waterLevel == 0;
199#line 286
200 return (retValue_acc);
201#line 293
202 return (retValue_acc);
203}
204}
205#line 1 "scenario.o"
206#pragma merger(0,"scenario.i","")
207#line 7 "scenario.c"
208#line 12
209void stopSystem(void) ;
210#line 14
211void timeShift(void) ;
212#line 16
213void cleanup(void) ;
214#line 1 "scenario.c"
215void test(void)
216{ int splverifierCounter ;
217 int tmp ;
218 int tmp___0 ;
219 int tmp___1 ;
220 int tmp___2 ;
221
222 {
223#line 2
224 splverifierCounter = 0;
225 {
226#line 3
227 while (1) {
228 while_0_continue: ;
229#line 3
230 if (splverifierCounter < 4) {
231
232 } else {
233 goto while_0_break;
234 }
235 {
236#line 7
237 tmp = __VERIFIER_nondet_int();
238 }
239#line 7
240 if (tmp) {
241 {
242#line 5
243 waterRise();
244 }
245 } else {
246
247 }
248 {
249#line 7
250 tmp___0 = __VERIFIER_nondet_int();
251 }
252#line 7
253 if (tmp___0) {
254 {
255#line 8
256 changeMethaneLevel();
257 }
258 } else {
259
260 }
261 {
262#line 10
263 tmp___2 = __VERIFIER_nondet_int();
264 }
265#line 10
266 if (tmp___2) {
267
268 } else {
269 {
270#line 12
271 tmp___1 = __VERIFIER_nondet_int();
272 }
273#line 12
274 if (tmp___1) {
275 {
276#line 12
277 stopSystem();
278 }
279 } else {
280
281 }
282 }
283 {
284#line 14
285 timeShift();
286 }
287 }
288 while_0_break: ;
289 }
290 {
291#line 16
292 cleanup();
293 }
294#line 76 "scenario.c"
295 return;
296}
297}
298#line 1 "MinePump.o"
299#pragma merger(0,"MinePump.i","")
300#line 6 "MinePump.h"
301void activatePump(void) ;
302#line 8
303void deactivatePump(void) ;
304#line 10
305int isPumpRunning(void) ;
306#line 13
307void printPump(void) ;
308#line 7 "MinePump.c"
309int pumpRunning = 0;
310#line 9 "MinePump.c"
311int systemActive = 1;
312#line 10
313void __utac_acc__Specification3_spec__1(void) ;
314#line 16
315void processEnvironment(void) ;
316#line 12 "MinePump.c"
317void timeShift(void)
318{
319
320 {
321#line 15
322 if (pumpRunning) {
323 {
324#line 16
325 lowerWaterLevel();
326 }
327 } else {
328
329 }
330#line 15
331 if (systemActive) {
332 {
333#line 16
334 processEnvironment();
335 }
336 } else {
337
338 }
339 {
340#line 101 "MinePump.c"
341 __utac_acc__Specification3_spec__1();
342 }
343#line 107
344 return;
345}
346}
347#line 19 "MinePump.c"
348void processEnvironment__wrappee__base(void)
349{
350
351 {
352#line 125 "MinePump.c"
353 return;
354}
355}
356#line 28 "MinePump.c"
357int isHighWaterLevel(void) ;
358#line 23 "MinePump.c"
359void processEnvironment__wrappee__highWaterSensor(void)
360{ int tmp ;
361
362 {
363#line 28
364 if (! pumpRunning) {
365 {
366#line 28
367 tmp = isHighWaterLevel();
368 }
369#line 28
370 if (tmp) {
371 {
372#line 25
373 activatePump();
374 }
375 } else {
376 {
377#line 27
378 processEnvironment__wrappee__base();
379 }
380 }
381 } else {
382 {
383#line 27
384 processEnvironment__wrappee__base();
385 }
386 }
387#line 151 "MinePump.c"
388 return;
389}
390}
391#line 36 "MinePump.c"
392int isLowWaterLevel(void) ;
393#line 31 "MinePump.c"
394void processEnvironment(void)
395{ int tmp ;
396
397 {
398#line 36
399 if (pumpRunning) {
400 {
401#line 36
402 tmp = isLowWaterLevel();
403 }
404#line 36
405 if (tmp) {
406 {
407#line 33
408 deactivatePump();
409 }
410 } else {
411 {
412#line 35
413 processEnvironment__wrappee__highWaterSensor();
414 }
415 }
416 } else {
417 {
418#line 35
419 processEnvironment__wrappee__highWaterSensor();
420 }
421 }
422#line 177 "MinePump.c"
423 return;
424}
425}
426#line 40 "MinePump.c"
427void activatePump(void)
428{
429
430 {
431#line 41
432 pumpRunning = 1;
433#line 197 "MinePump.c"
434 return;
435}
436}
437#line 45 "MinePump.c"
438void deactivatePump(void)
439{
440
441 {
442#line 46
443 pumpRunning = 0;
444#line 217 "MinePump.c"
445 return;
446}
447}
448#line 50 "MinePump.c"
449int isMethaneAlarm(void)
450{ int retValue_acc ;
451
452 {
453 {
454#line 235 "MinePump.c"
455 retValue_acc = isMethaneLevelCritical();
456 }
457#line 237
458 return (retValue_acc);
459#line 244
460 return (retValue_acc);
461}
462}
463#line 55 "MinePump.c"
464int isPumpRunning(void)
465{ int retValue_acc ;
466
467 {
468#line 266 "MinePump.c"
469 retValue_acc = pumpRunning;
470#line 268
471 return (retValue_acc);
472#line 275
473 return (retValue_acc);
474}
475}
476#line 60 "MinePump.c"
477void printPump(void)
478{
479
480 {
481 {
482#line 61
483 printf("Pump(System:");
484 }
485#line 62
486 if (systemActive) {
487 {
488#line 63
489 printf("On");
490 }
491 } else {
492 {
493#line 64
494 printf("Off");
495 }
496 }
497 {
498#line 66
499 printf(",Pump:");
500 }
501#line 67
502 if (pumpRunning) {
503 {
504#line 68
505 printf("On");
506 }
507 } else {
508 {
509#line 69
510 printf("Off");
511 }
512 }
513 {
514#line 71
515 printf(") ");
516#line 72
517 printEnvironment();
518#line 73
519 printf("\n");
520 }
521#line 315 "MinePump.c"
522 return;
523}
524}
525#line 75 "MinePump.c"
526int isHighWaterLevel(void)
527{ int retValue_acc ;
528 int tmp ;
529 int tmp___0 ;
530
531 {
532 {
533#line 333 "MinePump.c"
534 tmp = isHighWaterSensorDry();
535 }
536#line 333
537 if (tmp) {
538#line 333
539 tmp___0 = 0;
540 } else {
541#line 333
542 tmp___0 = 1;
543 }
544#line 333
545 retValue_acc = tmp___0;
546#line 335
547 return (retValue_acc);
548#line 342
549 return (retValue_acc);
550}
551}
552#line 78 "MinePump.c"
553int isLowWaterLevel(void)
554{ int retValue_acc ;
555 int tmp ;
556 int tmp___0 ;
557
558 {
559 {
560#line 364 "MinePump.c"
561 tmp = isLowWaterSensorDry();
562 }
563#line 364
564 if (tmp) {
565#line 364
566 tmp___0 = 0;
567 } else {
568#line 364
569 tmp___0 = 1;
570 }
571#line 364
572 retValue_acc = tmp___0;
573#line 366
574 return (retValue_acc);
575#line 373
576 return (retValue_acc);
577}
578}
579#line 81 "MinePump.c"
580void stopSystem(void)
581{
582
583 {
584#line 86
585 if (pumpRunning) {
586 {
587#line 83
588 deactivatePump();
589 }
590 } else {
591
592 }
593#line 86
594 systemActive = 0;
595#line 402 "MinePump.c"
596 return;
597}
598}
599#line 1 "Specification3_spec.o"
600#pragma merger(0,"Specification3_spec.i","")
601#line 4 "wsllib.h"
602void __automaton_fail(void) ;
603#line 11 "Specification3_spec.c"
604void __utac_acc__Specification3_spec__1(void)
605{ int tmp ;
606 int tmp___0 ;
607 int tmp___1 ;
608
609 {
610 {
611#line 19
612 tmp = isMethaneLevelCritical();
613 }
614#line 19
615 if (tmp) {
616
617 } else {
618 {
619#line 19
620 tmp___0 = getWaterLevel();
621 }
622#line 19
623 if (tmp___0 == 2) {
624 {
625#line 19
626 tmp___1 = isPumpRunning();
627 }
628#line 19
629 if (tmp___1) {
630
631 } else {
632 {
633#line 16
634 __automaton_fail();
635 }
636 }
637 } else {
638
639 }
640 }
641#line 16
642 return;
643}
644}
645#line 1 "Test.o"
646#pragma merger(0,"Test.i","")
647#line 8 "Test.c"
648int cleanupTimeShifts = 4;
649#line 11 "Test.c"
650#line 17 "Test.c"
651void cleanup(void)
652{ int i ;
653 int __cil_tmp2 ;
654
655 {
656 {
657#line 20
658 timeShift();
659#line 22
660 i = 0;
661 }
662 {
663#line 22
664 while (1) {
665 while_1_continue: ;
666 {
667#line 22
668 __cil_tmp2 = cleanupTimeShifts - 1;
669#line 22
670 if (i < __cil_tmp2) {
671
672 } else {
673 goto while_1_break;
674 }
675 }
676 {
677#line 23
678 timeShift();
679#line 22
680 i = i + 1;
681 }
682 }
683 while_1_break: ;
684 }
685#line 1111 "Test.c"
686 return;
687}
688}
689#line 56 "Test.c"
690void Specification2(void)
691{
692
693 {
694 {
695#line 57
696 timeShift();
697#line 57
698 printPump();
699#line 58
700 timeShift();
701#line 58
702 printPump();
703#line 59
704 timeShift();
705#line 59
706 printPump();
707#line 60
708 waterRise();
709#line 60
710 printPump();
711#line 61
712 timeShift();
713#line 61
714 printPump();
715#line 62
716 changeMethaneLevel();
717#line 62
718 printPump();
719#line 63
720 timeShift();
721#line 63
722 printPump();
723#line 64
724 cleanup();
725 }
726#line 1159 "Test.c"
727 return;
728}
729}
730#line 67 "Test.c"
731void setup(void)
732{
733
734 {
735#line 1177 "Test.c"
736 return;
737}
738}
739#line 74 "Test.c"
740void runTest(void)
741{
742
743 {
744 {
745#line 77
746 test();
747 }
748#line 1197 "Test.c"
749 return;
750}
751}
752#line 83 "Test.c"
753void select_helpers(void) ;
754#line 84
755void select_features(void) ;
756#line 85
757int valid_product(void) ;
758#line 82 "Test.c"
759int main(void)
760{ int retValue_acc ;
761 int tmp ;
762
763 {
764 {
765#line 83
766 select_helpers();
767#line 84
768 select_features();
769#line 85
770 tmp = valid_product();
771 }
772#line 85
773 if (tmp) {
774 {
775#line 86
776 setup();
777#line 87
778 runTest();
779 }
780 } else {
781
782 }
783#line 1226 "Test.c"
784 retValue_acc = 0;
785#line 1228
786 return (retValue_acc);
787#line 1235
788 return (retValue_acc);
789}
790}
791#line 1 "featureselect.o"
792#pragma merger(0,"featureselect.i","")
793#line 8 "featureselect.h"
794int select_one(void) ;
795#line 8 "featureselect.c"
796int select_one(void)
797{ int retValue_acc ;
798 int choice = __VERIFIER_nondet_int();
799
800 {
801#line 62 "featureselect.c"
802 retValue_acc = choice;
803#line 64
804 return (retValue_acc);
805#line 71
806 return (retValue_acc);
807}
808}
809#line 14 "featureselect.c"
810void select_features(void)
811{
812
813 {
814#line 93 "featureselect.c"
815 return;
816}
817}
818#line 20 "featureselect.c"
819void select_helpers(void)
820{
821
822 {
823#line 111 "featureselect.c"
824 return;
825}
826}
827#line 25 "featureselect.c"
828int valid_product(void)
829{ int retValue_acc ;
830
831 {
832#line 129 "featureselect.c"
833 retValue_acc = 1;
834#line 131
835 return (retValue_acc);
836#line 138
837 return (retValue_acc);
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}
1366#line 1 "wsllib_check.o"
1367#pragma merger(0,"wsllib_check.i","")
1368#line 3 "wsllib_check.c"
1369void __automaton_fail(void)
1370{
1371
1372 {
1373 goto ERROR;
1374 ERROR: ;
1375#line 53 "wsllib_check.c"
1376 return;
1377}
1378}