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.

Main domain of the Value Analysis.

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.

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

Alarms and imprecision warnings emitted during the analysis.

Equalities between syntactic lvalues and expressions.

Initial abstract state at the beginning of a call.

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

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

Map from alarms to status.

Eva public API.

Functions of the Value plugin registered in Db.

Value analysis alarms

Representation of Value's abstract memory.

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.

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

Widening hints for the Value Analysis datastructures.

General Eva requests registered in the server.

Abstract domains of the analysis.

Automatic builders to complete abstract domains from different simplified interfaces.

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

Hash-consed expressions and lvalues.

Computation of inputs of outputs.

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.

Abstraction of the sign of integer variables.

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

Simplified interfaces for abstract domains.

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

Registration and building of the analysis abstractions.

Value analysis of entire functions, using Eva engine.

Creation of the initial state of abstract domain.

Handling of recursion cycles in the callgraph

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.

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

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

Numeric evaluation.

Evaluation of terms and predicates

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

Heuristic for automatic loop unrolling.

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 is used to merge together the final states of a function according to a given strategy.

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

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

Access to other plugins API via .

Call start_doing when starting analyzing a new function.

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

Summary

Per-function computation of widening hints.

Syntax extension for widening hints, used by Value.

Abstract memory locations of the analysis.

Abstract numeric values of the analysis.

Abstract reductions on Cvalue.V.t

Forward operations on Cvalue.V.t

Main memory locations of Eva:

Main numeric values of Eva.

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

Cartesian product of two value abstractions.