--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on January 2014 ---
[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



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;
}