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