A | |
Abstract_domain |
Abstract domains of the analysis.
|
Abstract_location |
Abstract memory locations of the analysis.
|
Abstract_value |
Abstract numeric values of the analysis.
|
Abstractions |
Constructions of the abstractions used by EVA.
|
ActiveBehaviors [Eval_annots] | |
Alarm_cache [Value_messages] | |
Alarm_key [Value_messages] | |
Alarmset |
Map from alarms to status.
|
AllRoundingModes [Value_parameters] | |
AllRoundingModesConstants [Value_parameters] | |
AllocatedContextValid [Value_parameters] | |
ApronBox [Value_parameters] | |
ApronOctagon [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] | |
Atom [Equality_term] | |
AutomaticContextMaxDepth [Value_parameters] | |
AutomaticContextMaxWidth [Value_parameters] | |
B | |
BitwiseOffsmDomain [Value_parameters] | |
Box [Apron_domain] |
Intervals abstract domain.
|
Builtins |
Value analysis builtin shipped with Frama-C, more efficient than their
equivalent in C
|
BuiltinsOverrides [Value_parameters] | |
Builtins_float |
Builtins for standard floating-point functions.
|
Builtins_nonfree |
Non-free Value builtins.
|
Builtins_nonfree_deterministic |
Non-free Value builtins for deterministic code.
|
Builtins_nonfree_malloc |
Dynamic allocation related builtins.
|
Builtins_nonfree_print_c |
Translate a Value state into a bunch of C assertions
|
Builtins_nonfree_string |
Non-free Value builtins.
|
Builtins_nonfree_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] | |
Compute_functions |
Value analysis of entire functions, using Eva engine.
|
Computer [Partitioned_dataflow] | |
Computer [Eval_slevel] | |
Cvalue |
Representation of Value's abstract memory.
|
CvalueDomain [Value_parameters] | |
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_transfer |
Transfer functions for the main domain of the Value analysis.
|
D | |
D [Offsm_domain] | |
Default [Abstractions] | |
Default_offsetmap [Cvalue] |
Values bound by default to a variable.
|
DegenerationPoints [Value_util] | |
Dom [Abstractions.S] | |
Domain_lift | |
Domain_product | |
E | |
EnumerateCond [Value_parameters] | |
Equality |
Type of the keys of the map.
|
EqualityDomain [Value_parameters] | |
Equality_domain | |
Equality_sig |
Signature for
Equality module, that implements equalities
over ordered types
|
Equality_term |
Atom of the predicates.
|
Eva [Value_parameters] | |
Eval |
Types and functions related to evaluations.
|
Eval_annots |
Check the postcondition of
kf for a given behavior b .
|
Eval_behaviors |
Evaluation of functions using their specification
|
Eval_exprs |
Reduction by operators condition
|
Eval_funs |
Value analysis of entire functions, using the legacy engine.
|
Eval_non_linear |
Evaluation of non-linear expressions.
|
Eval_op |
Numeric evaluation.
|
Eval_slevel |
Value analysis of statements and functions bodies with slevel.
|
Eval_stmt |
Value analysis of statements and functions bodies.
|
Eval_terms |
Evaluation of terms and predicates
|
Eval_typ |
Functions related to type conversions
|
Evaluation |
Generic evaluation and reduction of expressions and left values.
|
F | |
FloatTimingStep [Value_parameters] | |
ForceValues [Value_parameters] | |
Function_args | |
G | |
GCallstackMap [Gui_types] | |
Gui_callstacks_filters |
Filtering on analysis callstacks
|
Gui_eval |
This module defines an abstraction to evaluate various things across
multiple callstacks.
|
Gui_types | |
H | |
HashBehaviors [Eval_annots.ActiveBehaviors] | |
Hashtbl [Datatype.S_with_collections] | |
Hptset [Equality_term.Atom] | |
I | |
IgnoreRecursiveCalls [Value_parameters] | |
Initial_state |
Creation of the initial state for Value.
|
Initialization |
Creation of the inital state of abstract domain.
|
InitializationPaddingGlobals [Value_parameters] | |
InterpreterMode [Value_parameters] | |
Interval [Main_values] |
Dummy interval: no forward nor backward propagations.
|
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_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 | |
LOffset [Lmap_bitwise.Location_map_bitwise] | |
Lattice_Set [Equality_term.Atom] | |
Legacy [Abstractions] | |
Library_functions |
Fake varinfo used by Value to store the result of functions without
bodies.
|
LinearLevel [Value_parameters] | |
Lmap_Bitwise [Equality_term.Atom] | |
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_lift | |
M | |
Main_locations |
Main memory locations of EVA:
|
Main_values |
Main numeric values of EVA.
|
Make [Initialization] | |
Make [Mem_exec2] | |
Make [Transfer_stmt] | |
Make [Transfer_logic] | |
Make [Non_linear_evaluation] | |
Make [Evaluation] |
Generic functor.
|
Make [Equality_domain] | |
Make [Equality] | |
Make [Unit_domain] | |
Make [Domain_lift] | |
Make [Domain_product] | |
Make [Location_lift] | |
Make [Value_product] | |
Make [Structure] | |
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_Partition [Partitioning] |
Partition of the abstract states, computed for each node by the
dataflow analysis.
|
Make_Set [Partitioning] |
Set of states, propagated through the edges by the dataflow analysis.
|
Map [Datatype.S_with_collections] | |
Mark_noresults | |
MemExecAll [Value_parameters] | |
Mem_exec |
This module memorizes the analysis of entire calls to a function,
so that those analyzes can be reused later on.
|
Mem_exec2 |
Counter that must be used each time a new call is analyzed, in order
to refer to it later
|
Mem_lvalue |
Improved handling of l-values that are read/written multiple times in
a function.
|
MemoryFootprint [Value_parameters] | |
Model [Cvalue] |
Memories.
|
N | |
NoResultsAll [Value_parameters] | |
NoResultsFunctions [Value_parameters] | |
Non_linear_evaluation |
Evaluation of non-linear expressions.
|
O | |
O [Lattice_type.Lattice_Hashconsed_Set] | |
ObviouslyTerminatesAll [Value_parameters] | |
ObviouslyTerminatesFunctions [Value_parameters] | |
Octagon [Apron_domain] |
Octagons abstract domain.
|
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.
|
Partitioned_dataflow |
Mark the analysis as aborted.
|
Partitioning |
Set of states, propagated through the edges by the dataflow analysis.
|
Per_stmt_slevel |
Fine-tuning for slevel, according to
//@ slevel directives.
|
PolkaEqualities [Value_parameters] | |
PolkaLoose [Value_parameters] | |
PolkaStrict [Value_parameters] | |
Polka_Equalities [Apron_domain] |
Linear equalities.
|
Polka_Loose [Apron_domain] |
Loose polyhedra of the NewPolka library.
|
Polka_Strict [Apron_domain] |
Strict polyhedra of the NewPolka library.
|
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.
|
PrintCallstacks [Value_parameters] | |
R | |
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.
|
ResultsCallstack [Value_parameters] | |
ReusedExprs [Value_parameters] | |
RmAssert [Value_parameters] | |
S | |
SaveFunctionState [Value_parameters] | |
SemanticUnrollingLevel [Value_parameters] | |
Separate | |
SeparateStmtOf [Value_parameters] | |
SeparateStmtStart [Value_parameters] | |
SeparateStmtWord [Value_parameters] | |
Set [Equality_sig.S_with_collections] | |
Set [Datatype.S_with_collections] | |
ShowSlevel [Value_parameters] | |
SlevelFunction [Value_parameters] | |
SlevelMergeAfterLoop [Value_parameters] | |
SplitGlobalStrategy [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_imp |
Sets of Cvalue.Model.t implemented imperatively.
|
State_import |
Saving/loading of Value states, possibly among different ASTs.
|
State_set |
Functional sets of
Cvalue.Model.t , currently implemented as lists
without repetition.
|
Status [Alarmset] | |
StopAtNthAlarm [Value_parameters] | |
Stop_at_nth | |
Structure |
Gadt describing the structure of a tree of different data types,
and providing fast accessors of its nodes.
|
Subpart [Cvalue_domain] | |
Summary [Abstract_domain.S] |
Datatypes
|
Summary [Mem_exec2.Domain] | |
T | |
Transfer [Abstract_domain.S] |
Transfer functions from the result of evaluations.
|
Transfer [Cvalue_transfer] | |
Transfer_logic |
Check the postcondition of
kf for a given behavior b .
|
Transfer_stmt | |
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] | |
ValShowInitialState [Value_parameters] | |
ValShowPerf [Value_parameters] | |
ValShowProgress [Value_parameters] | |
Valarms |
Emission of alarms.
|
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 |
Analysis for values and pointers
|
ValueOutputs [Mem_exec] |
Subtype of
Value_types.call_res
|
Value_Message_Callback [Value_messages] | |
Value_messages |
UNDOCUMENTED.
|
Value_parameters | |
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 [Value] | |
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] | |
WarnLeftShiftNegative [Value_parameters] | |
WarnPointerComparison [Value_parameters] | |
WarnPointerSubstraction [Value_parameters] | |
Widen |
Per-function computation of widening hints.
|
Widen_type |
Widening hints for the Value Analysis datastructures.
|
WideningLevel [Value_parameters] |