Module `InferModules.Control`

module LoopHead = InferIR.Procdesc.Node

module LoopHeads = InferIR.Procdesc.NodeSet

module ControlMap : module type of sig ... end: Map control var -> loop head location

module GuardNodes : module type of sig ... end

module ExitNodeToLoopHeads = InferIR.Procdesc.NodeMap: Map exit node -> loop head set

module LoopHeadToGuardNodes = InferIR.Procdesc.NodeMap: Map loop head -> prune nodes in the loop guard

type invariant_map
type loop_control_maps = { exit_map : LoopHeads.t ExitNodeToLoopHeads.t; loop_head_to_guard_nodes : GuardNodes.t LoopHeadToGuardNodes.t; }

val compute_invariant_map : Summary.t -> InferIR.Tenv.t -> loop_control_maps -> invariant_map
val compute_control_vars : invariant_map -> LoopInvariant.VarsInLoop.t LoopHeadToGuardNodes.t -> LoopHead.t -> InferBase.Location.t ControlMap.t