Module Checkers.ReachingDefs
module Defs : module type of sig ... end
The node in which the reaching definition x := e is defined.
module ReachingDefsMap : module type of 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