Up
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
]