module type FORWARD_MONOTONE_PARAMETER =sig
..end
Edge-based forward dataflow. It is edge-based because the transfer function can differentiate the state after a statement between different successors. In particular, the state can be reduced according to the conditions in if statements.
include Dataflows.JOIN_SEMILATTICE
val transfer_stmt : Cil_types.stmt -> t -> (Cil_types.stmt * t) list
transfer_stmt s state
must returns a list of pairs in which the
first element is a statement s'
in s.succs
, and the second
element a value that will be joined with the current result for
before s'
.
Note that it is allowed that not all succs are present in the
list returned by transfer_stmt
(in which case, the successor is
assumed to be unreachable in the current state), or that succs are
present several times (this is useful to handle switches).
Helper functions are provided for If
and Switch
statements. See
Dataflows.transfer_if_from_guard
and Dataflows.transfer_switch_from_guard
below.
val init : (Cil_types.stmt * t) list
The initial value for each statement. Statements in this list are given the associated value, and are added to the worklist. Other statements are initialized to bottom.
Unless you want to do something very specific, supplying only the state
for the first statement of the function (as found by
Kernel_function.find_first_stmt
) is sufficient.