C | |
Config [Typed_memory] | |
Config [Segmentation] | |
Config [Abstract_structure] | |
Conversion [Domain_lift] | |
Conversion [Location_lift] | |
D | |
Disjunction [Abstract_structure] | |
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 |
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. |
LeafDomain [Domain_builder] | Part of an abstract domain signature automatically built by the
|
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. |
P | |
ProtoMemory [Abstract_memory] | |
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 [Transfer_logic] | |
S [Abstractions] | The three abstractions used in an Eva analysis. |
S [Evaluation] | |
S [Powerset] | |
S [Simple_memory] | Signature of a simple memory abstraction for scalar variables. |
S [Domain_store] | Automatic storage of the states computed during the analysis. |
Segmentation | |
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. |
Structure [Abstract_structure] | |
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 [Typed_memory] | |
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. |