Showing error 1651

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: product-lines/elevator_spec9_productSimulator_unsafe.cil.c
Line in file: 2509
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

2479          {
2480#line 69
2481          __automaton_fail();
2482          }
2483        } else {
2484#line 70
2485          if (floorButtons_spc9_4) {
2486            {
2487#line 71
2488            __automaton_fail();
2489            }
2490          } else {
2491
2492          }
2493        }
2494      }
2495    }
2496  }
2497#line 71
2498  return;
2499}
2500}
2501#line 1 "wsllib_check.o"
2502#pragma merger(0,"wsllib_check.i","")
2503#line 3 "wsllib_check.c"
2504void __automaton_fail(void) 
2505{ 
2506
2507  {
2508  goto ERROR;
2509  ERROR: ;
2510#line 53 "wsllib_check.c"
2511  return;
2512}
2513}
2514#line 1 "scenario.o"
2515#pragma merger(0,"scenario.i","")
2516#line 3 "scenario.c"
2517void test(void) 
2518{ 
2519
Show full sources
↑