Frama-C:
Plug-ins:
Libraries:

Frama-C API - Stmts_graph

Statements graph.

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 trivial 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

reachable_stmts kf stmt returns the transitive closure of the successors of stmt in kf. The result is cached for later calls.

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:

  • the entry point : coming from outside the loop
  • the back edges. Notice that there might be nothing in the entry point when the loop is the first statement.
  • raises Invalid_argument

    if the statement is not a loop.