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_value

Abstract numeric values of the analysis.

Abstractions

Registration and building of the analysis abstractions.

ActiveBehaviors [Transfer_logic]
AlarmOrProp [Red_statuses]
Alarmset

Map from alarms to status.

AllRoundingModesConstants [Value_parameters]
AllocBuiltin [Value_parameters]
AllocFunctions [Value_parameters]
AllocReturnsNull [Value_parameters]
AllocatedContextValid [Value_parameters]
Analysis [Gui_eval.S]
Analysis
ApronStorage [Value_parameters]
ArrayPrecisionLevel [Value_parameters]
AutoLoopUnroll [Value_parameters]
Auto_loop_unroll

Heuristic for automatic loop unrolling.

AutomaticContextMaxDepth [Value_parameters]
AutomaticContextMaxWidth [Value_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.

BitwiseOffsmStorage [Value_parameters]
Builtins

Eva analysis builtins for the cvalue domain, more efficient than their equivalent in C.

Builtins [Eva]

Analysis builtins for the cvalue domain, more efficient than the analysis of the C functions.

BuiltinsAuto [Value_parameters]
BuiltinsList [Value_parameters]
BuiltinsOverrides [Value_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

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]
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 [Value_parameters]
Default_offsetmap [Cvalue]

Values bound by default to a variable.

DegenerationPoints [Value_util]
DescendingIteration [Value_parameters]
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 [Value_parameters]
DomainsFunction [Value_parameters]
E
E [Hcexprs]
Edge [Traces_domain]
EnumerateCond [Value_parameters]
Equality

Representation of an equality between a set of elements.

Equality

Equalities between syntactic lvalues and expressions.

EqualityCall [Value_parameters]
EqualityCallFunction [Value_parameters]
EqualityStorage [Value_parameters]
Equality_domain

Initial abstract state at the beginning of a call.

Eva

Analysis for values and pointers

Eva_annotations

Registers Eva annotations: slevel annotations: "slevel default", "slevel merge" and "slevel i", loop unroll annotations: "loop unroll term", value partitioning annotations: "split term" and "merge term", subdivision annotations: "subdivide i" Widen hints annotations are still registered in !.

Eva_annotations [Eva]

Register special annotations to locally guide the partitioning of states performed by an Eva analysis.

Eva_audit
Eval [Abstractions.Eva]
Eval
Eval_annots
Eval_op

Numeric evaluation.

Eval_terms

Evaluation of terms and predicates

Eval_terms [Eva]
Eval_typ
Evaluation
F
Flagged_Value [Eval]
ForceValues [Value_parameters]
Function_Mode [Domain_mode]
Function_args

Nothing is exported; the function compute_atual is registered in Db.Value.

G
GCallstackMap [Gui_types]
GaugesStorage [Value_parameters]
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 [Value_parameters]
HistoryPartitioning [Value_parameters]
I
Initialization

Creation of the initial state of abstract domain.

InitializationPaddingGlobals [Value_parameters]
InitializedLocals [Value_parameters]
Inout_domain

Computation of inputs of outputs.

InterpreterMode [Value_parameters]
Interval [Main_values]

Dummy interval: no forward nor backward propagations.

Iterator
J
JoinResults [Value_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 [Value_parameters]
LinearLevelFunction [Value_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 [Analysis]
Make [Compute_functions]
Make [Initialization]
Make [Mem_exec]
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 [Transfer_specification]
Make [Transfer_stmt]
Make [Evaluation]

Generic functor.

Make [Subdivided_evaluation]
Make [Transfer_logic]
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 [Value_parameters]
Map [Datatype.S_with_collections]
Mark_noresults
MemExecAll [Value_parameters]
Mem_exec
MinLoopUnroll [Value_parameters]
Mode [Domain_mode]

Datatype for modes.

Model [Cvalue]

Memories.

N
NoResultsFunctions [Value_parameters]
Node [Traces_domain]
NumerorsLogFile [Value_parameters]
Numerors_Mode [Value_parameters]
Numerors_Real_Size [Value_parameters]
O
OctagonCall [Value_parameters]
Octagons
Offsm [Offsm_value]
Offsm_domain
Offsm_value
Open [Structure]

Opens an internal tree module into an external one.

OracleDepth [Value_parameters]
P
PLoc [Main_locations]

Abstract locations built over Precise_locs.

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 [Value_parameters]

Meta-option

PrintCallstacks [Value_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 [Value_parameters]
Red_statuses
ReduceOnLogicAlarms [Value_parameters]
ReductionDepth [Value_parameters]
Register

Functions of the Value plugin registered in Db.

Register_gui

Extension of the GUI in order to support the value analysis.

ReportRedStatuses [Value_parameters]
Restrict [Domain_builder]
ResultsAll [Value_parameters]
RmAssert [Value_parameters]
S
SemanticUnrollingLevel [Value_parameters]
Set [Datatype.S_with_collections]
Set [Equality]

Sets of equalities.

Shape [Structure]
ShowSlevel [Value_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 [Value_parameters]
SlevelFunction [Value_parameters]
SlevelMergeAfterLoop [Value_parameters]
SplitGlobalStrategy [Value_parameters]
SplitLimit [Value_parameters]
SplitReturnFunction [Value_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 [Value_parameters]
Store [Abstract_domain.Internal]
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]
SymbolicLocsStorage [Value_parameters]
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
Trace_partitioning
TracesDot [Value_parameters]
TracesProject [Value_parameters]
TracesUnifyLoop [Value_parameters]
TracesUnrollLoop [Value_parameters]
Traces_domain

Traces domain

Transfer_logic
Transfer_specification
Transfer_stmt
U
UndefinedPointerComparisonPropagateAll [Value_parameters]
Unit_domain
Unit_tests

Currently tested by this file: semantics of sign values.

Unit_tests [Eva]
UsePrototype [Value_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 [Value_parameters]
ValShowPerf [Value_parameters]
ValShowProgress [Value_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 [Value_parameters]
Value_parameters
Value_parameters [Eva]
Value_perf

Call start_doing when starting analyzing a new function.

Value_product

Cartesian product of two value abstractions.

Value_results

This file will ultimately contain all the results computed by Value (which must be moved out of Db.Value), both per stack and globally.

Value_results [Eva]
Value_types

Declarations that are useful for plugins written on top of the results of Value.

Value_util
Values_request
W
Warn

Alarms and imprecision warnings emitted during the analysis.

WarnCopyIndeterminate [Value_parameters]
WarnPointerComparison [Value_parameters]
WarnPointerSubstraction [Value_parameters]
WarnSignedConvertedDowncast [Value_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 [Value_parameters]
WideningPeriod [Value_parameters]