Showing error 2109

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

Source: 

 420#line 12
 421      if (tmp___1) {
 422
 423      } else {
 424
 425      }
 426    }
 427    {
 428#line 13
 429    timeShift();
 430    }
 431  }
 432  while_0_break: /* CIL Label */ ;
 433  }
 434  {
 435#line 15
 436  cleanup();
 437  }
 438#line 74 "scenario.c"
 439  return;
 440}
 441}
 442#line 1 "wsllib_check.o"
 443#pragma merger(0,"wsllib_check.i","")
 444#line 3 "wsllib_check.c"
 445void __automaton_fail(void) 
 446{ 
 447
 448  {
 449  goto ERROR;
 450  ERROR: ;
 451#line 53 "wsllib_check.c"
 452  return;
 453}
 454}
 455#line 1 "Test.o"
 456#pragma merger(0,"Test.i","")
 457#line 8 "Test.c"
 458int cleanupTimeShifts  =    4;
 459#line 11 "Test.c"
 460#line 17 "Test.c"
Show full sources
↑