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/index.html

Module `Eva`Source

Eva public API.

The main modules are:

Analysis: run the analysis.
Results: access analysis results, especially the values of expressions and memory locations of lvalues at each program point.

The following modules allow configuring the Eva analysis:

Parameters: change the configuration of the analysis.
Eva_annotations: add local annotations to guide the analysis.
Builtins: register ocaml builtins to be used by the cvalue domain instead of analysing the body of some C functions.

Other modules are for internal use only.

Sourcemodule Analysis : sig ... end

Sourcemodule Callstack : sig ... end

module Deps : sig ... end

module Results : sig ... end

Eva's result API is a new interface to access the results of an analysis, once it is completed. It may slightly change in the future.

Sourcemodule Parameters : sig ... end

Configuration of the analysis.

Sourcemodule Eva_annotations : sig ... end

Sourcemodule Eval : sig ... end

Sourcemodule Assigns : sig ... end

Sourcemodule Builtins : sig ... end

Eva analysis builtins for the cvalue domain, more efficient than their equivalent in C.

Sourcemodule Cvalue_callbacks : sig ... end

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.

module Logic_inout : sig ... end

Functions used by the Inout and From plugins to interpret predicate and assigns clauses. This API may change according to these plugins development.

Sourcemodule Eva_results : sig ... end

Internal temporary API: please do not use it, as it should be removed in a future version.

module Unit_tests : sig ... end

Currently tested by this module: