module Eval_terms:sig
..end
type
eval_env
Evaluation environment, built by env_annot
.
typelogic_deps =
Locations.Zone.t Cil_datatype.Logic_label.Map.t
Dependencies needed to evaluate a term or a predicate.
typelabels_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
.