Module Stmts_graph

module Stmts_graph: sig .. end
Statements graph.
Consult the Plugin Development Guide for additional details.

val stmt_can_reach : Cil_types.kernel_function -> Cil_types.stmt -> Cil_types.stmt -> bool
stmt_can_reach kf s1 s2 is true iff the control flow can reach s2 starting at s1 in function kf.
val stmt_can_reach_filtered : (Cil_types.stmt -> bool) -> Cil_types.stmt -> Cil_types.stmt -> bool
Just like stmt_can_reach but uses a function to filter the nodes of the graph it operates on. Note that the output of the filter function must be functionally dependent on its input
val stmt_is_in_cycle : Cil_types.stmt -> bool
stmt_is_in_cycle s is true iff s is reachable through a non trival path starting at s.
val stmt_is_in_cycle_filtered : (Cil_types.stmt -> bool) -> Cil_types.stmt -> bool
Just like stmt_is_in_cycle but uses a function to filter the nodes of the graph it operates on. Note that the output of the filter function must be functionally dependent on its input
val reachable_stmts : Cil_types.kernel_function -> Cil_types.stmt -> Cil_types.stmt list
val get_stmt_stmts : Cil_types.stmt -> Cil_datatype.Stmt.Set.t
Get the statements that compose s. For a simple statement (not containing blocks), it is only the statement itself.
val get_block_stmts : Cil_types.block -> Cil_datatype.Stmt.Set.t
val get_all_stmt_last_stmts : Cil_types.stmt -> Cil_types.stmt list
Find the last statements in s, meaning that if s' is in the returned statements, s' is in s statements, but a least one of its successor is not.
val get_all_block_last_stmts : Cil_types.block -> Cil_types.stmt list
val get_stmt_last_stmts : Cil_types.termination_kind option -> Cil_types.stmt -> Cil_types.stmt list
Subset of get_all_stmt_last_stmts according to termination_kind. termination_kind = None means Goto.
Raises Invalid_argument for termination_kind = Some Exits since every call possibly have an Exits termination: it should be handled differently.
val get_block_last_stmts : Cil_types.termination_kind option -> Cil_types.block -> Cil_types.stmt list
val get_stmt_in_edges : Cil_types.stmt -> (Cil_types.stmt * Cil_types.stmt) list
Find the entry edges that go inside s statements, meaning that if the pair (s1,s2) is in the returned information, s2 is a successor of s1 and s2 is in s statements, but s1 is not.
Since Nitrogen-20111001
val get_block_in_edges : Cil_types.block -> (Cil_types.stmt * Cil_types.stmt) list
val get_all_stmt_out_edges : Cil_types.stmt -> (Cil_types.stmt * Cil_types.stmt) list
Like get_stmt_in_edges but for edges going out of s statements. Similar to get_all_stmt_last_stmts but gives the edge information instead of just the first statement.
Since Nitrogen-20111001
val get_all_block_out_edges : Cil_types.block -> (Cil_types.stmt * Cil_types.stmt) list
val loop_preds : Cil_types.stmt -> Cil_types.stmt list * Cil_types.stmt list
Split the loop predecessors into:
Raises Invalid_argument if the statement is not a loop.