Module Dataflow

module Dataflow: sig .. end

Deprecated: use Dataflows instead. A framework for implementing data flow analysis.


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

*)
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: 
functor (X : sig
type t 
val size : int
end-> StmtStartData  with type data = X.t

This module can be used to instantiate the StmtStartData components of the functors below.

Forwards Dataflow Analysis

module type ForwardsTransfer = sig .. end

Interface to provide for a forward dataflow analysis.

module Forwards: 
functor (T : ForwardsTransfer-> sig .. end

Backwards Dataflow Analysis

module type BackwardsTransfer = sig .. end

Interface to provide for a backward dataflow analysis.

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