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