Index of types

A
action [Hptset.S]
alarm [Alarmset]
alarm_behavior [CilE]
alarm_mode [Eval_terms]	Three modes to handle the alarms when evaluating a logical term.
argument [Eval]	Argument of a function call.
assigned [Eval]	Assigned values.
B
binop_context [Eval]	Context for the evaluation of a binary operator: contains the expressions of both operands and of the result, needed to create the appropriate alarms.
C
cacheable [Value_types]
call [Eval]	A function call.
call_action [Eval]	Action to perform on a call site.
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.
config [Abstractions]	Configuration of the abstract domain.
cvalue_valuation [Simpler_domains]	A simpler functional interface for valuations.
D
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]
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 [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.S]	This is the record that encapsulates all evaluation functions
expterm [Builtins_string]
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]
H
hashconsed_exprs [Hcexprs]	Hashconsed `hash_consed_exprs`
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_kind [Abstract_domain]
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
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 [State_builder.Hashtbl]
key [Parameter_sig.Map]	Type of keys of the map.
L
labels_states [Eval_terms]
left_value [Eval]
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 [Analysis.Results]
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_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
M
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_top_or_bottom [Eval]
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
precise_location [Precise_locs]
precise_location_bits [Precise_locs]
precise_offset [Precise_locs]
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.
results [Value_results]	Results
results [Value.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]
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 [Partitioning.S]
state [Transfer_stmt.S]
state [Evaluation.S]	State of abstract domain.
state [Subdivided_evaluation.Forward_Evaluation]
state [Transfer_logic.S]
state [Powerset.S]
state [Abstract_domain.Store]
state_set [Partitioning.S]
states [Transfer_logic.S]
status [Alarmset]
str_builtin_sig [Builtins_string]
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.
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 [Simpler_domains.Minimal]
t [Abstract_domain.Interface]
t [Abstract_domain.Valuation]
t [Partitioning.S]
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 [Structure.Internal]
t [Structure.External]
t [Eval.Valuation]
t [Alarmset]
t [Widen_hints_ext]
tree [Equality_sig]
trivial [Equality_sig]
U
unhashconsed_exprs [Hcexprs]
unop_context [Eval]	Context for the evaluation of an unary operator: contains the involved expressions needed to create the appropriate alarms.
V
valuation [Abstract_domain.Transfer]
valuation [Subdivided_evaluation.Forward_Evaluation]
value [Gui_types.S]
value [Abstract_domain.Transfer]
value [Abstract_domain.Valuation]	Abstract value.
value [Abstract_domain.Queries]	Numerical values to which the expressions are evaluated.
value [Abstract_location.S]
value [Analysis.Results]
value [Transfer_stmt.S]
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.
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).
with_alarms [Eval]	A type and a set of alarms.