C | |
| Conversion [Domain_lift] | |
| Conversion [Location_lift] | |
D | |
| Domain [Mem_exec] | |
| Domain [Partitioning] | |
| Domain [Powerset] | |
E | |
| Element [Equality] | |
| 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 [Equality_sig] |
Representation of an equality between a set of elements.
|
| 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 [Equality_domain] | |
| 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.
|
| S_with_collections [Equality_sig] | |
| Set [Equality_sig] |
Sets of equalities.
|
| 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.
|