Showing error 1889

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

Source: 

1306#line 253 "Environment.c"
1307    retValue_acc = 0;
1308#line 255
1309    return (retValue_acc);
1310  }
1311#line 262 "Environment.c"
1312  return (retValue_acc);
1313}
1314}
1315#line 67 "Environment.c"
1316int isLowWaterSensorDry(void) 
1317{ int retValue_acc ;
1318
1319  {
1320#line 284 "Environment.c"
1321  retValue_acc = waterLevel == 0;
1322#line 286
1323  return (retValue_acc);
1324#line 293
1325  return (retValue_acc);
1326}
1327}
1328#line 1 "wsllib_check.o"
1329#pragma merger(0,"wsllib_check.i","")
1330#line 3 "wsllib_check.c"
1331void __automaton_fail(void) 
1332{ 
1333
1334  {
1335  goto ERROR;
1336  ERROR: ;
1337#line 53 "wsllib_check.c"
1338  return;
1339}
1340}
Show full sources
↑