C | |
Conversion [Domain_lift] | |
Conversion [Location_lift] | |
D | |
Domain [Mem_exec] | |
Domain [Partitioning_index] | |
Domain [Powerset] | |
E | |
Eva [Abstractions] | Module gathering: the analysis abstractions: value, location and state abstractions;, the evaluation functions for these abstractions. |
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 | |
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] | Types of the abstractions of the analysis: value, location and state abstractions. |
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. |