Showing error 2112

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

Source: 

 524#line 13
 525        stopSystem();
 526        }
 527      } else {
 528
 529      }
 530    }
 531    {
 532#line 15
 533    timeShift();
 534    }
 535  }
 536  while_0_break: /* CIL Label */ ;
 537  }
 538  {
 539#line 17
 540  cleanup();
 541  }
 542#line 78 "scenario.c"
 543  return;
 544}
 545}
 546#line 1 "wsllib_check.o"
 547#pragma merger(0,"wsllib_check.i","")
 548#line 3 "wsllib_check.c"
 549void __automaton_fail(void) 
 550{ 
 551
 552  {
 553  goto ERROR;
 554  ERROR: ;
 555#line 53 "wsllib_check.c"
 556  return;
 557}
 558}
 559#line 1 "Test.o"
 560#pragma merger(0,"Test.i","")
 561#line 8 "Test.c"
 562int cleanupTimeShifts  =    4;
 563#line 11 "Test.c"
 564#line 17 "Test.c"
Show full sources
↑