Frama-C:
Plug-ins:
Libraries:

Frama-C API - Simple_backward

Parameters

module _ : FUNCTION_ENV

Signature

Retrieving the state before and after a statement.

val post_state : Cil_types.stmt -> P.t
val pre_state : Cil_types.stmt -> P.t

This function calls transfer_stmt on the result of post_state. Beware if transfer_stmt is impure or costly

Iterations on the results of the dataflow.

In this dataflow, the results are the post-states of all the statements that may reach the statements in 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