Module `Checkers.LoopInvariant`

module InvariantVars : module type of sig ... end

module VarsInLoop : module type of sig ... end

module LoopNodes : module type of sig ... end

module VarSet : module type of 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
val get_loop_inv_var_map : IR.Tenv.t -> (IR.Procname.t -> PurityDomain.ModifiedParamIndices.t Absint.AbstractDomain.Types.top_lifted option) -> ReachingDefs.invariant_map -> LoopNodes.t LoopHeadToInvVars.t -> invariant_map