Module Frama_c_kernel.Dataflow2

Implementation of data flow analyses over user-supplied domains.

type 't action =
| Default(*

The default action

*)
| Done of 't(*

Do not do the default action. Use this result

*)
| Post of 't -> 't(*

The default action, followed by the given * transformer

*)

possible kinds of action for backward analysis

type 't stmtaction =
| SDefault(*

The default action

*)
| SDone(*

Do not visit this statement or its successors

*)
| SUse of 't(*

Visit the instructions and successors of this statement as usual, but use the specified state instead of the one that was passed to doStmt

*)
type 't guardaction =
| GDefault(*

The default state

*)
| GUse of 't(*

Use this data for the branch

*)
| GUnreachable(*

The branch will never be taken.

*)

For if statements

module type StmtStartData = sig ... end
module StartData (X : sig ... end) : StmtStartData with type data = X.t

This module can be used to instantiate the StmtStartData components of the functors below. It is implemented through stmt-indexed hashtables.

Forwards Dataflow Analysis

module type ForwardsTransfer = sig ... end

Interface to provide for a backward dataflow analysis.

module Forwards (T : ForwardsTransfer) : sig ... end

Backwards Dataflow Analysis

module type BackwardsTransfer = sig ... end

Interface to provide for a backward dataflow analysis.

module Backwards (T : BackwardsTransfer) : sig ... end
val find_stmts : Cil_types.fundec -> Cil_types.stmt list * Cil_types.stmt list
  • returns

    (all_stmts, sink_stmts), where all_stmts is a list of the statements in a function, and sink_stmts is a list of the return statements (including statements that fall through the end of a void function). Useful when you need an initial set of statements for BackwardsDataFlow.compute.