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 it possible to change the if statement state then re-do value analysis programmatically?

  • Subject: [Frama-c-discuss] Could it possible to change the if statement state then re-do value analysis programmatically?
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
  • Date: Fri, 3 Jan 2014 20:40:14 +0800
Dear all,

For a given if statement,  we can get the evaluated condition value by using :

(* the api is:  Db.Value.condition_truth_value : Cil_types.stmt ->
bool * bool *)
let (flag1, flag2) = Db.Value.condition_truth_value stmt in

For my source code, flag1 is false  but i can make sure the condition
can be true, Could it possible to set the flag1 and flag2 to be true
then re-do the value analysis?

How can I customize these values for value analysis programmatically?
Or could it possible to change the abstract interpretation and the
state of the statement (e.g. the if condition) programmatically?

Thank you very much.

-david