Module Dataflow

module Dataflow: sig .. end

A framework for data flow analysis for CIL code. Before using this framework, you must initialize the Control-flow Graph for your program, e.g using Cfg.computeFileCFG


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.

*)
module type ForwardsTransfer = sig .. end
module ForwardsDataFlow: 
functor (T : ForwardsTransfer) -> sig .. end
module type BackwardsTransfer = sig .. end
module BackwardsDataFlow: 
functor (T : BackwardsTransfer) -> sig .. end
val find_stmts : Cil.fundec -> Cil.stmt list * Cil.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 statments (including statements that fall through the end of a void function). Useful when you need an initial set of statements for BackwardsDataFlow.compute.