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:
Kernel_function.find_return
)