如何使用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。
不幸的是，我无法找到在我的插件中使用这些功能的方法。我尝试按照 Frama-c 插件开发指南第 4.10.1 节（通过 .mli 文件注册）中提到的步骤进行操作，并在我的 Makefile 中添加了 PLUGIN_DEPENDENCIES:=Value，但我注意到 Value.mli 文件是空的，没有函数通过这个文件公开。之后，我查看了 kernel 目录中的 db.ml 文件，但找不到任何可用于访问 Eval_exprs、Eval_op 等中可用功能的模块。
有没有办法从其他插件访问Value插件的这些功能？
有多种机制可用于以编程方式使用 Frama-C 插件的结果：
- 通过
Db 模块，该模块包含访问许多 "core" 插件结果的函数
- 通过调用 "dynamic" API（模块
Dynamic）
- 通过插件的界面（例如
Value.mli 在你的情况下）
前两种方法已弃用，最终会消失。此外，方法 1. 不适用于 user-written 插件。这就是开发人员手册强调方法 3 的原因。
也就是说，目前，Value 的结果可使用方法 1（仅）获得。在您的插件中，您可以简单地编写 !Db.Value.eval_expr 或 !Db.Value.eval_lval 来分别计算表达式和 left-value。这将自动工作。您仍然应该将 Value 声明为插件的依赖项（如您所见，PLUGIN_DEPENDENCIES:=Value），因为这将在下一版本的 Frama-C 中被要求。 Value 的所有 internal 模块，例如 Eval_exprs，都是 not 有意导出的。 Value 结果的大部分用途都可以使用 Db.Value.
中可用的函数来编写
最后，lval_to_precise_loc 是一个非常高级的函数，因为返回的位置具有难以使用的类型。 Db.Value.lval_to_loc 几乎总是更好的选择。
我正在尝试创建一个 frama-c 插件。这个插件依赖于 Frama-c Value 插件。我想获取并打印 C 源代码中所有左值的值集。为此，我想使用 Value.Eval_exprs、Value.Eval_op 等中可用的函数，例如 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 等中可用功能的模块。
有没有办法从其他插件访问Value插件的这些功能？
有多种机制可用于以编程方式使用 Frama-C 插件的结果：
- 通过
Db模块，该模块包含访问许多 "core" 插件结果的函数 - 通过调用 "dynamic" API（模块
Dynamic） - 通过插件的界面（例如
Value.mli在你的情况下）
前两种方法已弃用，最终会消失。此外，方法 1. 不适用于 user-written 插件。这就是开发人员手册强调方法 3 的原因。
也就是说，目前，Value 的结果可使用方法 1（仅）获得。在您的插件中，您可以简单地编写 !Db.Value.eval_expr 或 !Db.Value.eval_lval 来分别计算表达式和 left-value。这将自动工作。您仍然应该将 Value 声明为插件的依赖项（如您所见，PLUGIN_DEPENDENCIES:=Value），因为这将在下一版本的 Frama-C 中被要求。 Value 的所有 internal 模块，例如 Eval_exprs，都是 not 有意导出的。 Value 结果的大部分用途都可以使用 Db.Value.
最后，lval_to_precise_loc 是一个非常高级的函数，因为返回的位置具有难以使用的类型。 Db.Value.lval_to_loc 几乎总是更好的选择。