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 call_assigns = (Assigns.t * Frama_c_kernel.Locations.Zone.t) option

If not None:

  • the assigns of the function, i.e. the dependencies of the result and the dependencies of each zone written to;
  • and its sure outputs, i.e. an under-approximation of written zones.
type analysis_kind = [
  1. | `Builtin
    (*

    A cvalue builtin is used to interpret the function.

    *)
  2. | `Spec
    (*

    The specification is used to interpret the function.

    *)
  3. | `Body
    (*

    The function body is analyzed. This is the standard case.

    *)
  4. | `Reuse
    (*

    The results of a previous analysis of the function are reused.

    *)
]

Signature of a hook to be called before the analysis of each function call. Arguments are the callstack of the call, the function called, the initial cvalue state, and the kind of analysis performed by Eva for this call.

val register_call_hook : call_hook -> unit

Registers a function to be applied at the start of the analysis of each function call.

type state_by_stmt = state Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.t Stdlib.Lazy.t
type results = {
  1. before_stmts : state_by_stmt;
  2. after_stmts : state_by_stmt;
}
type call_results = [
  1. | `Builtin of state list * call_assigns
    (*

    List of cvalue states at the end of the builtin.

    *)
  2. | `Spec of state list
    (*

    List of cvalue states at the end of the call.

    *)
  3. | `Body of results * int
    (*

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

    *)
  4. | `Reuse of int
    (*

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

    *)
]

Results of a function call.

Signature of a hook to be called after the analysis of each function call. Arguments are the callstack of the call, the function called, the initial cvalue state at the start of the call, and the results from its analysis.

val register_call_results_hook : call_results_hook -> unit

Registers a function to be applied at the end of the analysis of each function call.

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