Index of modules

Abstract domains of the analysis.

Abstract memory locations of the analysis.

Abstract numeric values of the analysis.

Constructions of the abstractions used by EVA.

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.

Intervals abstract domain.

Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C

Builtins for standard floating-point functions.

Non-free Value builtins.

Non-free Value builtins for deterministic code.

Dynamic allocation related builtins.

Translate a Value state into a bunch of C assertions

Non-free Value builtins.

Abstract values built over Cvalue.V

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

Value analysis alarms

Value analysis of entire functions, using Eva engine.

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

Transfer functions for the main domain of the Value analysis.

Values bound by default to a variable.

Type of the keys of the map.

Signature for Equality module, that implements equalities over ordered types

Atom of the predicates.

Types and functions related to evaluations.

Check the postcondition of kf for a given behavior b.

Evaluation of functions using their specification

Reduction by operators condition

Value analysis of entire functions, using the legacy engine.

Evaluation of non-linear expressions.

Numeric evaluation.

Value analysis of statements and functions bodies with slevel.

Value analysis of statements and functions bodies.

Evaluation of terms and predicates

Functions related to type conversions

Generic evaluation and reduction of expressions and left values.

Filtering on analysis callstacks

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

Creation of the initial state for Value.

Creation of the inital state of abstract domain.

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.

Fake varinfo used by Value to store the result of functions without bodies.

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

Main memory locations of EVA:

Main numeric values of EVA.

Generic functor.

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.

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

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

This module memorizes the analysis of entire calls to a function, so that those analyzes can be reused later on.

Counter that must be used each time a new call is analyzed, in order to refer to it later

Improved handling of l-values that are read/written multiple times in a function.

Memories.

Evaluation of non-linear expressions.

Octagons abstract domain.

If true, the offsetmap domain stores information that can probably be re-synthesized from the value domain.

Auxiliary functions

Opens an internal tree module into an external one.

Abstract locations built over Precise_locs.

Mark the analysis as aborted.

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

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

Linear equalities.

Loose polyhedra of the NewPolka library.

Strict polyhedra of the NewPolka library.

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.

Functions of the Value plugin registered in Db.

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

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

Sets of Cvalue.Model.t implemented imperatively.

Saving/loading of Value states, possibly among different ASTs.

Functional sets of Cvalue.Model.t, currently implemented as lists without repetition.

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

Datatypes

Transfer functions from the result of evaluations.

Check the postcondition of kf for a given behavior b.

Values.

Memory slices.

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

Emission of alarms.

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

Analysis for values and pointers

Subtype of Value_types.call_res

UNDOCUMENTED.

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.

Callstacks related types and functions

Alarms and imprecision warnings emitted during the analysis.

Per-function computation of widening hints.

Widening hints for the Value Analysis datastructures.