Index of types

A
action [Mem_lvalue]
alarm_behavior [CilE]
C
cacheable [Value_types]
call_result [Value_types]	Results of a a call to a function
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.
code_transformation_category [File]	type of registered code transformations
cond [Eval_exprs]
cpp_opt_kind [File]	Whether a given preprocessor supports gcc options used in some configurations.
D
data [State_builder.Hashtbl]
data [State_builder.Ref]	Type of the referenced value.
E
eval_env [Eval_terms]	Evaluation environment.
eval_result [Eval_terms]
evaluation_functions [Gui_eval]	This is the record that encapsulates all evaluation functions
F
file [File]
filter [Gui_callstacks_filters]	Filters on callstacks.
found [Mem_lvalue]
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]
K
key [FCMap.S]	The type of the map keys.
key [Hashtbl.S]
key [State_builder.Hashtbl]
key [Parameter_sig.Map]	Type of keys of the map.
L
labels_states [Eval_terms]
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
merge [Per_stmt_slevel]
P
postcondition_kf_kind [Eval_annots]
pre_post_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.
R
rcallstack [Gui_callstacks_filters]	List.rev on a callstack, enforced by strong typing outside of this module
S
skip_change [Mem_lvalue]
slevel [Per_stmt_slevel]
split_strategy [Split_strategy]
state [Value_messages]
state_per_stmt [Value_results]
states_by_callstack [Gui_eval]	Maps from callstacks to Value states before and after a GUI location.
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 [Hashtbl.S]
t [Eval_annots.ActiveBehaviors]
t [Mem_lvalue.GraphDeps.V]
t [Mem_lvalue.GraphDeps]
t [Mem_lvalue.LatticeDirty]
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.
V
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).