Search code examples
frama-c

Db.Value.AfterTable.find api change for Frama-C Aluminium

I am trying to migrate a plugin for Frama-C Fluorine version to Frama-C Aluminium. When doing so, I cannot find the appropriate replacement for function Db.Value.AfterTable.find, the closest one I found is Db.Value.AfterTable_By_Callstack.find. However, that function now returns different type, which is Db.Value.AfterTable_By_Callstack.data = Db.Value.state Value_types.Callstack.Hashtbl.t, rather than Db.Value.state in Frama-C Fluorine. Could anyone please help me with this?

Many thanks, Truc

Solution

  • Indeed, the information is now more precise. But you can compute the state by joining the states by call stack with :

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