5

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?

Gunjan Aggarwal
  • 710
  • 5
  • 19

1 Answers1

3

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.

byako
  • 3,372
  • 2
  • 21
  • 36
  • Thanks for the detailed explanation. I was able to obtain and print value set of lvalue(s) as following: `let before = !Db.Value.access (Kstmt stmt) lv in Format.fprintf out "value of lval : %a is: %a" Printer.pp_lval lv Db.Value.pretty before;` – Gunjan Aggarwal Dec 31 '15 at 19:26
  • I am finding it hard to obtain after state of the `stmt` to obtain values set of lval after statement is executed. I think if I can get `after_state`, I can obtain after value set as: `let _, after = !Db.Value.eval_lval ~with_alarms (Some Locations.Zone.bottom) after_state lv`. Can you please suggest a way to get after_state? – Gunjan Aggarwal Dec 31 '15 at 19:36
  • You can use `fold_stmt_state_callstack` to iterate over the results on a statement per analysis callstack. If you do not need the callstack, you can simply join all the possible states: `let state_after stmt = Db.Value.fold_stmt_state_callstack Cvalue.Model.join Cvalue.Model.bottom ~after:true stmt` – byako Jan 01 '16 at 21:04
  • @ byako, Thanks for the response, but I can't find function `fold_stmt_state_callstack` in `db.ml`. I am working with Sodium version. Am I missing something here? – Gunjan Aggarwal Jan 01 '16 at 21:30
  • You're right, this function was added in Magnesium, and this version has not been released yet. You can get the information for all callstacks on statement `s` using `Db.Value.AfterTable_By_Callstack.find s`. – byako Jan 03 '16 at 18:12