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?
Multiple mechanisms are available to use the results of a Frama-C plugin programatically:
- through the
Db
module, that contains functions to access the results of many "core" plugins
- through calls to the "dynamic" API (module
Dynamic
)
- 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.