Module Eva.Eval_terms

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.