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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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 callstack =
  (Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.kinstr)
    list

type state = Frama_c_kernel.Cvalue.Model.t

type analysis_kind = [

| `Builtin of Frama_c_kernel.Value_types.call_froms
| `Spec of Frama_c_kernel.Cil_types.funspec
| `Def
| `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 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 =

| Store 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 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.