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