Index of modules

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 Base.t to set of HCE.t.

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 start_doing when starting analyzing a new function.

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 compute_atual is registered in Db.Value.

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 Locations.Zone.t.

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

offset is an abstraction for array indexes when these arrays are used as a representation of multidimensional arrays or structures.

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 //@ slevel directives.

Powerset
Precise_locs

This module provides transient datastructures that may be more precise than an Ival.t, Locations.Location_Bits.t and Locations.location respectively, typically for l-values such as t[i][j], p->t[i], etc.

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 Db.

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[i] or *p when i or p is not exact.

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]