Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva

Eva public API.

Main API

module Analysis : sig ... end

Run the analysis and check analysis status.

module Results : sig ... end

Main API to access the results of an analysis, such as the possible values of expressions and memory locations of lvalues at each program point.

Statistics

module Eva_perf : sig ... end

Statistics about the analysis performance.

module Statistics : sig ... end

Various statistics collected during an analysis.

Types used in Eva

module Eva_ast : sig ... end

AST used by Eva.

module Callstack : sig ... end

Types of callstack.

module Deps : sig ... end

Types for the memory dependencies of an expression or lvalue.

Configuration of the analysis

module Parameters : sig ... end

Command-line parameters of the analysis.

module Eva_annotations : sig ... end

Add local annotations to guide the analysis.

module Builtins : sig ... end

Register OCaml builtins to be used by the cvalue domain instead of analysing the body of some C functions.

Internal API

These modules are for internal use only. They may be modified or removed in future versions. Please contact us if you need features from these modules.

module Export : sig ... end

Generation of annotations.

module Assigns : sig ... end

Types and operations for the From plugin.

module Cvalue_callbacks : sig ... end

Register hooks called during the analysis with states of the cvalue domain.

module Logic_inout : sig ... end

Interpretation of predicates and assigns clauses for Inout and From plugins.

module Eva_results : sig ... end

Undocumented.

module Unit_tests : sig ... end

Unit testing.