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.
|
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.
|
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
|
Gauges_domain |
Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of
Linear Inequality Invariants.
|
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
|
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.
|
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 |
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 |
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.
|
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.
|
Per_stmt_slevel |
Fine-tuning for slevel, according to
//@ slevel directives.
|
Separate | |
Split_strategy | |
Stop_at_nth |
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.
|
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.
|