sig
  val mark_kf_as_called : Cil_types.kernel_function -> unit
  val add_kf_caller :
    caller:Cil_types.kernel_function * Cil_types.stmt ->
    Cil_types.kernel_function -> unit
  val partition_terminating_instr :
    Cil_types.stmt -> Db.Value.callstack list * Db.Value.callstack list
  val is_non_terminating_instr : Cil_types.stmt -> bool
  type state_per_stmt = Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t
  val merge_states_in_db :
    Value_results.state_per_stmt Lazy.t -> Db.Value.callstack -> unit
  val merge_after_states_in_db :
    Value_results.state_per_stmt Lazy.t -> Db.Value.callstack -> unit
end