How to use functions in Value.Eval_expr, Value.Eval_op etc modules of Frama-c Value plugin

Question

I am trying to create a frama-c plugin. This plugin depends upon Frama-c Value plugin. I want to obtain and print value set of all the lvalue(s) in a C source code. In order to do that I want to use functions available in Value.Eval_exprs, Value.Eval_op etc. like Eval_exprs.lval_to_precise_loc.

Unfortunately I am unable to figure out a way to use these function in my plugin. I tried to follow steps mentioned in section 4.10.1 (Registration through a .mli file) of Frama-c Plugin Development Guide and added PLUGIN_DEPENDENCIES:=Value in my Makefile but I noticed that Value.mli file is empty and no function is exposed through this file. After that I looked at db.ml file in kernel directory and couldn't find any module that can be used to access all the functions available in Eval_exprs, Eval_op etc.

Is there any way to access these functions of Value plugin from other plugin?

Answer 1

Multiple mechanisms are available to use the results of a Frama-C plugin programatically:

1. through the Db module, that contains functions to access the results of many "core" plugins
2. through calls to the "dynamic" API (module Dynamic)
3. through the interface of the plugin (e.g. Value.mli in your case)

The first two approaches are deprecated, and will eventually disappear. Furthermore, approach 1. is not available for user-written plugins. This is why the developer manual emphasizes approach 3.

That being said, currently, the results of Value are available using approach 1 (only). Inside your plugin, you can simply write !Db.Value.eval_expr or !Db.Value.eval_lval to evalate an expression and a left-value respectively. This will work automatically. You should still declare Value as a dependency of your plugin (PLUGIN_DEPENDENCIES:=Value as you found out), as this will be required in the next version of Frama-C. All the internal modules of Value, such as Eval_exprs, are not exported, intentionally. Most uses of Value's results can be written using the functions available in Db.Value.

Finally, lval_to_precise_loc is a pretty advanced function, as the returned locations have a type that is hard to use. Db.Value.lval_to_loc is nearly always a better choice.