module type FORWARD_MONOTONE_PARAMETER =sig
..end
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
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.