Showing error 2087

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


Source:

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