module Eval_terms:sig..end
val annot_predicate_deps : pre:Cvalue.Model.t ->
here:Cvalue.Model.t -> Cil_types.predicate -> Locations.Zone.t optionannot_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.