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.