Value plugin


Directory domains

Section Apron (in domains/apron)


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