Index of module types

C
Conversion [Domain_lift]
Conversion [Location_lift]
D
Domain [Mem_exec]
Domain [Partitioning]
Domain [Powerset]
E
External [Abstract_domain]

Final interface of domains, as generated and used by Eva, with generic accessors for domains.

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_domain]

External interface of a domain, with accessors.

Internal [Abstract_domain]

Full implementation of domains.

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.

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]
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 [Abstractions]

Types of the abstractions of the analysis: value, location and state abstractions.

S [Initialization]
S [Partitioning]
S [Transfer_stmt]
S [Evaluation]
S [Transfer_logic]
S [Powerset]
S [Apron_domain]

Signature of an Apron domain in Eva.

S [Simple_memory]

Signature of a simple memory abstraction for scalar variables.

S_with_Structure [Abstract_domain]

Structure of a domain.

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.

Standard_abstraction [Abstractions]

Type of abstractions that use the builtin types for values and locations

Store [Abstract_domain]

Automatic storage of the states computed during the analysis.

T
Transfer [Abstract_domain]

Transfer function of the domain.

V
Valuation [Abstract_domain]

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.

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]
Value [Evaluation]
Value [Simple_memory]

Abstraction of the values variables are mapped to.