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