package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.0-beta-Cobalt.tar.gz

sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

doc/frama-c.kernel/Frama_c_kernel/Stmts_graph/index.html

Module `Frama_c_kernel.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

val reachable_stmts : 
  Cil_types.kernel_function ->
  Cil_types.stmt ->
  Cil_datatype.Stmt.Hptset.t

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.