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
, or that succs are present several
times (this is useful to handle switchs).
val init : (Cil_types.stmt * t) list