I am working on a Plugin for Frama-C, using the Value-analysis. I simply want to print the state of the variables (values) after each statement (I think the solution is quiet easy, but I couldn't figure it out).
I got the current state with Db.Value.get_stmt_state
in the vstmt_aux
method in the visitor.
How can I now get the values of the variables?
PS: I found this post, but it didn't help, there is no real solution, and with the help of the description I was not able to do it: How to use functions in Value.Eval_expr, Value.Eval_op etc modules of Frama-c Value plugin
Here's a concrete example of how to print, for each local and global variable, the result computed by Value before each statement in a given function (read the functions from bottom to top):
This is far from ideal, and the output is uglier than simply using
Cvalue.Model.pretty state
, but it could serve as base for further modifications.This script has been tested with Frama-C Magnesium.
To retrieve the state after a statement, simply replace the
~after:false
parameter infold_state_callstack
with~after:true
. My previous version of the code used a function which already bound that value for the pre-state, but no such function is exported for the post-state, so we must usefold_state_callstack
(which is incidentally more powerful, because it allows retrieving a specific state per callstack).