Module 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

type invariant_map
val compute_invariant_map : IR.Procdesc.t -> invariant_map
val extract_post : IR.Procdesc.Node.id -> invariant_map -> ReachingDefsMap.t option