package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Register actions to performed during the Eva analysis, with access to the states of the cvalue domain. This API is for internal use only, and may be modified or removed in a future version. Please contact us if you need to register callbacks to be executed during an Eva analysis.

type analysis_kind = [
  1. | `Builtin of Frama_c_kernel.Value_types.call_froms
  2. | `Spec of Frama_c_kernel.Cil_types.funspec
  3. | `Def
  4. | `Memexec
]
val register_call_hook : (callstack -> Frama_c_kernel.Cil_types.kernel_function -> analysis_kind -> state -> unit) -> unit

Registers a function to be applied at the beginning of the analysis of each function call. Arguments of the callback are the callstack of the call, the function called, the kind of analysis performed by Eva for this call, and the cvalue state at the beginning of the call.

type results = {
  1. before_stmts : state_by_stmt;
  2. after_stmts : state_by_stmt;
}
type call_results =
  1. | Store of results * int
    (*

    Cvalue states before and after each statement of the given function, plus a unique integer id for the call.

    *)
  2. | Reuse of int
    (*

    The results are the same as a previous call with the given integer id, previously recorded with the Store constructor.

    *)

Results of a function call.

val register_call_results_hook : (callstack -> Frama_c_kernel.Cil_types.kernel_function -> call_results -> unit) -> unit

Registers a function to be applied at the end of the analysis of each function call. Arguments of the callback are the callstack of the call, the function called and the cvalue states resulting from its analysis.

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