Index of types


A
alloc_size [Builtins_nonfree_malloc]

C
call_site [Value_util]
A call_stack is a list, telling which function was called at which site.
callstack [Value_util]
clobbered_set [Locals_scoping]
Set of bases that might contain a reference to a local or formal variable.
cond [Eval_exprs]

D
data [Dataflow2.StmtStartData]
data [State_builder.Ref]
Type of the referenced value.
data [State_builder.Hashtbl]

E
elt [Value_perf.Imperative_callstack_trie]
eval_env [Eval_terms]
Evaluation environment.
eval_result [Eval_terms]

F
flat_perf_info [Value_perf]
formatting_result [Builtins_nonfree_deterministic]

K
key [Hashtbl.S]
key [State_builder.Hashtbl]

L
labels_states [Eval_terms]
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
lval_or_absolute [Register_gui]

O
offsetmap_result [Register_gui]

P
perf_info [Value_perf]
postcondition_kf_kind [Eval_annots]
pre_post_kind [Eval_annots]
precise_location [Precise_locs]
precise_location_bits [Precise_locs]
precise_offset [Precise_locs]
predicate_status [Eval_terms]
Evaluating a predicate.

R
record [Current_table]
State on one statement
reduce_rel_int_float [Eval_op]
return_usage [Split_return.ReturnUsage]
return_usage_by_lv [Split_return.ReturnUsage]
return_usage_per_fun [Split_return.ReturnUsage]

S
seen_percent [Builtins_nonfree_deterministic]
slevel [Per_stmt_slevel]
split_strategy [Split_strategy]
state_imp [Current_table]
The array of all the states associated to a statement.

T
t [Eval_slevel.Computer]
t [Per_stmt_slevel.G]
t [Eval_annots.ActiveBehaviors]
t [Current_table]
State for an entire function
t [State_imp]
t [State_set]
t [Hashtbl.S]
t [Value_perf.Imperative_callstack_trie]
t [Value_perf.Call_info]
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
u [Eval_slevel.Computer]

V
validity_hidden_base [Initial_state]

W
watch [Builtins_nonfree_watchpoint]
watchpoint [Builtins_nonfree_watchpoint]