Module type Dataflows.FORWARD_MONOTONE_PARAMETER

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 switchs).

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.