Module EvaSource

Eva public API.

The main modules are:

The following modules allow configuring the Eva analysis:

Other modules are for internal use only.

Sourcemodule Analysis : sig ... end
Sourcemodule Callstack : 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. It aims at replacing most uses of Db.Value, and has some advantages over Db's :

Sourcemodule Parameters : sig ... end

Configuration of the analysis.

Sourcemodule Eva_annotations : sig ... end

Register special annotations to locally guide the Eva analysis:

Sourcemodule Eval : 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: