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

Question

Я пытаюсь перенести плагин для версии фтора Frama-C на алюминий Frama-C. При этом я не могу найти подходящую замену для функции 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. Может ли кто-нибудь помочь мне в этом?

Большое спасибо, Truc

Answer 1

Действительно, информация теперь более точно. Но вы можете вычислить состояние путем присоединения государств по стеку вызовов с:

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