Bug in slicing -- required C-statements getting knocked off from sliced code
ID0000709: This issue was created automatically from Mantis Issue 709. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000709 | Frama-C | Plug-in > slicing | public | 2011-02-08 | 2014-02-12 |
| Reporter | tukarammuske | Assigned To | Anne | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
The frama-c is used for slicing of the attached testcase. The required C-statements, nondets of var1 and var2 (line 54 & 55, function inputsOf_testcase_func) are getting removed from sliced code. Actually they should not. Looks like theres bug in the frama-c slicing.
Also, it is observed that if any one of the block of code ( three blocks are mentioned in the testcase with comment Block-1,2 or 3) is deleted, the required nondets of var1 and var2 are seen in the sliced code (that is slicing is done correctly!!!)
Additional Information :
The command used to run frama-c is --
frama-c -slice-print -no-unicode -slice-pragma func testcase.c
The required details like problem, the blocks affecting the slicing, the knocked off c statements are described with comments in the attached test case.
