Module `Checkers.Loop_control`

val get_all_nodes_upwards_until : IR.Procdesc.Node.t -> IR.Procdesc.Node.t list -> Control.GuardNodes.t: Starting from the start_nodes, find all the nodes upwards until the target is reached, i.e picking up predecessors which have not been already added to the found_nodes

val get_loop_head_to_source_nodes : IR.Procdesc.t -> IR.Procdesc.Node.t list IR.Procdesc.NodeMap.t: Since there could be multiple back-edges per loop, collect all source nodes per loop head. loop_head (target of back-edges) --> source nodes

val get_loop_control_maps : IR.Procdesc.Node.t list IR.Procdesc.NodeMap.t -> Control.loop_control_maps: Get a pair of maps (exit_map, loop_head_to_guard_map) where exit_map : exit_node -> loop_head set (i.e. target of the back edges) loop_head_to_guard_map : loop_head -> guard_nodes and guard_nodes contains the nodes that may affect the looping behavior, i.e. occur in the guard of the loop conditional.

val get_loop_head_to_loop_nodes : IR.Procdesc.Node.t list IR.Procdesc.NodeMap.t -> Control.GuardNodes.t Checkers.Control.LoopHeadToGuardNodes.t: Get a map from loop head -> all the nodes included in the corresponding loop