Module Dataflow

module Dataflow: sig .. end
Deprecated: use Dataflows instead. A framework for implementing data flow analysis.
Consult the Plugin Development Guide for additional details.

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
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.