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 |
(* | Do not do the default action. Use this result | *) |
| |
Post of |
(* | 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 |
(* | 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 |
(* | Use this data for the branch | *) |
| |
GUnreachable |
(* | The branch will never be taken. | *) |
module type ForwardsTransfer =sig
..end
module ForwardsDataFlow:
module type BackwardsTransfer =sig
..end
module BackwardsDataFlow:
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.