sig
  module Value_results :
    sig
      type results
      val get_results : unit -> Eva.Value_results.results
      val set_results : Eva.Value_results.results -> unit
      val merge :
        Eva.Value_results.results ->
        Eva.Value_results.results -> Eva.Value_results.results
      val change_callstacks :
        (Value_types.callstack -> Value_types.callstack) ->
        Eva.Value_results.results -> Eva.Value_results.results
    end
  module Value_parameters :
    sig val enabled_domains : unit -> (string * string) list end
  module Eval_terms :
    sig
      type eval_env
      type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
      type labels_states = Db.Value.state Cil_datatype.Logic_label.Map.t
      val env_annot :
        ?c_labels:Eva.Eval_terms.labels_states ->
        pre:Db.Value.state ->
        here:Db.Value.state -> unit -> Eva.Eval_terms.eval_env
      val predicate_deps :
        Eva.Eval_terms.eval_env ->
        Cil_types.predicate -> Eva.Eval_terms.logic_deps option
    end
end