A | |
action [Hptset.S] | |
action [Eval] |
Action to perform on a call site.
|
active_behaviors [Transfer_logic.S] | |
alarm [Alarmset] | |
alarm_behavior [CilE] | |
argument [Eval] | |
assigned [Eval] |
Assigned values.
|
atom [Equality_term] | |
B | |
binop_context [Eval] |
Evaluation of binary operator: e1 binop e2 = e3.
|
C | |
cacheable [Value_types] | |
call [Eval] | |
call_result [Value_types] |
Results of a a call to a function
|
call_result [Eval] | |
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_messages] | |
callstack [Value_util] | |
clobbered_set [Locals_scoping] |
Set of bases that might contain a reference to a local or formal
variable.
|
cond [Eval_exprs] | |
config [Abstractions] |
Configuration of the abstract domain.
|
copied [Eval] |
Copy of values.
|
D | |
data [State_builder.Hashtbl] | |
data [State_builder.Ref] |
Type of the referenced value.
|
E | |
element [Equality_sig.Set] |
The type of the equality elements.
|
elt [Equality_sig.S] |
The type of the equality elements.
|
eq [Structure] |
Equality witness between types.
|
equalities [Equality_domain.S] | |
equality [Equality_sig.Set] |
The type of the equalities.
|
eval_env [Abstract_domain.Logic] |
Evaluation environment.
|
eval_env [Eval_terms] |
Evaluation environment.
|
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] |
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 | |
fct_pointer_compatibility [Eval_typ] | |
filter [Gui_callstacks_filters] |
Filters on callstacks.
|
flagged_value [Eval] |
Right values with 'undefined' and 'escaping addresses' flags.
|
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] | |
I | |
if_consistent [Alarmset] | |
index_context [Eval] |
Evaluation of an index:
index, remaining, typ pointed, array size expression
|
init [Eval] |
Initialization of a dataflow analysis, by definig the initial value of
each statement.
|
internal_location [Domain_lift.Conversion] | |
internal_value [Domain_lift.Conversion] | |
internal_value [Location_lift.Conversion] | |
K | |
k [Structure.Key] | |
key [FCMap.S] |
The type of the map keys.
|
key [Abstract_domain] |
Keys identify abstract domains through the type of their abstract values.
|
key [Abstract_location] | |
key [Abstract_value] | |
key [Structure.External] | |
key [Hashtbl.S] | |
key [State_builder.Hashtbl] | |
key [Parameter_sig.Map] |
Type of keys of the map.
|
L | |
labels_states [Eval_terms] | |
left_value [Eval] | |
lmap [Lmap_bitwise.Location_map_bitwise] | |
loc [Abstract_domain.Valuation] |
Abstract memory location.
|
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 [Cvalue_transfer] | |
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_evaluation_error [Eval_terms] |
Error during the evaluation of a term or a predicate
|
M | |
map [Lmap_bitwise.Location_map_bitwise] | |
merge [Per_stmt_slevel] | |
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_void [Equality_sig] | |
origin [Abstract_domain.Valuation] |
Origin of abstract values.
|
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 [Eval.Valuation] |
Origin of values.
|
P | |
p_kind [Eval_annots] | |
postcondition_kf_kind [Eval_annots] | |
precise_location [Precise_locs] | |
precise_location_bits [Precise_locs] | |
precise_offset [Precise_locs] | |
precision_loss_message [Value_messages] | |
predicate_status [Eval_terms] |
Evaluating a predicate.
|
prefix [Cvalue_domain] | |
R | |
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.
|
res [Transfer_stmt.S] | |
results [Value_results] |
Results
|
results [Value.Value_results] | |
return [Eval] | |
S | |
s [Alarmset] | |
shape [Hptset.S] |
Shape of the set, ie.
|
slevel [Per_stmt_slevel] | |
split_strategy [Split_strategy] | |
state [Abstract_domain.S] | |
state [Abstract_domain.Logic] | |
state [Abstract_domain.Transfer] | |
state [Abstract_domain.Queries] |
Domain state.
|
state [Abstract_domain.Lattice] | |
state [Initialization.S] | |
state [Partitioning.Partition] | |
state [Partitioning.StateSet] | |
state [Transfer_stmt.S] | |
state [Transfer_logic.S] | |
state [Evaluation.S] |
State of abstract domain.
|
state [Value_messages] | |
state_per_stmt [Value_results] | |
state_set [Partitioning.Partition] | |
states [Transfer_logic.S] | |
states_by_callstack [Gui_eval] |
Maps from callstacks to Value states before and after a GUI location.
|
status [Alarmset] | |
structure [Abstract_domain] |
Describes the internal structure of a domain.
|
structure [Abstract_location] | |
structure [Abstract_value] | |
structure [Structure.Internal] | |
structure [Structure.Shape] |
The gadt, based on keys giving the type of each node.
|
summary [Abstract_domain.S] |
Summary of the analysis of a function.
|
summary [Abstract_domain.Transfer] | |
summary [Mem_exec2.Domain] | |
summary [Transfer_stmt.S] | |
syntactic_context [Valarms] | |
T | |
t [FCMap.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 [Abstract_domain.Valuation] | |
t [Partitioning.Partition] | |
t [Partitioning.StateSet] | |
t [Hashtbl.HashedType] |
The type of the hashtable keys.
|
t [Structure.Internal] | |
t [Structure.External] | |
t [Eval.Valuation] | |
t [Alarmset] | |
t [Hashtbl.S] | |
t [Eval_annots.ActiveBehaviors] | |
t [State_imp] | |
t [State_set] | |
topify_offsetmap [Locals_scoping] |
Type of a function that topifies the references to a local in an offsetmap.
|
topify_offsetmap_approx [Locals_scoping] |
Type of a function that partially topifies the references to a local in
an offsetmap.
|
topify_state [Locals_scoping] |
Type of a function that topifies a state.
|
U | |
unop_context [Eval] |
Evaluation of unary operator: unop e1 = e2.
|
V | |
v [Lmap_bitwise.Location_map_bitwise] | |
valuation [Abstract_domain.Transfer] | |
value [Abstract_domain.Valuation] |
Abstract value.
|
value [Abstract_domain.Transfer] | |
value [Abstract_domain.Queries] |
Numerical values to which the expressions are evaluated.
|
value [Abstract_location.S] | |
value [Transfer_stmt.S] | |
value [Evaluation.S] |
Numeric values to which the expressions are evaluated.
|
value [Cvalue_transfer] | |
value [Eval.Valuation] |
Abstract value.
|
value [Parameter_sig.Map] |
Type of the values associated to the keys.
|
value_message [Value_messages] | |
W | |
warn_mode [CilE] |
An argument of type
warn_mode is required by some of the access
functions in Db.Value (the interface to the value analysis).
|
warning [Value_messages] |
Warnings can either emit ACSL (Alarm), or do not emit ACSL
(others).
|
with_alarms [Eval] |
A type and a set of alarms.
|