Showing error 1840

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


Source:

1403#line 269 "Environment.c"
1404    retValue_acc = 0;
1405#line 271
1406    return (retValue_acc);
1407  }
1408#line 278 "Environment.c"
1409  return (retValue_acc);
1410}
1411}
1412#line 67 "Environment.c"
1413int isLowWaterSensorDry(void) 
1414{ int retValue_acc ;
1415
1416  {
1417#line 300 "Environment.c"
1418  retValue_acc = waterLevel == 0;
1419#line 302
1420  return (retValue_acc);
1421#line 309
1422  return (retValue_acc);
1423}
1424}
1425#line 1 "wsllib_check.o"
1426#pragma merger(0,"wsllib_check.i","")
1427#line 3 "wsllib_check.c"
1428void __automaton_fail(void) 
1429{ 
1430
1431  {
1432  goto ERROR;
1433  ERROR: ;
1434#line 53 "wsllib_check.c"
1435  return;
1436}
1437}
1438#line 1 "Test.o"
1439#pragma merger(0,"Test.i","")
1440#line 8 "Test.c"
1441int cleanupTimeShifts  =    4;
1442#line 11 "Test.c"
1443#line 17 "Test.c"
Show full sources