Showing error 2143

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


Source:

1321#line 20 "featureselect.c"
1322void select_helpers(void) 
1323{ 
1324
1325  {
1326#line 111 "featureselect.c"
1327  return;
1328}
1329}
1330#line 25 "featureselect.c"
1331int valid_product(void) 
1332{ int retValue_acc ;
1333
1334  {
1335#line 129 "featureselect.c"
1336  retValue_acc = 1;
1337#line 131
1338  return (retValue_acc);
1339#line 138
1340  return (retValue_acc);
1341}
1342}
1343#line 1 "wsllib_check.o"
1344#pragma merger(0,"wsllib_check.i","")
1345#line 3 "wsllib_check.c"
1346void __automaton_fail(void) 
1347{ 
1348
1349  {
1350  goto ERROR;
1351  ERROR: ;
1352#line 53 "wsllib_check.c"
1353  return;
1354}
1355}
Show full sources