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