Showing error 1944

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/minepump_spec2_product39_safe.cil.c
Line in file: 413
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 383#line 24
 384      if (methAndRunningLastTime) {
 385        {
 386#line 21
 387        __automaton_fail();
 388        }
 389      } else {
 390#line 23
 391        methAndRunningLastTime = 1;
 392      }
 393    } else {
 394#line 26
 395      methAndRunningLastTime = 0;
 396    }
 397  } else {
 398#line 26
 399    methAndRunningLastTime = 0;
 400  }
 401#line 26
 402  return;
 403}
 404}
 405#line 1 "wsllib_check.o"
 406#pragma merger(0,"wsllib_check.i","")
 407#line 3 "wsllib_check.c"
 408void __automaton_fail(void) 
 409{ 
 410
 411  {
 412  goto ERROR;
 413  ERROR: ;
 414#line 53 "wsllib_check.c"
 415  return;
 416}
 417}
 418#line 1 "scenario.o"
 419#pragma merger(0,"scenario.i","")
 420#line 12 "scenario.c"
 421void stopSystem(void) ;
 422#line 1 "scenario.c"
 423void test(void)
Show full sources
↑