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 | |
Recycle [Abstract_domain] |
MemExec is a global cache for the complete analysis of functions.
|
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 [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 [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] |
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.
|