A | |
Abstract | Internal and External signature of abstractions used in the Eva engine. |
Abstract_domain | Abstract domains of the analysis. |
Abstract_location | Abstract memory locations of the analysis. |
Abstract_memory | |
Abstract_offset | |
Abstract_structure | |
Abstract_value | Abstract numeric values of the analysis. |
Abstractions | Registration and building of the analysis abstractions. |
Active_behaviors | |
AlarmOrProp [Red_statuses] | |
Alarmset | Map from alarms to status. |
AllRoundingModesConstants [Parameters] | |
AllocBuiltin [Parameters] | |
AllocFunctions [Parameters] | |
AllocReturnsNull [Parameters] | |
AllocatedContextValid [Parameters] | |
Analysis [Gui_eval.S] | |
Analysis | |
Analysis [Eva] | |
ArrayPrecisionLevel [Parameters] | |
AutoLoopUnroll [Parameters] | |
Auto_loop_unroll | Heuristic for automatic loop unrolling. |
AutomaticContextMaxDepth [Parameters] | |
AutomaticContextMaxWidth [Parameters] | |
B | |
Backward_formals | Functions related to the backward propagation of the value of formals at the end of a call. |
BaseToHCESet [Hcexprs] | Maps froms |
Bit [Abstract_memory] | |
Bound [Segmentation] | |
Builtins | |
Builtins [Eva] | |
BuiltinsAuto [Parameters] | |
BuiltinsList [Parameters] | |
BuiltinsOverrides [Parameters] | |
Builtins_float | Builtins for standard floating-point functions. |
Builtins_malloc | Dynamic allocation related builtins. |
Builtins_memory | Nothing is exported, all the builtins are registered through |
Builtins_misc | Builtins for normalization and dumping of values or state. |
Builtins_print_c | Translate a Value state into a bunch of C assertions |
Builtins_split | |
Builtins_string | A builtin takes the state and a list of values for the arguments, and returns the return value (which can be bottom), and a boolean indicating the possibility of alarms. |
Builtins_watchpoint | |
C | |
CVal [Main_values] | Abstract values built over Cvalue.V |
Callgraph [Eva_dynamic] | |
Callsite [Value_types] | |
Callstack [Value_types] | |
CardinalEstimate [Cvalue] | Estimation of the cardinal of the concretization of an abstract state or value. |
CilE | Value analysis alarms |
Clear_Valuation [Eval] | |
Complete [Domain_builder] | Automatically builds some functions of an abstract domain. |
Complete_Minimal [Domain_builder] | |
Complete_Minimal_with_datatype [Domain_builder] | |
Complete_Simple_Cvalue [Domain_builder] | |
Compute_functions | Value analysis of entire functions, using Eva engine. |
Computer [Iterator] | |
Config [Abstractions] | Configuration defining the abstractions to be used in an analysis. |
Cvalue | Representation of Value's abstract memory. |
CvalueOffsm [Offsm_value] | |
Cvalue_backward | Abstract reductions on Cvalue.V.t |
Cvalue_domain | Main domain of the Value Analysis. |
Cvalue_forward | Forward operations on Cvalue.V.t |
Cvalue_init | Creation of the initial state for Value |
Cvalue_offsetmap | Auxiliary functions on cvalue offsetmaps, used by the cvalue domain. |
Cvalue_specification | No function exported. |
Cvalue_transfer | Transfer functions for the main domain of the Value analysis. |
D | |
D [Inout_domain] | |
D [Symbolic_locs] | |
D [Offsm_domain] | |
D [Gauges_domain] | |
D [Traces_domain] | |
DatatypeIntegerRange [Eval_typ] | |
Default [Abstractions] | |
DefaultLoopUnroll [Parameters] | |
Default_offsetmap [Cvalue] | Values bound by default to a variable. |
DegenerationPoints [Eva_utils] | |
DescendingIteration [Parameters] | |
Disjunction [Abstract_structure] | |
Dom [Abstractions.S] | |
Domain [Abstract] | Key and structure for abstract domains. |
Domain_builder | Automatic builders to complete abstract domains from different simplified interfaces. |
Domain_lift | |
Domain_mode | This module defines the mode to restrict an abstract domain on specific functions. |
Domain_product | |
Domain_store | |
Domains [Parameters] | |
DomainsFunction [Parameters] | |
E | |
E [Hcexprs] | |
Edge [Traces_domain] | |
EnumerateCond [Parameters] | |
Equality | Representation of an equality between a set of elements. |
Equality | Equalities between syntactic lvalues and expressions. |
EqualityCall [Parameters] | |
EqualityCallFunction [Parameters] | |
Equality_domain | Initial abstract state at the beginning of a call. |
Eva | Eva public API. |
Eva_annotations | |
Eva_annotations [Eva] | |
Eva_audit | |
Eva_dynamic | Access to other plugins API via . |
Eva_perf | Call |
Eva_results | |
Eva_results [Eva] | |
Eva_utils | |
Eval [Abstractions.Eva] | |
Eval | |
Eval [Eva] | |
Eval_annots | |
Eval_op | Numeric evaluation. |
Eval_terms | Evaluation of terms and predicates |
Eval_terms [Eva] | |
Eval_typ | |
Evaluation | |
F | |
Flagged_Value [Eval] | |
ForceValues [Parameters] | |
FunctionStats [Summary] | |
Function_Mode [Domain_mode] | |
Function_args | Nothing is exported; the function |
Function_calls | |
G | |
GCallstackMap [Gui_types] | |
Gauges_domain | Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. |
General_requests | General Eva requests registered in the server. |
Graph [Traces_domain] | |
GraphShape [Traces_domain] | Can't use Graph.t it needs an impossible recursive module |
Gui_callstacks_filters | Filtering on analysis callstacks |
Gui_callstacks_manager | This module creates and manages the "Values" panel on the lower notebook of the GUI. |
Gui_eval | This module defines an abstraction to evaluate various things across multiple callstacks. |
Gui_red | Extension of the GUI in order to display red alarms emitted during the value analysis |
Gui_types | |
H | |
HCE [Hcexprs] | Datatype + utilities functions for hashconsed exprsessions. |
HCESet [Hcexprs] | Hashconsed sets of symbolic expressions. |
HCEToZone [Hcexprs] | Maps from symbolic expressions to their memory dependencies, expressed as a
|
Hashtbl [Datatype.S_with_collections] | |
Hcexprs | Hash-consed expressions and lvalues. |
HierarchicalConvergence [Parameters] | |
HistoryPartitioning [Parameters] | |
I | |
Initialization | Creation of the initial state of abstract domain. |
InitializationPaddingGlobals [Parameters] | |
InitializedLocals [Parameters] | |
Inout_domain | Computation of inputs of outputs. |
InterpreterMode [Parameters] | |
InterproceduralHistory [Parameters] | |
InterproceduralSplits [Parameters] | |
Interval [Main_values] | Dummy interval: no forward nor backward propagations. |
Iterator | |
J | |
JoinResults [Parameters] | |
K | |
Key [Datatype.Hashtbl] | Datatype for the keys of the hashtbl. |
Key [Datatype.Map] | Datatype for the keys of the map. |
Key [Partition] | |
Key_Domain [Structure] | Keys module for the abstract domains of Eva. |
Key_Location [Structure] | Keys module for the abstract locations of Eva. |
Key_Value [Structure] | Keys module for the abstract values of Eva. |
L | |
Legacy [Abstractions] | |
Library_functions | |
LinearLevel [Parameters] | |
LinearLevelFunction [Parameters] | |
Loc [Abstractions.S] | |
Locals_scoping | Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends. |
Location [Abstract] | Key and structure for abstract locations. |
Location_lift | |
Loops [Traces_domain] | |
M | |
Main_locations | Main memory locations of Eva: |
Main_values | Main numeric values of Eva. |
Make [Gui_eval] | |
Make [Gui_types] | The types below depend on the abstract values currently available. |
Make [Datatype.Hashtbl] | Build a datatype of the hashtbl according to the datatype of values in the hashtbl. |
Make [Datatype.Map] | Build a datatype of the map according to the datatype of values in the map. |
Make [Typed_memory] | |
Make [Segmentation] | |
Make [Abstract_structure] | |
Make [Analysis] | |
Make [Compute_functions] | |
Make [Initialization] | |
Make [Mem_exec] | |
Make [Transfer_specification] | |
Make [Transfer_stmt] | |
Make [Transfer_logic] | |
Make [Evaluation] | Generic functor. |
Make [Subdivided_evaluation] | |
Make [Trace_partitioning] | |
Make [Partitioning_index] | Partition of the abstract states, computed for each node by the dataflow analysis. |
Make [Partitioning_parameters] | |
Make [Auto_loop_unroll] | |
Make [Powerset] | Set of states, propagated through the edges by the dataflow analysis. |
Make [Equality_domain] | |
Make [Unit_domain] | |
Make [Domain_lift] | |
Make [Domain_product] | |
Make [Domain_store] | |
Make [Location_lift] | |
Make [Value_product] | |
Make [Structure] | |
MakeFlow [Partition] | Flows are used to transfer states from one partition to another, by applying transfer functions and partitioning actions. |
Make_Domain [Simple_memory] | |
Make_Memory [Simple_memory] | |
MallocLevel [Parameters] | |
Map [Datatype.S_with_collections] | |
MemExecAll [Parameters] | |
Mem_exec | |
MinLoopUnroll [Parameters] | |
Mode [Domain_mode] | Datatype for modes. |
Model [Cvalue] | Memories. |
Multidim |
|
MultidimDisjunctiveInvariants [Parameters] | |
MultidimSegmentLimit [Parameters] | |
Multidim_domain | |
N | |
NoResultsDomains [Parameters] | |
NoResultsFunctions [Parameters] | |
Node [Traces_domain] | |
NumerorsLogFile [Parameters] | |
Numerors_Mode [Parameters] | |
Numerors_Real_Size [Parameters] | |
O | |
OctagonCall [Parameters] | |
Octagons | |
Offsm [Offsm_value] | |
Offsm_domain | |
Offsm_value | |
Open [Structure] | Opens an internal tree module into an external one. |
OracleDepth [Parameters] | |
P | |
PLoc [Main_locations] | Abstract locations built over Precise_locs. |
Parameters | |
Parameters [Eva] | |
Partition | A partition is a collection of states, each identified by a unique key. |
Partitioning_index | A partitioning index is a collection of states optimized to determine if a new state is included in one of the states it contains — in a more efficient way than to test the inclusion with all stored states. |
Partitioning_parameters | |
Per_stmt_slevel | Fine-tuning for slevel, according to |
Powerset | |
Precise_locs | This module provides transient datastructures that may be more precise
than an |
Precision [Parameters] | Meta-option |
Pretty_memory | |
PrintCallstacks [Parameters] | |
Printer_domain | An abstract domain built on top of the Simpler_domains.Simple_Cvalue interface that just prints the transfer functions called by the engine during an analysis. |
R | |
Recursion | Handling of recursion cycles in the callgraph |
RecursiveUnroll [Parameters] | |
Red_statuses | |
ReduceOnLogicAlarms [Parameters] | |
ReductionDepth [Parameters] | |
Register | Functions of the Value plugin registered in |
Register_gui | Extension of the GUI in order to support the value analysis. |
ReportRedStatuses [Parameters] | |
Restrict [Domain_builder] | |
Results | |
Results [Eva] | |
ResultsAll [Parameters] | |
RmAssert [Parameters] | |
RteGen [Eva_dynamic] | |
S | |
Scope [Eva_dynamic] | |
Segmentation | |
Self | |
SemanticUnrollingLevel [Parameters] | |
Set [Datatype.S_with_collections] | |
Set [Equality] | Sets of equalities. |
Shape [Structure] | |
ShowSlevel [Parameters] | |
Sign_domain | Abstraction of the sign of integer variables. |
Sign_value | Sign domain: abstraction of integer numerical values by their signs. |
Simple_memory | Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction. |
Simpler_domains | Simplified interfaces for abstract domains. |
SkipLibcSpecs [Parameters] | |
SlevelFunction [Parameters] | |
SlevelMergeAfterLoop [Parameters] | |
SplitGlobalStrategy [Parameters] | |
SplitLimit [Parameters] | |
SplitReturnFunction [Parameters] | |
Split_return | This module is used to merge together the final states of a function according to a given strategy. |
Split_strategy | |
State [Cvalue_domain] | |
Status [Alarmset] | |
StopAtNthAlarm [Parameters] | |
Store [Abstract_domain.S] | Storage of the states computed by the analysis. |
Store [Domain_builder.LeafDomain] | |
Structure | Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes. |
Subdivided_evaluation | Subdivision of the evaluation on non-linear expressions: for expressions in which some l-values appear multiple times, proceed by disjunction on their abstract value, in order to gain precision. |
Subpart [Cvalue_domain] | |
Summary | Summary |
Symbolic_locs | Domain that store information on non-precise l-values such as
|
T | |
Taint_domain | Domain for a taint analysis. |
Trace_partitioning | |
TracesDot [Parameters] | |
TracesProject [Parameters] | |
TracesUnifyLoop [Parameters] | |
TracesUnrollLoop [Parameters] | |
Traces_domain | Traces domain |
Transfer_logic | |
Transfer_specification | |
Transfer_stmt | |
Typed_memory | |
U | |
UndefinedPointerComparisonPropagateAll [Parameters] | |
Unit_domain | |
Unit_tests | |
Unit_tests [Eva] | |
UsePrototype [Parameters] | |
V | |
V [Cvalue] | Values. |
V_Offsetmap [Cvalue] | Memory slices. |
V_Or_Uninitialized [Cvalue] | Values with 'undefined' and 'escaping addresses' flags. |
Val [Abstractions.S] | |
ValPerfFlamegraphs [Parameters] | |
ValShowPerf [Parameters] | |
ValShowProgress [Parameters] | |
Valuation [Evaluation.S] | Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached here. |
Value [Abstract] | Key and structure for abstract values. |
ValuePartitioning [Parameters] | |
Value_product | Cartesian product of two value abstractions. |
Value_types | Declarations that are useful for plugins written on top of the results of Value. |
Values_request | |
W | |
Warn | Alarms and imprecision warnings emitted during the analysis. |
WarnCopyIndeterminate [Parameters] | |
WarnPointerComparison [Parameters] | |
WarnPointerSubstraction [Parameters] | |
WarnSignedConvertedDowncast [Parameters] | |
Widen | Per-function computation of widening hints. |
Widen_hints_ext | Syntax extension for widening hints, used by Value. |
Widen_type | Widening hints for the Value Analysis datastructures. |
WideningDelay [Parameters] | |
WideningPeriod [Parameters] |