Module Reachingdefs.DF

module DF: Dataflow2

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 backward 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 statments (including statements that fall through the end of a void function). Useful when you need an initial set of statements for BackwardsDataFlow.compute.