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