Index of module types


A
Arithmetic [Numerors_arithmetics]
Signature of an arithmetic

C
Conversion [Domain_lift]
Conversion [Location_lift]

D
Domain [Mem_exec]
Domain [Partitioning_index]
Domain [Powerset]

E
Eva [Abstractions]
The three abstractions plus an evaluation engine for these abstractions.
External [Abstract.Domain]
External [Abstract.Location]
External [Abstract.Value]
External [Structure]
External view of the tree, with accessors.

F
Forward_Evaluation [Subdivided_evaluation]

I
Input [Gui_callstacks_manager]
InputDomain [Domain_builder]
InputDomain [Domain_store]
Interface [Abstract]
External interface of an abstraction, built by Structure.Open.
Internal [Abstract_domain]
Full implementation of domains.
Internal [Abstract.Domain]
Internal [Abstract.Location]
Internal [Abstract.Value]
Internal [Structure]
Internal view of the tree, with the structure.

K
Key [Structure]
Keys identifying datatypes.

L
Lattice [Abstract_domain]
Lattice structure of a domain.
Leaf [Abstract_domain]
Signature for a leaf module of a domain.
Leaf [Abstract_location]
Signature for a leaf module of abstract locations.
Leaf [Abstract_value]
Signature for a leaf module of abstract values.
LogicDomain [Transfer_logic]

M
Minimal [Simpler_domains]
Simplest interface for an abstract domain.
Minimal_with_datatype [Simpler_domains]
The simplest interface of domains, equipped with a frama-c datatype.

Q
Queries [Abstract_domain]
Extraction of information: queries for values or locations inferred by a domain about expressions and lvalues.
Queries [Evaluation]

R
Results [Analysis]
Reuse [Abstract_domain]
MemExec is a global cache for the complete analysis of functions.

S
S [Gui_eval]
The types and function below depend on the abstract domains and values currently available in Eva.
S [Gui_types]
S [Abstract_domain]
Signature for the abstract domains of the analysis.
S [Abstract_location]
Signature of abstract memory locations.
S [Abstract_value]
Signature of abstract numerical values.
S [Analysis]
S [Initialization]
S [Transfer_stmt]
S [Abstractions]
The three abstractions used in an Eva analysis.
S [Evaluation]
S [Transfer_logic]
S [Powerset]
S [Simple_memory]
Signature of a simple memory abstraction for scalar variables.
Shape [Structure]
A Key module with its structure type.
Simple_Cvalue [Simpler_domains]
A simple interface allowing the abstract domain to use the value and location abstractions computed by the other domains.
Store [Abstract_domain]
Automatic storage of the states computed during the analysis.

T
Transfer [Abstract_domain]
Transfer function of the domain.

V
Valuation [Eval]
Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached in a map.
Value [Abstractions]
The external signature of value abstractions, plus the reduction function of the reduced product.
Value [Evaluation]
Value [Simple_memory]
Abstraction of the values variables are mapped to.

D
domain_functor [Abstractions]
Module type of a functor building a leaf domain from a value abstraction.

L
leaf_domain [Abstractions]
Module type of a leaf domain over precise_loc abstraction.