如何在Frama-c Value插件的Value.Eval_expr,Value.Eval_op等模块中使用函数

Question

我正在尝试创建一个frama-c插件.这个插件取决于Frama-c Value插件.我想获取并打印C源代码中所有左值的值集.为了做到这一点,我想使用Value.Eval_exprs,Value.Eval_op等中可用的函数Eval_exprs.lval_to_precise_loc.

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

有没有办法从其他插件访问Value插件的这些功能？

Answer 1

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

1. 通过该Db模块，该模块包含访问许多“核心”插件结果的函数
2. 通过调用“动态”API（模块Dynamic）
3. 通过插件的界面（例如Value.mli在您的情况下）

前两种方法已被弃用，并且最终将消失。此外，方法 1. 不适用于用户编写的插件。这就是开发者手册强调方法 3 的原因。

话虽如此，目前（仅）可以使用方法 1 获得 Value 的结果。在您的插件中，您可以简单地编写!Db.Value.eval_expr或!Db.Value.eval_lval分别计算表达式和左值。这将自动工作。您仍然应该将 Value 声明为插件的依赖项（PLUGIN_DEPENDENCIES:=Value正如您所发现的），因为 Frama-C 的下一个版本将需要这样做。Value 的所有内部模块（例如Eval_exprs）都不会被有意导出。Value 结果的大多数用途都可以使用 中提供的函数来编写Db.Value。

最后，lval_to_precise_loc这是一个非常高级的函数，因为返回的位置具有难以使用的类型。Db.Value.lval_to_loc几乎总是更好的选择。