Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva

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.

module Analysis : sig ... end
module 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.

module Parameters : sig ... end

Configuration of the analysis.

module Eva_annotations : sig ... end

Register special annotations to locally guide the Eva analysis:

module Eval : sig ... end
module Assigns : sig ... end
module Eva_ast : sig ... end

Eva Syntax Tree.

module Builtins : sig ... end

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

module 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 Eva_perf : sig ... end

Statistics about the analysis performance.

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.

module 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: