我正在尝试将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。有没有人能帮我一下?
非常感谢,Truc
发布于 2016-09-07 14:56:45
事实上,现在的信息更精确了。但您可以通过调用堆栈连接状态来计算状态:
let state = Value_callstack.Callstack.Hashtbl.fold
(fun _cs state acc -> Cvalue.Model.join acc state)
csh Cvalue.Model.bottomhttps://stackoverflow.com/questions/39354133
复制相似问题