frama-c - Frama-C 铝的 Db.Value.AfterTable.find api 更改

Question

我正在尝试将 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，而不是 Db.Value.state Frama-C 氟。有人可以帮我解决这个问题吗？

非常感谢， 特鲁克

Answer 1

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

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