Module Checkers.LoopInvariant

module InvariantVars : sig ... end
module VarsInLoop : sig ... end
module LoopNodes : sig ... end
module VarSet : sig ... end
module LoopHeadToLoopNodes = IR.Procdesc.NodeMap

Map loop header node -> all nodes in the loop

module LoopHeadToInvVars = IR.Procdesc.NodeMap

Map loop head -> invariant vars in loop

type invariant_map = VarsInLoop.t IR.Procdesc.NodeMap.t
val get_inv_vars_in_loop : IR.Tenv.t -> ReachingDefs.invariant_map -> is_pure_by_default:bool -> get_callee_purity: (IR.Procname.t -> PurityDomain.ModifiedParamIndices.t Absint.AbstractDomain.Types.top_lifted option) -> IR.Procdesc.Node.t -> LoopNodes.t -> VarSet.t