如何在Frama-c Value插件的Value.Eval_expr，Value.Eval_op等模块中使用函数 [英] How to use functions in Value.Eval_expr, Value.Eval_op etc modules of Frama-c Value plugin

问题描述

我正在尝试创建frama-c插件.该插件取决于Frama-c Value插件.我想在C源代码中获取并打印所有左值的值集.为此，我想使用Value.Eval_exprs，Value.Eval_op等可用的函数，例如Eval_exprs.lval_to_precise_loc.

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.

不幸的是，我无法找到一种在插件中使用这些功能的方法.我尝试遵循Frama-c插件开发指南的4.10.1节(通过.mli文件注册)中提到的步骤，并在我的Makefile文件中添加了PLUGIN_DEPENDENCIES:=Value，但是我注意到Value.mli文件为空，并且没有任何函数通过这个文件.之后，我查看了kernel目录中的db.ml文件，找不到任何可用于访问Eval_exprs，Eval_op等可用功能的模块.

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.

是否可以从其他插件访问Value插件的这些功能?

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

推荐答案

可以使用多种机制以编程方式使用Frama-C插件的结果:

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

1. 通过Db模块，该模块包含用于访问许多核心"插件结果的功能
2. 通过调用动态" API(模块Dynamic)
3. 通过插件的界面(例如您的情况下为Value.mli)

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)

不建议使用前两种方法，最终将消失.此外，方法1.不适用于用户编写的插件.这就是开发人员手册强调方法3的原因.

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.

话虽如此，目前，使用方法1(仅)可获得Value的结果.在您的插件内部，您只需编写!Db.Value.eval_expr或!Db.Value.eval_lval即可分别逃避表达式和左值.这将自动运行.您仍然应该将Value声明为插件的依赖项(您发现的PLUGIN_DEPENDENCIES:=Value)，因为在下一版本的Frama-C中将需要此值. Value的所有内部模块，例如Eval_exprs，是有意不导出的. Value结果的大多数用法都可以使用Db.Value中可用的功能编写.

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.

最后，lval_to_precise_loc是一个相当高级的功能，因为返回的位置具有难以使用的类型. Db.Value.lval_to_loc几乎总是一个更好的选择.

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.

这篇关于如何在Frama-c Value插件的Value.Eval_expr，Value.Eval_op等模块中使用函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！