EDIT: The original question had unnecessary details
I have a source file which I do value analysis in Frama-C, some of the code is highlighted as dead code in the normalized window, no the original source code.
Can I obtain a slice of the original code that removes the dead code?
Short answer: there's nothing in the current Frama-C version that will let you do that directly. Moreover, if your original code contains macros, Frama-C will not even see the real original code, as it relies on an external preprocessor (e.g. cpp
) to do macro expansion.
Longer answer: Each statement in the normalized (aka CIL) Abstract Syntax Tree (AST, the internal representation of C code within Frama-C) contains information about the location (start point and end point) of the original statement where it stems from, and this information is also available in the original AST (aka Cabs). It might thus be possible for someone with a good knowledge of Frama-C's inner workings (e.g. a reader of the developer's manual), to build a correspondance between both, and to use that to detect dead statement in Cabs. Going even further, one could bypass Cabs, and identify zones in the original text of the program which are dead code. Note however that it would be a tedious and quite error prone (notably because a single original statement can be expanded in several normalized ones) task.