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 'a action =

`\|`	`Default`	`(*`	The default action	`*)`
`\|`	`Done of 'a`	`(*`	Do not do the default action. Use this result	`*)`
`\|`	`Post of ('a -> 'a)`	`(*`	The default action, followed by the given transformer	`*)`

type 'a stmtaction =

`\|`	`SDefault`	`(*`	The default action	`*)`
`\|`	`SDone`	`(*`	Do not visit this statement or its successors	`*)`
`\|`	`SUse of 'a`	`(*`	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 'a guardaction =

`\|`	`GDefault`	`(*`	The default state	`*)`
`\|`	`GUse of 'a`	`(*`	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.