module type BACKWARD_MONOTONE_PARAMETER = sig
.. end
Statement-based backward dataflow. Contrary to the forward dataflow,
the transfer function cannot differentiate the state before a
statement between different predecessors.
include Dataflows.JOIN_SEMILATTICE
val transfer_stmt : Cil_types.stmt -> t -> t
transfer_stmt s state
must implement the transfer function for s
.
val init : (Cil_types.stmt * t) list
The initial state after each statement. Statements in this list are
given the associated value, and are added to the worklist. Other
statements are initialized to bottom.
To get results for an entire function, this list should contain
information for the following statements:
- the final statement of the function (
Kernel_function.find_return
)
- all the statements with no successors
- at least one statement per non-terminating loop