Db.Value.AfterTable.find Frama-C 铝的 api 更改答案

【问题标题】：Db.Value.AfterTable.find api change for Frama-C AluminiumDb.Value.AfterTable.find Frama-C 铝的 api 更改
【发布时间】：2016-09-07 14:56:45
【问题描述】：

我正在尝试将 Frama-C Fluorine 版本的插件迁移到 Frama-C Aluminium。这样做时，我找不到函数Db.Value.AfterTable.find 的合适替代品，我找到的最接近的是Db.Value.AfterTable_By_Callstack.find。但是，该函数现在返回不同的类型，即 Db.Value.AfterTable_By_Callstack.data = Db.Value.state Value_types.Callstack.Hashtbl.t，而不是 Frama-C Fluorine 中的 Db.Value.state。有人可以帮我解决这个问题吗？

非常感谢，特鲁克

【问题讨论】：

标签： frama-c

【解决方案1】：

确实，现在信息更加准确。但是您可以通过调用堆栈加入状态来计算状态：

let state = Value_callstack.Callstack.Hashtbl.fold
      (fun _cs state acc -> Cvalue.Model.join acc state)
      csh Cvalue.Model.bottom

【讨论】：

csh 是 Db.Value.AfterTable_By_Callstack.find stmt。