module type ForwardsTransfer =sig
..end
Interface to provide for a backward dataflow analysis.
val name : string
For debugging purposes, the name of the analysis
val debug : bool
Whether to turn on debugging
type
t
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. Useful when Dataflow2.ForwardsTransfer.t
is a mutable type.
A copy of the data stored for a statement is made each time this
statement is processed, just before Dataflow2.ForwardsTransfer.doStmt
is called.
val pretty : Stdlib.Format.formatter -> t -> unit
Pretty-print the state.
val computeFirstPredecessor : Cil_types.stmt ->
t -> t
computeFirstPredecessor s d
is called when s
is reached for the
first time (i.e. no previous data is associated with it). The data d
is propagated to s
from an unspecified preceding statement s'
.
The result of the call is stored as the new data for s
.
computeFirstPredecessor
usually leaves d
unchanged, but may
potentially change it. It is also possible to perform a side-effect,
for dataflows that store information out of the type t
.
val combinePredecessors : Cil_types.stmt ->
old:t ->
t -> t option
Take some old data for the given statement, and some new data for the same point. Return None if the combination is identical to the old data, to signify that a fixpoint is currently reached for this statement. Otherwise, compute the combination, and return it.
val doInstr : Cil_types.stmt ->
Cil_types.instr ->
t -> t
The (forwards) transfer function for an instruction, internally
called by Dataflow2.ForwardsTransfer.doStmt
when the returned action is not SDone
.
The current location is updated before this function is called.
The argument of type stmt
is the englobing statement.
val doGuard : Cil_types.stmt ->
Cil_types.exp ->
t ->
t Dataflow2.guardaction *
t Dataflow2.guardaction
Generate the successors act_th, act_el
to an If
statement. act_th
(resp. act_el
) corresponds to the case where the given expression
evaluates to zero (resp. non-zero). It is always possible to return
GDefault, GDefault
, especially for analyses that do not use guard
information. This is equivalent to returning GUse d, GUse d
, where d
is the input state. A return value of GUnreachable indicates
that this half of the branch will not be taken and should not be explored.
stmt
is the corresponding If
statement, passed as information only.
val doStmt : Cil_types.stmt ->
t ->
t Dataflow2.stmtaction
The (forwards) transfer function for a statement. The (Cil.CurrentLoc.get
* is set before calling this. The default action is to do the
instructions * in this statement, if applicable, and continue with the
successors.
())
val doEdge : Cil_types.stmt ->
Cil_types.stmt ->
t -> t
what to do when following the edge between the two given statements. Can default to identity if nothing special is required.
module StmtStartData:Dataflow2.StmtStartData
with type data = t
For each statement id, the data at the start.