How to use functions in Value.Eval_expr, Value.Eval_op, etc. Value Frama-c Plugin Modules

Question

I am trying to create a frama-c plugin. This plugin is dependent on the Value Frama-c plugin. I want to get and print the set of values ​​of all lvalue (s) in the source code of C. For this, I want to use the functions available in Value.Eval_exprs, Value.Eval_op, etc. For example, Eval_exprs.lval_to_precise_loc .

Unfortunately, I cannot figure out how to use this function in my plugin. I tried to follow the steps mentioned in section 4.10.1 (Registering via the .mli File) of the Frama-c Plugin Development Guide and added PLUGIN_DEPENDENCIES:=Value to my Makefile, but I noticed that the Value.mli file Value.mli empty and no function is not displayed through this file. After that, I looked at the db.ml file in the kernel directory and could not find any module that can be used to access all the functions available in Eval_exprs, Eval_op, etc.

Is there a way to access these functions of the Value plugin from another plugin?

Answer 1

Several mechanisms are available for using the results of the Frama-C plugin programmatically:

• through the Db module, which contains functions for accessing the results of many "basic" plugins
• through calls to the "dynamic" API ( Dynamic module)
• via the plugin interface (e.g. Value.mli in your case)

The first two approaches are outdated and will eventually disappear. In addition, approach 1. is not available for custom plugins. This is why the development guide emphasizes approach 3.

However, Value results are currently available using Approach 1 (only). Inside your plugin, you can simply write !Db.Value.eval_expr or !Db.Value.eval_lval to evaluate the expression and the left value, respectively. This will work automatically. You must declare the value as a dependency of your plugin ( PLUGIN_DEPENDENCIES:=Value , as you learned), as this will be required in the next version of Frama-C. All internal Value modules, such as Eval_exprs , are not intentionally exported. Most applications of Value results can be written using the functions available in Db.Value .

Finally, lval_to_precise_loc is a pretty advanced feature, since the returned locations are of a type that is difficult to use. Db.Value.lval_to_loc is almost always the best choice.