Checkers.ReachingDefs
module Defs : sig ... end
The node in which the reaching definition x := e is defined.
module ReachingDefsMap : sig ... end
Map var -> its reaching definition
val compute_invariant_map : IR.Procdesc.t -> invariant_map
val extract_post :
IR.Procdesc.Node.id ->
invariant_map ->
ReachingDefsMap.t option