Showing error 2059

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


Source:

1299#line 20 "featureselect.c"
1300void select_helpers(void) 
1301{ 
1302
1303  {
1304#line 111 "featureselect.c"
1305  return;
1306}
1307}
1308#line 25 "featureselect.c"
1309int valid_product(void) 
1310{ int retValue_acc ;
1311
1312  {
1313#line 129 "featureselect.c"
1314  retValue_acc = 1;
1315#line 131
1316  return (retValue_acc);
1317#line 138
1318  return (retValue_acc);
1319}
1320}
1321#line 1 "wsllib_check.o"
1322#pragma merger(0,"wsllib_check.i","")
1323#line 3 "wsllib_check.c"
1324void __automaton_fail(void) 
1325{ 
1326
1327  {
1328  goto ERROR;
1329  ERROR: ;
1330#line 53 "wsllib_check.c"
1331  return;
1332}
1333}
Show full sources