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, or that succs are present several times (this is useful to handle switchs).

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.