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.

The abstractions used in the latest analysis, and its results.

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.

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.

Intervals abstract domain.

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

Builtins for standard floating-point functions.

Dynamic allocation related builtins.

Builtins for normalization and dumping of values or state.

Non-free Value builtins.

Translate a Value state into a bunch of C assertions

Enumeration

Value builtins related to functions in string.h.

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

No function exported.

Transfer functions for the main domain of the Value analysis.

Values bound by default to a variable.

Automatic builders to complete abstract domains from different simplified interfaces.

Type of the keys of the map.

Initial abstract state at the beginning of a call.

Signature for Equality module, that implements equalities over ordered types

Types and functions related to evaluations.

Numeric evaluation.

Evaluation of terms and predicates

Functions related to type conversions

Generic evaluation and reduction of expressions and left values.

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.

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.

The types below depend on the abstract values currently available.

Datatype + utilities functions for Hcexprs.hashconsed_exprs.

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.

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

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.

The types below depend on the abstract values currently available.

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

Generic functor.

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

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.

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

Memories.

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.

Partition of the abstract states, computed for each node 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.

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

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.

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.

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.

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

Alarms are triples (kind, text, warning_msg): Alarm kind, Message text (to be emitted via emit_alarm), Warning message (to be emitted via Value_util.alarm_report)

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.

Transfer functions from the result of evaluations.

Check the postcondition of kf for the list of behaviors.

Applies the show_each or dump_each directives.

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.

Analysis for values and pointers

Dynamic allocation

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.

Syntax extension for widening hints, used by Value.

Widening hints for the Value Analysis datastructures.