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