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.