Showing error 2161

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


Source:

1263#line 20 "featureselect.c"
1264void select_helpers(void) 
1265{ 
1266
1267  {
1268#line 111 "featureselect.c"
1269  return;
1270}
1271}
1272#line 25 "featureselect.c"
1273int valid_product(void) 
1274{ int retValue_acc ;
1275
1276  {
1277#line 129 "featureselect.c"
1278  retValue_acc = 1;
1279#line 131
1280  return (retValue_acc);
1281#line 138
1282  return (retValue_acc);
1283}
1284}
1285#line 1 "wsllib_check.o"
1286#pragma merger(0,"wsllib_check.i","")
1287#line 3 "wsllib_check.c"
1288void __automaton_fail(void) 
1289{ 
1290
1291  {
1292  goto ERROR;
1293  ERROR: ;
1294#line 53 "wsllib_check.c"
1295  return;
1296}
1297}
1298#line 1 "Test.o"
1299#pragma merger(0,"Test.i","")
1300#line 8 "Test.c"
1301int cleanupTimeShifts  =    4;
1302#line 11 "Test.c"
1303#line 17 "Test.c"
Show full sources