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