package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

sha256=0e5809db85a00f7dad24ad1645133467c101083ad0a5842bc66c2f312d156a5b

module _ : FUNCTION_ENV

module P : BACKWARD_MONOTONE_PARAMETER

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

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

On This Page