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.
|ID0000709||Frama-C||Plug-in > slicing||public||2011-02-08||2014-02-12|
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||Frama-C Nitrogen-20111001|
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.