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.Hashtbl]
data [State_builder.Ref]
Type of the referenced value.
diff [Eval_slevel.Computer]
State propagated by the dataflow, that contains only 'new' states (i.e.

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

F
flat_perf_info [Value_perf]
formatting_result [Builtins_nonfree_deterministic]

I
imprecise_memset_reason [Builtins_nonfree]

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

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]
predicate_status [Eval_terms]
Evaluating a predicate.

R
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_per_stmt [Value_results]
stmt_state [Eval_slevel.Computer]
The real state for a given statement, used in particular to detect convergence.
syntactic_context [Valarms]

T
t [Eval_slevel.Computer.DataflowArg]
t [Eval_slevel.Computer]
t [Per_stmt_slevel.G]
t [Eval_annots.ActiveBehaviors]
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.

V
validity_hidden_base [Initial_state]

W
watch [Builtins_nonfree_watchpoint]
watchpoint [Builtins_nonfree_watchpoint]