Showing error 2151

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

Source: 

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