A | |
abstraction [Abstractions] |
Abstraction to be registered.
|
action [Partition] |
These actions redefine the partitioning by updating keys or spliting states.
|
action [Hptset.S] | |
alarm [Alarmset] | |
alarm_behavior [CilE] | |
alarm_mode [Eval_terms] |
Three modes to handle the alarms when evaluating a logical term.
|
alarm_or_property [Red_statuses] | |
argument [Eval] |
Argument of a function call.
|
assigned [Eval] |
Assigned values.
|
B | |
bound [Abstract_value] | |
bound_kind [Abstract_value] | |
branch [Partition] |
Junction branch id in the control flow
|
builtin [Builtins] | |
builtin [Simple_memory] |
A builtin is an ocaml function for the interpretation of a whole C function:
it takes the list of value arguments, and returns the result (that can be
bottom).
|
C | |
cacheable [Value_types] | |
call [Builtins] | |
call [Eval] |
A function call.
|
call_init_state [Equality_domain] | |
call_result [Value_types] |
Results of a a call to a function
|
call_result [Transfer_stmt.S] | |
call_site [Value_types] | |
call_site [Value_util] |
A call_stack is a list, telling which function was called at which
site.
|
callback_result [Value_types] | |
callstack [Value_types] |
Value callstacks, as used e.g.
|
callstack [Value_util] | |
clobbered_set [Locals_scoping] |
Set of bases that might contain a reference to a local or formal
variable.
|
context [Subdivided_evaluation.Forward_Evaluation] | |
cvalue [Simpler_domains] | |
cvalue_valuation [Simpler_domains] |
A simpler functional interface for valuations.
|
D | |
data [Structure.Shape] | |
data [State_builder.Hashtbl] | |
data [State_builder.Ref] |
Type of the referenced value.
|
data_by_callstack [Gui_callstacks_manager] | |
display_data_by_callstack [Gui_callstacks_manager] | |
domain [Abstractions] |
Type of domain to be registered: either a leaf module with
'v as value
abstraction, or a functor building a domain from any value abstraction.
|
E | |
edge [Traces_domain] | |
elt [Equality] |
The type of the equality elements.
|
eq [Structure] |
Equality witness between types.
|
equalities [Equality_domain.Make] | |
equality [Equality] | |
eval_env [Eval_terms] |
Evaluation environment.
|
eval_env [Eva.Eval_terms] |
Evaluation environment, built by
env_annot .
|
eval_result [Eval_terms] | |
evaluated [Eval] |
Most forward evaluation functions return the set of alarms resulting from
the operations, and a result which can be `Bottom, if the evaluation fails,
or the expected value.
|
evaluation_functions [Gui_eval.S] |
This is the record that encapsulates all evaluation functions
|
extended_location [Domain_lift.Conversion] | |
extended_value [Domain_lift.Conversion] | |
extended_value [Location_lift.Conversion] | |
F | |
filter [Gui_callstacks_filters] |
Filters on callstacks.
|
flag [Abstractions] |
Flag for an abstract domain.
|
flagged_value [Eval] |
Right values with 'undefined' and 'escaping addresses' flags.
|
flow [Trace_partitioning.Make] |
A set of states which are currently propagated
|
flow_annotation [Eva_annotations] | |
forward [Numerors_arithmetics.Arithmetic] | |
function_mode [Domain_mode] |
A function associated with an analysis mode.
|
G | |
gui_after [Gui_types] | |
gui_callstack [Gui_types] | |
gui_loc [Gui_types] | |
gui_offsetmap_res [Gui_types] | |
gui_res [Gui_types] | |
gui_selection [Gui_types] | |
gui_selection_data [Gui_eval] | |
H | |
hint_lval [Widen_hints_ext] |
Type of widening hints: a special kind of lval
for which the hints will apply and a list of names (e.g.
|
hint_vars [Widen_hints_ext] | |
I | |
if_consistent [Alarmset] | |
init_value [Abstract_domain] |
Value for the initialization of variables.
|
integer_range [Eval_typ] |
Abstraction of an integer type, more convenient than an
ikind because
it can also be used for bitfields.
|
internal_location [Domain_lift.Conversion] | |
internal_value [Domain_lift.Conversion] | |
internal_value [Location_lift.Conversion] | |
K | |
key [Map.S] |
The type of the map keys.
|
key [Abstract_domain] | |
key [Abstract_location] | |
key [Abstract_value] | |
key [Partition] |
Partitioning keys attached to states.
|
key [Abstract.Interface] | |
key [Structure.External] | |
key [Structure.Key] | |
key [State_builder.Hashtbl] | |
key [Parameter_sig.Map] |
Type of keys of the map.
|
key [Parameter_sig.Multiple_map] | |
key [Parameter_sig.Multiple_value_datatype] | |
kill_type [Hcexprs] |
Reason of the replacement of an lvalue
lval : Modified means that the
value of lval has been modified (in which case &lval is unchanged), and
Deleted means that lval is no longer in scope (in which case &lval
raises the NonExchangeable error).
|
L | |
labels_states [Eval_terms] | |
labels_states [Eva.Eval_terms] | |
left_value [Eval] |
Lvalue with its location and type.
|
loc [Evaluation.S] |
Location of an lvalue.
|
loc [Eval.Valuation] |
Abstract memory location.
|
location [Abstract_domain.Transfer] | |
location [Abstract_domain.Queries] |
Abstract memory locations associated to left values.
|
location [Abstract_location.S] |
abstract locations
|
location [Analysis.Results] | |
location [Transfer_stmt.S] | |
location [Cvalue_transfer] | |
logic_assign [Eval] | |
logic_dependencies [Value_types] |
Dependencies for the evaluation of a term or a predicate: for each
program point involved, sets of zones that must be read
|
logic_deps [Eval_terms] |
Dependencies needed to evaluate a term or a predicate
|
logic_deps [Eva.Eval_terms] |
Dependencies needed to evaluate a term or a predicate.
|
logic_environment [Abstract_domain] |
Environment for the logical evaluation of predicates.
|
logic_evaluation_error [Eval_terms] |
Error during the evaluation of a term or a predicate
|
loops [Traces_domain] |
stack of open loops
|
lvalues [Hcexprs] | |
M | |
merge [Per_stmt_slevel] | |
mode [Domain_mode] |
Mode for the analysis of a function
f : current is the read/write permission for f ., calls is the read/write permission for all functions called from f .
|
N | |
node [Traces_domain] | |
O | |
offset [Abstract_location.S] |
abstract offsets
|
offsm_or_top [Offsm_value] | |
or_top [Eval] |
For some functions, the special value top (denoting no information)
is managed separately.
|
or_top_or_bottom [Eval] | |
origin [Abstract_domain.Transfer] | |
origin [Abstract_domain.Queries] |
The
origin is used by the domain combiners to track the origin
of a value.
|
origin [Evaluation.S] |
Origin of values.
|
origin [Cvalue_transfer] | |
origin [Eval.Valuation] |
Origin of values.
|
P | |
partition [Partition] |
Collection of states, each identified by a unique key.
|
permission [Domain_mode] |
Permission for an abstract domain to read/write its state.
|
pointer_comparison [Abstract_value] | |
precise_loc [Simpler_domains] | |
precise_loc [Abstractions] |
For the moment, all domains must use
precise_loc as their location
abstraction, and no new location abstraction can be registered for an
analysis.
|
precise_location [Precise_locs] | |
precise_location_bits [Precise_locs] | |
precise_offset [Precise_locs] | |
predicate_status [Eval_terms] |
Evaluating a predicate.
|
prefix [Cvalue_domain] | |
R | |
rationing [Partition] |
Rationing are used to keep separate the
n first states propagated at
a point, by creating unique stamp until the limit is reached.
|
rcallstack [Gui_callstacks_filters] |
List.rev on a callstack, enforced by strong typing outside of this module
|
record_loc [Eval] |
Data record associated to each evaluated left-value.
|
record_val [Eval] |
Data record associated to each evaluated expression.
|
reduced [Eval] |
Most backward evaluation function returns `Bottom if the reduction leads to
an invalid state, `Unreduced if no reduction can be performed, or the
reduced value.
|
reductness [Eval] |
State of reduction of an abstract value.
|
result [Builtins] | |
results [Value_results] |
Results
|
results [Eva.Value_results] | |
S | |
s [Alarmset] | |
scalar_typ [Eval_typ] |
Abstraction of scalar types -- in particular, all those that can be involved
in a cast.
|
shape [Hptset.S] |
Shape of the set, ie.
|
simple_argument [Simpler_domains] |
Both the formal argument of a called function and the concrete argument at a
call site.
|
simple_call [Simpler_domains] |
Simple information about a function call.
|
slevel [Per_stmt_slevel] | |
slevel_annotation [Eva_annotations] | |
split_kind [Partition] |
Splits on an expression can be static or dynamic: static splits are processed once: the expression is only evaluated at the
split point, and the key is then kept unchanged until a merge., dynamic splits are regularly redone: the expression is re-evaluated, and
states are then split or merged accordingly.
|
split_monitor [Partition] |
Split monitor: prevents splits from generating too many states.
|
split_strategy [Split_strategy] | |
state [Abstract_domain.S] | |
state [Abstract_domain.Transfer] | |
state [Abstract_domain.Queries] |
Domain state.
|
state [Abstract_domain.Lattice] | |
state [Analysis.Results] | |
state [Initialization.S] | |
state [Trace_partitioning.Make] |
The states being partitioned
|
state [Partition.MakeFlow] | |
state [Transfer_stmt.S] | |
state [Evaluation.S] |
State of abstract domain.
|
state [Transfer_logic.S] | |
state [Powerset.S] | |
state [Traces_domain] | |
state [Abstract_domain.Store] | |
states [Transfer_logic.S] | |
status [Alarmset] | |
store [Trace_partitioning.Make] |
The storage of all states ever met at a control point
|
str_builtin_sig [Builtins_string] | |
structure [Structure.Internal] | |
structure [Structure.Shape] |
The gadt, based on keys giving the type of each node.
|
T | |
t [Map.S] |
The type of maps from type
key to type 'a .
|
t [Cvalue.V_Or_Uninitialized] |
Semantics of the constructors:
C_init_* : definitely initialized, C_uninit_* : possibly uninitialized, C_*_noesc : never contains escaping addresses, C_*_esc : may contain escaping addresses C_uninit_noesc V.bottom : guaranteed to be uninitialized, C_init_esc V.bottom : guaranteed to be an escaping address, C_uninit_esc V.bottom : either uninitialized or an escaping address C_init_noesc V.bottom : "real" bottom, with an empty concretization.
Corresponds to an unreachable state.
|
t [Cvalue.CardinalEstimate] | |
t [Simpler_domains.Minimal] | |
t [Abstract_domain.Reuse] |
Type of states.
|
t [Numerors_arithmetics] |
Type manipulated by the arithmetics
|
t [Numerors_interval] |
Opaque type of an interval.
|
t [Numerors_float] | |
t [Numerors_utils.Mode] |
Those constructors corresponds to the possible values of the option
-eva-numerors-mode
|
t [Numerors_utils.Rounding] |
We only use the rounding to nearest (represented by the constructor Near),
the rounding toward +oo (represented by the constructor Up) and the
rounding toward -oo (represented by the constructor Down)
|
t [Numerors_utils.Sign] | |
t [Numerors_utils.Precisions] |
We handle the format defined in C.
|
t [Partitioning_index.Make] | |
t [Partition.MakeFlow] | |
t [Hashtbl.HashedType] |
The type of the hashtable keys.
|
t [Transfer_logic.LogicDomain] | |
t [Transfer_logic.ActiveBehaviors] | |
t [Powerset.S] | |
t [Simple_memory.S] | |
t [Traces_domain.Loops] | |
t [Traces_domain.GraphShape] | |
t [Abstract.Interface] | |
t [Structure.Internal] | |
t [Structure.External] | |
t [Eval.Valuation] | |
t [Alarmset] | |
t [Widen_hints_ext] | |
tank [Trace_partitioning.Make] |
The set of states that remains to propagate from a
control point.
|
transition [Traces_domain] | |
tree [Equality] | |
trivial [Equality] | |
truth [Abstract_location] | |
truth [Abstract_value] |
Type for the truth value of an assertion in a value abstraction.
|
U | |
unhashconsed_exprs [Hcexprs] | |
unroll_annotation [Eva_annotations] | |
unroll_limit [Partition] |
The unroll limit of a loop.
|
V | |
valuation [Abstract_domain] |
Results of an evaluation: the results of all intermediate calculation (the
value of each (sub)expression and the location of each lvalue) are available
to the domain.
|
valuation [Subdivided_evaluation.Forward_Evaluation] | |
value [Gui_types.S] | |
value [Abstract_domain.Transfer] | |
value [Abstract_domain.Queries] |
Numerical values to which the expressions are evaluated.
|
value [Abstract_location.S] | |
value [Analysis.Results] | |
value [Transfer_stmt.S] | |
value [Abstractions] |
Module types of value abstractions: either a single leaf module, or
a compound of several modules described by a structure.
|
value [Evaluation.S] |
Numeric values to which the expressions are evaluated.
|
value [Subdivided_evaluation.Forward_Evaluation] | |
value [Cvalue_transfer] | |
value [Simple_memory.S] | |
value [Eval.Valuation] |
Abstract value.
|
value [Parameter_sig.Map] |
Type of the values associated to the keys.
|
value [Parameter_sig.Multiple_map] | |
value_reduced_product [Abstractions] |
Reduced product between two value abstractions, identified by their keys.
|
variable_kind [Abstract_domain] | |
W | |
warn_mode [CilE] |
An argument of type
warn_mode can be supplied to some of the access
functions in Db.Value (the interface to the value analysis).
|
widening [Trace_partitioning.Make] |
Widening information
|
with_alarms [Eval] |
A type and a set of alarms.
|
with_info [Abstractions] |
Information about a registered abstraction.
|