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] How to modify the value state of a statement for re-running the value analysis

  • Subject: [Frama-c-discuss] How to modify the value state of a statement for re-running the value analysis
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Thu, 2 Jan 2014 23:31:31 +0800
Dear all,

Could it possible to modify the state of specified statement then
re-run the value analysis at some program point?

For example, for the given main function, it has an array parameter:int *A.
The default value analysis context-width is 2 in default. By default,
the statement after statement 3 are dead codes.

Actually I am sure the statement 3 is valid and the memory access is
not out of bound.
I want to change the state of the statement 3 by initializing the
{&S_A + {8}‌} and then re-run the value analysis.

How can I achieve this?

Currently I can get the value state of the corresponding statement. By
using : let state = Db.Value.get_state (Cil_types.Kstmt(stmt)) in

There are too many modules for abstract interpretation. (Locations,
Cvalue, Base, et.al). These modules makes me confused. Any
suggestions?

Thank you very much.

/* example */
int main(int *A, int n){
   /* other stmts */
   int res = A[8] + 6; /* stmt 3 */
   /* other stmts */

   return res;
}