module Eval_terms:sig
..end
val annot_predicate_deps : pre:Cvalue.Model.t ->
here:Cvalue.Model.t -> Cil_types.predicate -> Locations.Zone.t option
annot_predicate_deps ~pre ~here p
computes the logic dependencies needed
to evaluate the predicate p
in a code annotation in cvalue state here
,
in a function whose pre-state is pre
.
Returns None on either an evaluation error or on unsupported construct.