Dataflows.Simple_forward
module Fenv : FUNCTION_ENV
module P : FORWARD_MONOTONE_PARAMETER
val pre_state : Cil_types.stmt -> P.t
val post_state : Cil_types.stmt -> P.t
This function calls transfer_stmt
on the result of pre_state
. Beware if transfer_stmt
is impure or costly
In this dataflow, the results are the pre-states of all the statements reachable from the statements from P.init
.
val fold_on_result : ( 'a -> Cil_types.stmt -> P.t -> 'a ) -> 'a -> 'a
val iter_on_result : ( Cil_types.stmt -> P.t -> unit ) -> unit