Showing error 2089

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

Source: 

1311#line 253 "Environment.c"
1312    retValue_acc = 0;
1313#line 255
1314    return (retValue_acc);
1315  }
1316#line 262 "Environment.c"
1317  return (retValue_acc);
1318}
1319}
1320#line 67 "Environment.c"
1321int isLowWaterSensorDry(void) 
1322{ int retValue_acc ;
1323
1324  {
1325#line 284 "Environment.c"
1326  retValue_acc = waterLevel == 0;
1327#line 286
1328  return (retValue_acc);
1329#line 293
1330  return (retValue_acc);
1331}
1332}
1333#line 1 "wsllib_check.o"
1334#pragma merger(0,"wsllib_check.i","")
1335#line 3 "wsllib_check.c"
1336void __automaton_fail(void) 
1337{ 
1338
1339  {
1340  goto ERROR;
1341  ERROR: ;
1342#line 53 "wsllib_check.c"
1343  return;
1344}
1345}
1346#line 1 "featureselect.o"
1347#pragma merger(0,"featureselect.i","")
1348#line 8 "featureselect.h"
1349int select_one(void) ;
1350#line 8 "featureselect.c"
1351int select_one(void)
Show full sources
↑