package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val at_entry : result -> state option

Extract the result at the entry point of the analysed function

val at_return : result -> state option

Extract the result at the return point of the analysed function (just after the return transfer function)

val before : result -> Cil_types.stmt -> state option

Extract the result obtained for the control point immediately before the given statement

val after : result -> Cil_types.stmt -> state option

Extract the result obtained for the control point immediately after the given statement

val iter_vertex : (vertex -> state -> unit) -> result -> unit

Iter on the results obtained at each vertex of the graph. Do nothing when the vertex is not reachable (for instance if transfer returned None)

val iter_stmt : (Cil_types.stmt -> state -> unit) -> result -> unit

Iter on the results obtained before each statements of the function. Do nothing when the vertex is not reachable (for instance if transfer returned None)

val to_dot_output : (Stdlib.Format.formatter -> state -> unit) -> result -> Stdlib.out_channel -> unit

Output result to the given channel. Must be supplied with a pretty printer for abstract values

val to_dot_file : (Stdlib.Format.formatter -> state -> unit) -> result -> Filepath.Normalized.t -> unit

Output result to a file with the given path. Must be supplied with pretty printer for abstract values

val as_table : result -> state Vertex.Hashtbl.t

Extract the result as a table from control points to states

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct