--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Could I get the statement that caused the dead code programatically?



Dear all,

I want to programatically get the statement(Cil_types.stmt)  or the
expression (Cil_types.expr) or the left value (Cil_types.lval) that
caused other statement to be dead code in value analysis.

For example, if a function has the following three kinds of
statements, those statements after these three statements are detected
to be dead code from value analysis result.
1. y = a[8] + 6; /* assume the memory access is out of bounds */
2. if(0) {..}
3. x = k + 5; /* k is not initialized. */

How can I programatically get these statements by using the Db.Value.
state information or the Cvalue.V.t information or the Locations
information?

The API document lacks detail description for the abstract
interpretation related API functions. Could it possible to add some
description for these functions in later frama-c release?

Thank you very much.

-david