Module type Dataflows.BACKWARD_MONOTONE_PARAMETER

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: