module type ForwardsTransfer = 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. May be
imperative.
val copy : t -> t
Make a deep copy of the data
val stmtStartData : t Inthash.t
For each statement id, the data at the start. Not found in the hash
table means nothing is known about the state at this point. At the end
of the analysis this means that the block is not reachable.
val pretty : unit -> t -> Pretty.doc
Pretty-print the state
val computeFirstPredecessor : Cil.stmt -> t -> t
Give the first value for a predecessors, compute the value to be set
for the block
val combinePredecessors : Cil.stmt ->
old:t ->
t -> t option
Take some old data for the start of a statement, and some new data for
the same point. Return None if the combination is identical to the old
data. Otherwise, compute the combination, and return it.
val doInstr : Cil.instr ->
t -> t Dataflow.action
The (forwards) transfer function for an instruction. The
Cil.currentLoc is set before calling this. The default action is to
continue with the state unchanged.
val doStmt : Cil.stmt ->
t ->
t Dataflow.stmtaction
The (forwards) transfer function for a statement. The
Cil.currentLoc
is set before calling this. The default action is to do the instructions
in this statement, if applicable, and continue with the successors.
val doGuard : Cil.exp ->
t ->
t Dataflow.guardaction
Generate the successor to an If statement assuming the given expression
is nonzero. Analyses that don't need guard information can return
GDefault; this is equivalent to returning GUse of the input.
A return value of GUnreachable indicates that this half of the branch
will not be taken and should not be explored. This will be called
twice per If, once for "then" and once for "else".
val filterStmt : Cil.stmt -> bool
Whether to put this statement in the worklist. This is called when a
block would normally be put in the worklist.