Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] Could I get the statement that caused the dead code programatically?
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Sun, 5 Jan 2014 01:25:10 +0800
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