module type BackwardsTransfer = sig .. end
val name : string
For debugging purposes, the name of the analysis
val debug : bool ref
Whether to turn on debugging
type
The type of the data we compute for each block start. In many
presentations of backwards data flow analysis we maintain the
data at the block end. This is not easy to do with JVML because
a block has many exceptional ends. So we maintain the data for
the statement start.
val pretty : unit -> t -> Pretty.doc
Pretty-print the state
val stmtStartData : t Inthash.t
For each block id, the data at the start. This data structure must be
initialized with the initial data for each block
val funcExitData : t
The data at function exit. Used for statements with no successors.
This is usually bottom, since we'll also use doStmt on Return
statements.
val combineStmtStartData : Cil.stmt ->
old:t ->
t -> t option
When the analysis reaches the start of a block, combine the old data
with the one we have just computed. Return None if the combination is
the same as the old data, otherwise return the combination. In the
latter case, the predecessors of the statement are put on the working
list.
val combineSuccessors : t ->
t -> t
Take the data from two successors and combine it
val doStmt : Cil.stmt -> t Dataflow.action
The (backwards) transfer function for a branch. The
Cil.currentLoc is
set before calling this. If it returns None, then we have some default
handling. Otherwise, the returned data is the data before the branch
(not considering the exception handlers)
val doInstr : Cil.instr ->
t -> t Dataflow.action
The (backwards) transfer function for an instruction. The
Cil.currentLoc is set before calling this. If it returns None, then we
have some default handling. Otherwise, the returned data is the data
before the branch (not considering the exception handlers)
val filterStmt : Cil.stmt -> Cil.stmt -> bool
Whether to put this predecessor block in the worklist. We give the
predecessor and the block whose predecessor we are (and whose data has
changed)