Showing error 2160

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

Source: 

1267#line 20 "featureselect.c"
1268void select_helpers(void) 
1269{ 
1270
1271  {
1272#line 111 "featureselect.c"
1273  return;
1274}
1275}
1276#line 25 "featureselect.c"
1277int valid_product(void) 
1278{ int retValue_acc ;
1279
1280  {
1281#line 129 "featureselect.c"
1282  retValue_acc = 1;
1283#line 131
1284  return (retValue_acc);
1285#line 138
1286  return (retValue_acc);
1287}
1288}
1289#line 1 "wsllib_check.o"
1290#pragma merger(0,"wsllib_check.i","")
1291#line 3 "wsllib_check.c"
1292void __automaton_fail(void) 
1293{ 
1294
1295  {
1296  goto ERROR;
1297  ERROR: ;
1298#line 53 "wsllib_check.c"
1299  return;
1300}
1301}
1302#line 1 "Environment.o"
1303#pragma merger(0,"Environment.i","")
1304#line 9 "Environment.c"
1305int waterLevel  =    1;
1306#line 12 "Environment.c"
1307int methaneLevelCritical  =    0;
Show full sources
↑