Module Checkers.Control

module LoopHead = IR.Procdesc.Node
module LoopHeads = IR.Procdesc.NodeSet
module ControlMap : sig ... end

Map control var -> loop head location

module ExitNodeToLoopHeads = IR.Procdesc.NodeMap

Map exit node -> loop head set

module LoopHeadToGuardNodes = IR.Procdesc.NodeMap

Map loop head -> prune nodes in the loop guard

type invariant_map
type loop_control_maps = {
  1. exit_map : LoopHeads.t ExitNodeToLoopHeads.t;
  2. loop_head_to_guard_nodes : GuardNodes.t LoopHeadToGuardNodes.t;
}
val compute_invariant_map : IR.Procdesc.t -> loop_control_maps -> invariant_map
val compute_control_vars : invariant_map -> LoopInvariant.VarsInLoop.t LoopHeadToGuardNodes.t -> LoopHead.t -> IBase.Location.t ControlMap.t