Frama-C:
Plug-ins:
Libraries:

Frama-C API - Dataflow2

Implementation of data flow analyses over user-supplied domains.

type 't action =
  1. | Default
    (*

    The default action

    *)
  2. | Done of 't
    (*

    Do not do the default action. Use this result

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

    The default action, followed by the given transformer

    *)

possible kinds of action for backward analysis

type 't stmtaction =
  1. | SDefault
    (*

    The default action

    *)
  2. | SDone
    (*

    Do not visit this statement or its successors

    *)
  3. | 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 =
  1. | GDefault
    (*

    The default state

    *)
  2. | GUse of 't
    (*

    Use this data for the branch

    *)
  3. | 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 (_ : ForwardsTransfer) : sig ... end

Backwards Dataflow Analysis

module type BackwardsTransfer = sig ... end

Interface to provide for a backward dataflow analysis.

module Backwards (_ : 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.