Showing error 1992

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

Source: 

 160  {
 161#line 209 "Environment.c"
 162  retValue_acc = waterLevel;
 163#line 211
 164  return (retValue_acc);
 165#line 218
 166  return (retValue_acc);
 167}
 168}
 169#line 58 "Environment.c"
 170int isLowWaterSensorDry(void) 
 171{ int retValue_acc ;
 172
 173  {
 174#line 240 "Environment.c"
 175  retValue_acc = waterLevel == 0;
 176#line 242
 177  return (retValue_acc);
 178#line 249
 179  return (retValue_acc);
 180}
 181}
 182#line 1 "wsllib_check.o"
 183#pragma merger(0,"wsllib_check.i","")
 184#line 3 "wsllib_check.c"
 185void __automaton_fail(void) 
 186{ 
 187
 188  {
 189  goto ERROR;
 190  ERROR: ;
 191#line 53 "wsllib_check.c"
 192  return;
 193}
 194}
 195#line 1 "Test.o"
 196#pragma merger(0,"Test.i","")
 197#line 8 "Test.c"
 198int cleanupTimeShifts  =    4;
 199#line 11 "Test.c"
 200#line 20 "Test.c"
Show full sources
↑