Showing error 1897

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

Source: 

1331#line 253 "Environment.c"
1332    retValue_acc = 0;
1333#line 255
1334    return (retValue_acc);
1335  }
1336#line 262 "Environment.c"
1337  return (retValue_acc);
1338}
1339}
1340#line 67 "Environment.c"
1341int isLowWaterSensorDry(void) 
1342{ int retValue_acc ;
1343
1344  {
1345#line 284 "Environment.c"
1346  retValue_acc = waterLevel == 0;
1347#line 286
1348  return (retValue_acc);
1349#line 293
1350  return (retValue_acc);
1351}
1352}
1353#line 1 "wsllib_check.o"
1354#pragma merger(0,"wsllib_check.i","")
1355#line 3 "wsllib_check.c"
1356void __automaton_fail(void) 
1357{ 
1358
1359  {
1360  goto ERROR;
1361  ERROR: ;
1362#line 53 "wsllib_check.c"
1363  return;
1364}
1365}
Show full sources
↑