Index of modules

Internal and External signature of abstractions used in the Eva engine.

Abstract domains of the analysis.

Abstract memory locations of the analysis.

Abstract numeric values of the analysis.

Registration and building of the analysis abstractions.

Map from alarms to status.

Experimental binding for the numerical abstract domains provided by the APRON library: http://apron.cri.ensmp.fr/library For now, this binding only processes scalar integer variables.

Heuristic for automatic loop unrolling.

Backward comparisons

Functions related to the backward propagation of the value of formals at the end of a call.

Maps froms Base.t to set of HCE.t.

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

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

Builtins for standard floating-point functions.

Dynamic allocation related builtins.

Nothing is exported, all the builtins are registered through

Builtins for normalization and dumping of values or state.

Translate a Value state into a bunch of C assertions

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.

Abstract values built over Cvalue.V

Estimation of the cardinal of the concretization of an abstract state or value.

Value analysis alarms

Automatically builds some functions of an abstract domain.

Value analysis of entire functions, using Eva engine.

Configuration defining the abstractions to be used in an analysis.

Representation of Value's abstract memory.

Abstract reductions on Cvalue.V.t

Main domain of the Value Analysis.

Forward operations on Cvalue.V.t

Creation of the initial state for Value

Auxiliary functions on cvalue offsetmaps, used by the cvalue domain.

No function exported.

Transfer functions for the main domain of the Value analysis.

Values bound by default to a variable.

Key and structure for abstract domains.

Automatic builders to complete abstract domains from different simplified interfaces.

This module defines the mode to restrict an abstract domain on specific functions.

Representation of an equality between a set of elements.

Equalities between syntactic lvalues and expressions.

Initial abstract state at the beginning of a call.

Analysis for values and pointers

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

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

Numeric evaluation.

Evaluation of terms and predicates

Modules which implement the previous signature for each field of <t>

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

Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of Linear Inequality Invariants.

General Eva requests registered in the server.

Can't use Graph.t it needs an impossible recursive module

Filtering on analysis callstacks

This module creates and manages the "Values" panel on the lower notebook of the GUI.

This module defines an abstraction to evaluate various things across multiple callstacks.

Extension of the GUI in order to display red alarms emitted during the value analysis

Datatype + utilities functions for hashconsed exprsessions.

Hashconsed sets of symbolic expressions.

Maps from symbolic expressions to their memory dependencies, expressed as a Locations.Zone.t.

Hash-consed expressions and lvalues.

Creation of the initial state of abstract domain.

Computation of inputs of outputs.

Dummy interval: no forward nor backward propagations.

Datatype for the keys of the hashtbl.

Datatype for the keys of the map.

Keys module for the abstract domains of Eva.

Keys module for the abstract locations of Eva.

Keys module for the abstract values of Eva.

Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends.

Key and structure for abstract locations.

Main memory locations of Eva:

Main numeric values of Eva.

The types below depend on the abstract values currently available.

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Build a datatype of the map according to the datatype of values in the map.

Generic functor.

Partition of the abstract states, computed for each node by the dataflow analysis.

Set of states, propagated through the edges by the dataflow analysis.

Flows are used to transfer states from one partition to another, by applying transfer functions and partitioning actions.

Are the states of the function analysis saved?

Datatype for modes.

Memories.

Numerors domain: computes over-approximations of the rounding errors bounds of floating-point computations.

Opens an internal tree module into an external one.

Abstract locations built over Precise_locs.

A partition is a collection of states, each identified by a unique key.

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.

Fine-tuning for slevel, according to //@ slevel directives.

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.

Meta-option

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.

Handling of recursion cycles in the callgraph

Functions of the Value plugin registered in Db.

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

Sets of equalities.

Abstraction of the sign of integer variables.

Sign domain: abstraction of integer numerical values by their signs.

Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction.

Simplified interfaces for abstract domains.

This module is used to merge together the final states of a function according to a given strategy.

Storage of the states computed by the analysis.

Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes.

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.

Domain that store information on non-precise l-values such as t[i] or *p when i or p is not exact.

Domain for a taint analysis.

Traces domain

Currently tested by this file: semantics of sign values.

Values.

Memory slices.

Values with 'undefined' and 'escaping addresses' flags.

Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached here.

Key and structure for abstract values.

Call start_doing when starting analyzing a new function.

Cartesian product of two value abstractions.

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

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

Alarms and imprecision warnings emitted during the analysis.

Per-function computation of widening hints.

Syntax extension for widening hints, used by Value.

Widening hints for the Value Analysis datastructures.