Showing error 1869

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

Source: 

1281  {
1282#line 209 "Environment.c"
1283  retValue_acc = waterLevel;
1284#line 211
1285  return (retValue_acc);
1286#line 218
1287  return (retValue_acc);
1288}
1289}
1290#line 58 "Environment.c"
1291int isLowWaterSensorDry(void) 
1292{ int retValue_acc ;
1293
1294  {
1295#line 240 "Environment.c"
1296  retValue_acc = waterLevel == 0;
1297#line 242
1298  return (retValue_acc);
1299#line 249
1300  return (retValue_acc);
1301}
1302}
1303#line 1 "wsllib_check.o"
1304#pragma merger(0,"wsllib_check.i","")
1305#line 3 "wsllib_check.c"
1306void __automaton_fail(void) 
1307{ 
1308
1309  {
1310  goto ERROR;
1311  ERROR: ;
1312#line 53 "wsllib_check.c"
1313  return;
1314}
1315}
Show full sources
↑