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