Showing error 2149

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


Source:

 558#line 253 "Environment.c"
 559    retValue_acc = 0;
 560#line 255
 561    return (retValue_acc);
 562  }
 563#line 262 "Environment.c"
 564  return (retValue_acc);
 565}
 566}
 567#line 67 "Environment.c"
 568int isLowWaterSensorDry(void) 
 569{ int retValue_acc ;
 570
 571  {
 572#line 284 "Environment.c"
 573  retValue_acc = waterLevel == 0;
 574#line 286
 575  return (retValue_acc);
 576#line 293
 577  return (retValue_acc);
 578}
 579}
 580#line 1 "wsllib_check.o"
 581#pragma merger(0,"wsllib_check.i","")
 582#line 3 "wsllib_check.c"
 583void __automaton_fail(void) 
 584{ 
 585
 586  {
 587  goto ERROR;
 588  ERROR: ;
 589#line 53 "wsllib_check.c"
 590  return;
 591}
 592}
 593#line 1 "Test.o"
 594#pragma merger(0,"Test.i","")
 595#line 8 "Test.c"
 596int cleanupTimeShifts  =    4;
 597#line 11 "Test.c"
 598#line 17 "Test.c"
Show full sources