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