Module Eva.Eval_terms

module Eval_terms: sig .. end

type eval_env 
Evaluation environment, built by env_annot.
type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t 
Dependencies needed to evaluate a term or a predicate.
type labels_states = Db.Value.state Cil_datatype.Logic_label.Map.t 
val env_annot : ?c_labels:labels_states ->
pre:Db.Value.state -> here:Db.Value.state -> unit -> eval_env
val predicate_deps : eval_env ->
Cil_types.predicate -> logic_deps option
predicate_deps env p computes the logic dependencies needed to evaluate p in the given evaluation environment env.
Returns None on either an evaluation error or on unsupported construct.