Showing error 2034

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


Source:

1371#line 85
1372  tmp = valid_product();
1373  }
1374#line 85
1375  if (tmp) {
1376    {
1377#line 86
1378    setup();
1379#line 87
1380    runTest();
1381    }
1382  } else {
1383
1384  }
1385#line 1226 "Test.c"
1386  retValue_acc = 0;
1387#line 1228
1388  return (retValue_acc);
1389#line 1235
1390  return (retValue_acc);
1391}
1392}
1393#line 1 "wsllib_check.o"
1394#pragma merger(0,"wsllib_check.i","")
1395#line 3 "wsllib_check.c"
1396void __automaton_fail(void) 
1397{ 
1398
1399  {
1400  goto ERROR;
1401  ERROR: ;
1402#line 53 "wsllib_check.c"
1403  return;
1404}
1405}
1406#line 1 "Specification3_spec.o"
1407#pragma merger(0,"Specification3_spec.i","")
1408#line 11 "Specification3_spec.c"
1409void __utac_acc__Specification3_spec__1(void) 
1410{ int tmp ;
1411  int tmp___0 ;
Show full sources