Value plugin

Directory domains

Section Apron (in domains/apron)

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.

Section Cvalue (in domains/cvalue)

Builtins	Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C
Builtins_float	Builtins for standard floating-point functions.
Builtins_malloc	Dynamic allocation related builtins.
Builtins_misc	Builtins for normalization and dumping of values or state.
Builtins_nonfree	Non-free Value builtins.
Builtins_nonfree_print_c	Translate a Value state into a bunch of C assertions
Builtins_nonfree_watchpoint
Builtins_string	Value builtins related to functions in string.h.
Cvalue_domain	Main domain of the Value Analysis.
Cvalue_init	Creation of the initial state for Value
Cvalue_specification	Evaluation of functions using their specification
Cvalue_transfer	Transfer functions for the main domain of the Value analysis.
Locals_scoping	Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends.

Section Equality (in domains/equality)

Equality	Type of the keys of the map.
Equality_domain	Initial abstract state at the beginning of a call.
Equality_sig	Signature for `Equality` module, that implements equalities over ordered types

Section Gauges (in domains/gauges)

Gauges_domain

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

Directory plugins

Section Value (in plugins/value)

Alarmset	Map from alarms to status.
Eval	Types and functions related to evaluations.
Register	Functions of the Value plugin registered in `Db`.
Value	Analysis for values and pointers
Value_parameters	Dynamic allocation

Section Value_types (in plugins/value_types)

CilE	Value analysis alarms
Cvalue	Representation of Value's abstract memory.
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.
Value_types	Declarations that are useful for plugins written on top of the results of Value.
Widen_type	Widening hints for the Value Analysis datastructures.

Directory value

Section Domains (in value/domains)

Abstract_domain	Abstract domains of the analysis.
Domain_builder
Domain_lift
Domain_product
Domain_store
Hcexprs	Hash-consed expressions and lvalues.
Offsm_domain	If `true`, the offsetmap domain stores information that can probably be re-synthesized from the value domain.
Powerset	Set of states, propagated through the edges by the dataflow analysis.
Symbolic_locs	Domain that store information on non-precise l-values such as `t[i]` or `*p` when `i` or `p` is not exact.
Unit_domain

Section Engine (in value/engine)

Abstractions	Constructions of the abstractions used by EVA.
Analysis	The abstractions used in the latest analysis, and its results.
Compute_functions	Value analysis of entire functions, using Eva engine.
Evaluation	Generic evaluation and reduction of expressions and left values.
Initialization	Creation of the initial state of abstract domain.
Mem_exec	Counter that must be used each time a new call is analyzed, in order to refer to it later
Non_linear_evaluation	Evaluation of non-linear expressions.
Partitioned_dataflow	Mark the analysis as aborted.
Partitioning	Partition of the abstract states, computed for each node by the dataflow analysis.
Recursion	Handling of recursion cycles in the callgraph
Split_return	This module is used to merge together the final states of a function according to a given strategy.
Transfer_logic	Check the postcondition of `kf` for the list of `behaviors`.
Transfer_stmt

Section Gui_files (in value/gui_files)

Gui_callstacks_filters	Filtering on analysis callstacks
Gui_eval	This module defines an abstraction to evaluate various things across multiple callstacks.
Gui_types
Register_gui	Extension of the GUI in order to support the value analysis.

Section Legacy (in value/legacy)

Eval_annots
Eval_op	Numeric evaluation.
Eval_terms	Evaluation of terms and predicates
Function_args	Nothing is exported; the function `compute_atual` is registered in `Db.Value`.
Warn	Alarms and imprecision warnings emitted during the analysis.

Section Slevel (in value/slevel)

Per_stmt_slevel	Fine-tuning for slevel, according to `//@ slevel` directives.
Separate
Split_strategy
Stop_at_nth

Section Utils (in value/utils)

Backward_formals	Functions related to the backward propagation of the value of formals at the end of a call.
Eval_typ	Functions related to type conversions
Library_functions	Fake varinfo used by Value to store the result of functions.
Mark_noresults
State_import	Saving/loading of Value states, possibly among different ASTs.
Structure	Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes.
Value_perf	Call `start_doing` when starting analyzing a new function.
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_util	Callstacks related types and functions
Widen	Per-function computation of widening hints.
Widen_hints_ext	Syntax extension for widening hints, used by Value.

Section Values (in value/values)

Abstract_location	Abstract memory locations of the analysis.
Abstract_value	Abstract numeric values of the analysis.
Cvalue_backward	Abstract reductions on Cvalue.V.t
Cvalue_forward	Forward operations on Cvalue.V.t
Location_lift
Main_locations	Main memory locations of EVA:
Main_values	Main numeric values of EVA.
Offsm_value	Auxiliary functions
Value_product	Cartesian product of two value abstractions.