我正在尝试创建一个 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 模块，该模块包含访问许多“核心”插件结果的函数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 几乎总是更好的选择。
【讨论】：
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;
stmt 的状态之后获得执行语句后的 lval 值集。我想如果我能得到after_state，我可以得到设置为：let _, after = !Db.Value.eval_lval ~with_alarms (Some Locations.Zone.bottom) after_state lv的值。您能否建议一种获取 after_state 的方法？
fold_stmt_state_callstack 在每个分析调用堆栈的语句上迭代结果。如果你不需要调用栈，你可以简单地加入所有可能的状态：let state_after stmt = Db.Value.fold_stmt_state_callstack Cvalue.Model.join Cvalue.Model.bottom ~after:true stmt
db.ml 中找不到函数fold_stmt_state_callstack。我正在使用钠版本。我在这里错过了什么吗？
Db.Value.AfterTable_By_Callstack.find s 获取语句s 上所有调用堆栈的信息。