package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-eva.core/Eva/Cvalue_callbacks/index.html

Module `Eva.Cvalue_callbacks`Source

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 state = Frama_c_kernel.Cvalue.Model.t

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 = [

| `Builtin
(*
A cvalue builtin is used to interpret the function.
*)
| `Spec
(*
The specification is used to interpret the function.
*)
| `Body
(*
The function body is analyzed. This is the standard case.
*)
| `Reuse
(*
The results of a previous analysis of the function are reused.
*)

]

type call_hook =
  Callstack.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  state ->
  analysis_kind ->
  unit

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 Lazy.t

type results = {

before_stmts : state_by_stmt;
after_stmts : state_by_stmt;

}

type call_results = [

| `Builtin of state list * call_assigns
(*
List of cvalue states at the end of the builtin.
*)
| `Spec of state list
(*
List of cvalue states at the end of the call.
*)
| `Body of results * int
(*
Cvalue states before and after each statement of the given function, plus a unique integer id for the call.
*)
| `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.

type call_results_hook =
  Callstack.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  state ->
  call_results ->
  unit

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.