package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct