Showing error 1892

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

Source: 

 501    deactivatePump();
 502    }
 503  } else {
 504
 505  }
 506#line 86
 507  systemActive = 0;
 508#line 404 "MinePump.c"
 509  return;
 510}
 511}
 512#line 88 "MinePump.c"
 513void startSystem(void) 
 514{ 
 515
 516  {
 517#line 90
 518  systemActive = 1;
 519#line 424 "MinePump.c"
 520  return;
 521}
 522}
 523#line 1 "wsllib_check.o"
 524#pragma merger(0,"wsllib_check.i","")
 525#line 3 "wsllib_check.c"
 526void __automaton_fail(void) 
 527{ 
 528
 529  {
 530  goto ERROR;
 531  ERROR: ;
 532#line 53 "wsllib_check.c"
 533  return;
 534}
 535}
 536#line 1 "scenario.o"
 537#pragma merger(0,"scenario.i","")
 538#line 7 "scenario.c"
 539#line 17
 540void cleanup(void) ;
 541#line 1 "scenario.c"
Show full sources
↑