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