ocaml - 如何使用 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 插件的结果:

通过Db模块，包含访问许多“核心”插件结果的函数

通过调用“动态”API(模块 Dynamic)

通过插件的界面(例如 Value.mli 在你的情况下)

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

话虽如此，目前，Value 的结果可使用方法 1(仅)获得。在你的插件里面，你可以简单地写 !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几乎总是一个更好的选择。