module type ForwardsTransfer =sig
..end
val name : string
val debug : bool Pervasives.ref
type
t
val copy : t -> t
val pretty : Format.formatter -> t -> unit
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
val doInstr : Cil_types.stmt ->
Cil_types.instr ->
t -> t Dataflow.action
Default
propagates the state
passed as an argument unchanged. The current location is updated before
this function is called.val doGuard : Cil_types.stmt ->
Cil_types.exp ->
t ->
t Dataflow.guardaction *
t Dataflow.guardaction
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 Dataflow.stmtaction
(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 filterStmt : Cil_types.stmt -> bool
val stmt_can_reach : Cil_types.stmt -> Cil_types.stmt -> bool
true
if ther is a path in the control-flow graph of the
function from the first statement to the second. Used to choose a "good"
node in the worklist. Suggested use is let stmt_can_reach =
Stmts_graph.stmt_can_reach kf
, where kf
is the kernel_function
being analyzed; let stmt_can_reach _ _ = true
is also correct,
albeit less efficientval doEdge : Cil_types.stmt ->
Cil_types.stmt -> t -> t
module StmtStartData:Dataflow.StmtStartData
with type data = t