A | |
Abs_Err [Numerors_arithmetics] | |
Abstract |
Internal and External signature of abstractions used in the Eva engine.
|
Abstract_domain |
Abstract domains of the analysis.
|
Abstract_location |
Abstract memory locations of the analysis.
|
Abstract_value |
Abstract numeric values of the analysis.
|
Abstractions |
Registration and building of the analysis abstractions.
|
ActiveBehaviors [Transfer_logic] | |
AlarmOrProp [Red_statuses] | |
AlarmsWarnings [Value_parameters] | |
Alarmset |
Map from alarms to status.
|
AllRoundingModesConstants [Value_parameters] | |
AllocFunctions [Value_parameters] | |
AllocReturnsNull [Value_parameters] | |
AllocatedContextValid [Value_parameters] | |
Analysis [Gui_eval.S] | |
Analysis |
The abstractions used in the latest analysis, and its results.
|
Approx [Numerors_arithmetics] | |
ApronStorage [Value_parameters] | |
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.
|
ArrayPrecisionLevel [Value_parameters] | |
AutoLoopUnroll [Value_parameters] | |
Auto_loop_unroll |
Heuristic for automatic loop unrolling.
|
AutomaticContextMaxDepth [Value_parameters] | |
AutomaticContextMaxWidth [Value_parameters] | |
B | |
Backward [Numerors_arithmetics.Arithmetic] | |
Backward_Comparisons [Numerors_arithmetics] |
Backward comparisons
|
Backward_formals |
Functions related to the backward propagation of the value of formals
at the end of a call.
|
BaseToHCESet [Hcexprs] |
Maps froms
Base.t to set of HCE.t .
|
BitwiseOffsmStorage [Value_parameters] | |
Builtins |
Value analysis builtin shipped with Frama-C, more efficient than their
equivalent in C
|
BuiltinsAuto [Value_parameters] | |
BuiltinsList [Value_parameters] | |
BuiltinsOverrides [Value_parameters] | |
Builtins_float |
Builtins for standard floating-point functions.
|
Builtins_malloc |
Dynamic allocation related builtins.
|
Builtins_memory |
Nothing is exported, all the builtins are registered through
|
Builtins_misc |
Builtins for normalization and dumping of values or state.
|
Builtins_print_c |
Translate a Value state into a bunch of C assertions
|
Builtins_split |
Enumeration
|
Builtins_string |
A builtin takes the state and a list of values for the arguments, and
returns the offsetmap of the return value (None if bottom), and a boolean
indicating the possibility of alarms.
|
Builtins_watchpoint | |
C | |
CVal [Main_values] |
Abstract values built over Cvalue.V
|
Callsite [Value_types] | |
Callstack [Value_types] | |
CardinalEstimate [Cvalue] |
Estimation of the cardinal of the concretization of an abstract state
or value.
|
CilE |
Value analysis alarms
|
Clear_Valuation [Eval] | |
Complete [Domain_builder] | |
Complete_Minimal [Domain_builder] | |
Complete_Minimal_with_datatype [Domain_builder] | |
Complete_Simple_Cvalue [Domain_builder] | |
Compute_functions |
Value analysis of entire functions, using Eva engine.
|
Computer [Iterator] | |
Config [Abstractions] |
Configuration defining the abstractions to be used in an analysis.
|
Cvalue |
Representation of Value's abstract memory.
|
CvalueOffsm [Offsm_value] | |
Cvalue_backward |
Abstract reductions on Cvalue.V.t
|
Cvalue_domain |
Main domain of the Value Analysis.
|
Cvalue_forward |
Forward operations on Cvalue.V.t
|
Cvalue_init |
Creation of the initial state for Value
|
Cvalue_offsetmap |
Auxiliary functions on cvalue offsetmaps, used by the cvalue domain.
|
Cvalue_specification |
No function exported.
|
Cvalue_transfer |
Transfer functions for the main domain of the Value analysis.
|
D | |
D [Inout_domain] | |
D [Symbolic_locs] | |
D [Offsm_domain] | |
D [Gauges_domain] | |
D [Traces_domain] | |
DatatypeIntegerRange [Eval_typ] | |
Default [Abstractions] | |
DefaultLoopUnroll [Value_parameters] | |
Default_offsetmap [Cvalue] |
Values bound by default to a variable.
|
DegenerationPoints [Value_util] | |
DescendingIteration [Value_parameters] | |
Dom [Abstractions.S] | |
Domain [Abstract] |
Key and structure for abstract domains.
|
Domain_builder |
Automatic builders to complete abstract domains from different
simplified interfaces.
|
Domain_lift | |
Domain_mode |
This module defines the mode to restrict an abstract domain on specific
functions.
|
Domain_product | |
Domain_store | |
Domains [Value_parameters] | |
DomainsFunction [Value_parameters] | |
E | |
E [Hcexprs] | |
Edge [Traces_domain] | |
EnumerateCond [Value_parameters] | |
Equality |
Representation of an equality between a set of elements.
|
Equality |
Equalities between syntactic lvalues and expressions.
|
EqualityCall [Value_parameters] | |
EqualityCallFunction [Value_parameters] | |
EqualityStorage [Value_parameters] | |
Equality_domain |
Initial abstract state at the beginning of a call.
|
Eva |
Analysis for values and pointers
|
Eva_annotations |
Registers Eva annotations: slevel annotations: "slevel default", "slevel merge" and "slevel i", loop unroll annotations: "loop unroll term", value partitioning annotations: "split term" and "merge term", subdivision annotations: "subdivide i"
Widen hints annotations are still registered in !.
|
Eval [Abstractions.Eva] | |
Eval |
Types and functions related to evaluations.
|
Eval_annots | |
Eval_op |
Numeric evaluation.
|
Eval_terms |
Evaluation of terms and predicates
|
Eval_terms [Eva] | |
Eval_typ |
Functions related to type conversions
|
Evaluation |
Generic evaluation and reduction of expressions and left values.
|
Exact [Numerors_arithmetics] |
Modules which implement the previous signature for each field of <t>
|
F | |
Flagged_Value [Eval] | |
ForceValues [Value_parameters] | |
Forward [Numerors_arithmetics.Arithmetic] | |
Function_Mode [Domain_mode] | |
Function_args |
Nothing is exported; the function
compute_atual is registered
in Db.Value .
|
G | |
GCallstackMap [Gui_types] | |
GaugesStorage [Value_parameters] | |
Gauges_domain |
Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of
Linear Inequality Invariants.
|
Graph [Traces_domain] | |
GraphShape [Traces_domain] |
Can't use Graph.t it needs an impossible recursive module
|
Gui_callstacks_filters |
Filtering on analysis callstacks
|
Gui_callstacks_manager |
This module creates and manages the "Values" panel on the lower notebook
of the GUI.
|
Gui_eval |
This module defines an abstraction to evaluate various things across
multiple callstacks.
|
Gui_red |
Extension of the GUI in order to display red alarms emitted during the
value analysis
|
Gui_types |
The types below depend on the abstract values currently available.
|
H | |
HCE [Hcexprs] |
Datatype + utilities functions for hashconsed exprsessions.
|
HCESet [Hcexprs] |
Hashconsed sets of symbolic expressions.
|
HCEToZone [Hcexprs] |
Maps from symbolic expressions to their memory dependencies, expressed as a
Locations.Zone.t .
|
Hashtbl [Datatype.S_with_collections] | |
Hcexprs |
Hash-consed expressions and lvalues.
|
HierarchicalConvergence [Value_parameters] | |
HistoryPartitioning [Value_parameters] | |
I | |
I [Numerors_arithmetics] | |
IgnoreRecursiveCalls [Value_parameters] | |
Initialization |
Creation of the initial state of abstract domain.
|
InitializationPaddingGlobals [Value_parameters] | |
InitializedLocals [Value_parameters] | |
Inout_domain |
Computation of inputs of outputs.
|
InterpreterMode [Value_parameters] | |
Interval [Main_values] |
Dummy interval: no forward nor backward propagations.
|
Iterator |
Mark the analysis as aborted.
|
J | |
JoinResults [Value_parameters] | |
K | |
Key [Datatype.Hashtbl] |
Datatype for the keys of the hashtbl.
|
Key [Datatype.Map] |
Datatype for the keys of the map.
|
Key [Partition] | |
Key_Domain [Structure] |
Keys module for the abstract domains of Eva.
|
Key_Location [Structure] |
Keys module for the abstract locations of Eva.
|
Key_Value [Structure] |
Keys module for the abstract values of Eva.
|
L | |
Legacy [Abstractions] | |
Library_functions |
Fake varinfo used by Value to store the result of functions.
|
LinearLevel [Value_parameters] | |
LinearLevelFunction [Value_parameters] | |
LoadFunctionState [Value_parameters] | |
Loc [Abstractions.S] | |
Locals_scoping |
Auxiliary functions to mark invalid (more precisely 'escaping') the
references to a variable whose scope ends.
|
Location [Abstract] |
Key and structure for abstract locations.
|
Location_lift | |
Loops [Traces_domain] | |
M | |
Main_locations |
Main memory locations of Eva:
|
Main_values |
Main numeric values of Eva.
|
Make [Gui_eval] | |
Make [Gui_types] |
The types below depend on the abstract values currently available.
|
Make [Datatype.Hashtbl] |
Build a datatype of the hashtbl according to the datatype of values in the
hashtbl.
|
Make [Datatype.Map] |
Build a datatype of the map according to the datatype of values in the
map.
|
Make [Analysis] | |
Make [Compute_functions] | |
Make [Initialization] | |
Make [Mem_exec] | |
Make [Trace_partitioning] | |
Make [Partitioning_index] |
Partition of the abstract states, computed for each node by the
dataflow analysis.
|
Make [Partitioning_parameters] | |
Make [Auto_loop_unroll] | |
Make [Transfer_specification] | |
Make [Transfer_stmt] | |
Make [Evaluation] |
Generic functor.
|
Make [Subdivided_evaluation] | |
Make [Transfer_logic] | |
Make [Powerset] |
Set of states, propagated through the edges by the dataflow analysis.
|
Make [Equality_domain] | |
Make [Unit_domain] | |
Make [Domain_lift] | |
Make [Domain_product] | |
Make [Domain_store] | |
Make [Location_lift] | |
Make [Value_product] | |
Make [Structure] | |
MakeFlow [Partition] |
Flows are used to transfer states from one partition to another, by
applying transfer functions and partitioning actions.
|
Make_Domain [Simple_memory] | |
Make_Memory [Simple_memory] | |
MallocLevel [Value_parameters] | |
Map [Datatype.S_with_collections] | |
Mark_noresults | |
MemExecAll [Value_parameters] | |
Mem_exec |
Counter that must be used each time a new call is analyzed, in order
to refer to it later
|
MinLoopUnroll [Value_parameters] | |
Mode [Numerors_utils] | |
Mode [Domain_mode] |
Datatype for modes.
|
Model [Cvalue] |
Memories.
|
N | |
NoResultsFunctions [Value_parameters] | |
Node [Traces_domain] | |
NumerorsLogFile [Value_parameters] | |
Numerors_Mode [Value_parameters] | |
Numerors_Real_Size [Value_parameters] | |
Numerors_arithmetics |
Type manipulated by the arithmetics
|
Numerors_domain |
Numerors domain: computes over-approximations of the rounding errors bounds
of floating-point computations.
|
Numerors_float |
Returns a t element representing a positive infinite value
|
Numerors_interval |
Opaque type of an interval.
|
Numerors_utils |
We handle the format defined in C.
|
Numerors_value |
Reduction of an error value according to a floating-point interval.
|
O | |
OctagonCall [Value_parameters] | |
Octagons | |
Offsm [Offsm_value] | |
Offsm_domain |
If
true , the offsetmap domain stores information that can probably be
re-synthesized from the value domain.
|
Offsm_value |
Auxiliary functions
|
Open [Structure] |
Opens an internal tree module into an external one.
|
OracleDepth [Value_parameters] | |
P | |
PLoc [Main_locations] |
Abstract locations built over Precise_locs.
|
Partition |
A partition is a collection of states, each identified by a unique key.
|
Partitioning_index |
A partitioning index is a collection of states optimized to determine
if a new state is included in one of the states it contains — in a more
efficient way than to test the inclusion with all stored states.
|
Partitioning_parameters | |
Per_stmt_slevel |
Fine-tuning for slevel, according to
//@ slevel directives.
|
Powerset |
Set of states, propagated through the edges by the dataflow analysis.
|
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.
|
Precision [Value_parameters] |
Meta-option
|
Precisions [Numerors_utils] | |
PrintCallstacks [Value_parameters] | |
Printer_domain |
An abstract domain built on top of the Simpler_domains.Simple_Cvalue
interface that just prints the transfer functions called by the engine
during an analysis.
|
R | |
Recursion |
Handling of recursion cycles in the callgraph
|
Red_statuses |
This modules stores the alarms and properties for which a red status has
been emitted.
|
ReduceOnLogicAlarms [Value_parameters] | |
ReductionDepth [Value_parameters] | |
Register |
Functions of the Value plugin registered in
Db .
|
Register_gui |
Extension of the GUI in order to support the value analysis.
|
Rel_Err [Numerors_arithmetics] | |
ReportRedStatuses [Value_parameters] | |
Restrict [Domain_builder] | |
ResultsAll [Value_parameters] | |
RmAssert [Value_parameters] | |
Rounding [Numerors_utils] | |
S | |
SaveFunctionState [Value_parameters] | |
SemanticUnrollingLevel [Value_parameters] | |
Set [Datatype.S_with_collections] | |
Set [Equality] |
Sets of equalities.
|
Shape [Structure] | |
ShowSlevel [Value_parameters] | |
Sign [Numerors_utils] | |
Sign_domain |
Abstraction of the sign of integer variables.
|
Sign_value |
Sign domain: abstraction of integer numerical values by their signs.
|
Simple_memory |
Simple memory abstraction for scalar non-volatile variables, built upon a
value abstraction.
|
Simpler_domains |
Simplified interfaces for abstract domains.
|
SkipLibcSpecs [Value_parameters] | |
SlevelFunction [Value_parameters] | |
SlevelMergeAfterLoop [Value_parameters] | |
SplitGlobalStrategy [Value_parameters] | |
SplitLimit [Value_parameters] | |
SplitReturnFunction [Value_parameters] | |
Split_return |
This module is used to merge together the final states of a function
according to a given strategy.
|
Split_strategy | |
State [Cvalue_domain] | |
State_import |
Saving/loading of Value states, possibly among different ASTs.
|
Status [Alarmset] | |
StopAtNthAlarm [Value_parameters] | |
Store [Abstract_domain.Internal] | |
Structure |
Gadt describing the structure of a tree of different data types,
and providing fast accessors of its nodes.
|
Subdivided_evaluation |
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.
|
Subpart [Cvalue_domain] | |
SymbolicLocsStorage [Value_parameters] | |
Symbolic_locs |
Domain that store information on non-precise l-values such as
t[i] or *p when i or p is not exact.
|
T | |
Trace_partitioning |
The states being partitioned
|
TracesDot [Value_parameters] | |
TracesProject [Value_parameters] | |
TracesUnifyLoop [Value_parameters] | |
TracesUnrollLoop [Value_parameters] | |
Traces_domain |
Traces domain
|
Transfer_logic |
Check the postcondition of
kf for the list of behaviors .
|
Transfer_specification | |
Transfer_stmt |
Applies the show_each or dump_each directives.
|
U | |
UndefinedPointerComparisonPropagateAll [Value_parameters] | |
Unit_domain | |
UsePrototype [Value_parameters] | |
V | |
V [Cvalue] |
Values.
|
V_Offsetmap [Cvalue] |
Memory slices.
|
V_Or_Uninitialized [Cvalue] |
Values with 'undefined' and 'escaping addresses' flags.
|
Val [Abstractions.S] | |
ValPerfFlamegraphs [Value_parameters] | |
ValShowInitialState [Value_parameters] | |
ValShowPerf [Value_parameters] | |
ValShowProgress [Value_parameters] | |
Valuation [Evaluation.S] |
Results of an evaluation: the results of all intermediate calculation (the
value of each expression and the location of each lvalue) are cached here.
|
Value [Abstract] |
Key and structure for abstract values.
|
ValuePartitioning [Value_parameters] | |
Value_parameters |
Dynamic allocation
|
Value_parameters [Eva] | |
Value_perf |
Call
start_doing when starting analyzing a new function.
|
Value_product |
Cartesian product of two value abstractions.
|
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_results [Eva] | |
Value_types |
Declarations that are useful for plugins written on top of the results
of Value.
|
Value_util |
Callstacks related types and functions
|
W | |
Warn |
Alarms and imprecision warnings emitted during the analysis.
|
WarnCopyIndeterminate [Value_parameters] | |
WarnPointerComparison [Value_parameters] | |
WarnPointerSubstraction [Value_parameters] | |
WarnSignedConvertedDowncast [Value_parameters] | |
Widen |
Per-function computation of widening hints.
|
Widen_hints_ext |
Syntax extension for widening hints, used by Value.
|
Widen_type |
Widening hints for the Value Analysis datastructures.
|
WideningDelay [Value_parameters] | |
WideningPeriod [Value_parameters] |