Index of types

A
abstraction [Abstractions]

Abstraction to be registered.

action [Partition]

These actions redefine the partitioning by updating keys or spliting states.

action [Hptset.S]
alarm [Alarmset]
alarm_behavior [CilE]
alarm_mode [Eval_terms]

Three modes to handle the alarms when evaluating a logical term.

alarm_or_property [Red_statuses]
allocation_kind [Eva_annotations]
argument [Eval]

Argument of a function call.

assigned [Eval]

Assigned values.

B
bound [Abstract_value]
bound_kind [Abstract_value]
branch [Partition]

Junction branch id in the control flow

builtin [Builtins]
builtin [Simple_memory]

A builtin is an ocaml function for the interpretation of a whole C function: it takes the list of value arguments, and returns the result (that can be bottom).

C
cacheable [Value_types]
call [Builtins]
call [Eval]

A function call.

call_init_state [Equality_domain]
call_result [Value_types]

Results of a a call to a function

call_result [Transfer_stmt.S]
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_util]
clobbered_set [Locals_scoping]

Set of bases that might contain a reference to a local or formal variable.

context [Subdivided_evaluation.Forward_Evaluation]
cvalue [Simpler_domains]
cvalue_valuation [Simpler_domains]

A simpler functional interface for valuations.

D
data [Structure.Shape]
data [State_builder.Hashtbl]
data [State_builder.Ref]

Type of the referenced value.

data_by_callstack [Gui_callstacks_manager]
display_data_by_callstack [Gui_callstacks_manager]
domain [Abstractions]

Type of domain to be registered: either a leaf module with 'v as value abstraction, or a functor building a domain from any value abstraction.

E
edge [Traces_domain]
elt [Equality]

The type of the equality elements.

eq [Structure]

Equality witness between types.

equalities [Equality_domain.Make]
equality [Equality]
eval_env [Eval_terms]

Evaluation environment.

eval_env [Eva.Eval_terms]

Evaluation environment, built by env_annot.

eval_result [Eval_terms]
evaluated [Eval]

Most forward evaluation functions return the set of alarms resulting from the operations, and a result which can be `Bottom, if the evaluation fails, or the expected value.

evaluation_functions [Gui_eval.S]

This is the record that encapsulates all evaluation functions

extended_location [Domain_lift.Conversion]
extended_value [Domain_lift.Conversion]
extended_value [Location_lift.Conversion]
F
filter [Gui_callstacks_filters]

Filters on callstacks.

flag [Abstractions]

Flag for an abstract domain.

flagged_value [Eval]

Right values with 'undefined' and 'escaping addresses' flags.

flow [Trace_partitioning.Make]

A set of states which are currently propagated

flow_annotation [Eva_annotations]
flow_annotation [Eva.Eva_annotations]

Split/merge annotations for value partitioning.

forward [Numerors_arithmetics.Arithmetic]
function_mode [Domain_mode]

A function associated with an analysis mode.

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]
H
hint_lval [Widen_hints_ext]

Type of widening hints: a special kind of lval for which the hints will apply and a list of names (e.g.

hint_vars [Widen_hints_ext]
I
if_consistent [Alarmset]
init_value [Abstract_domain]

Value for the initialization of variables.

integer_range [Eval_typ]

Abstraction of an integer type, more convenient than an ikind because it can also be used for bitfields.

internal_location [Domain_lift.Conversion]
internal_value [Domain_lift.Conversion]
internal_value [Location_lift.Conversion]
K
key [Map.S]

The type of the map keys.

key [Abstract_domain]
key [Abstract_location]
key [Abstract_value]
key [Partition]

Partitioning keys attached to states.

key [Abstract.Interface]
key [Structure.External]
key [Structure.Key]
key [State_builder.Hashtbl]
key [Parameter_sig.Map]

Type of keys of the map.

key [Parameter_sig.Multiple_map]
key [Parameter_sig.Multiple_value_datatype]
kill_type [Hcexprs]

Reason of the replacement of an lvalue lval: Modified means that the value of lval has been modified (in which case &lval is unchanged), and Deleted means that lval is no longer in scope (in which case &lval raises the NonExchangeable error).

L
labels_states [Eval_terms]
labels_states [Eva.Eval_terms]
left_value [Eval]

Lvalue with its location and type.

loc [Evaluation.S]

Location of an lvalue.

loc [Eval.Valuation]

Abstract memory location.

location [Abstract_domain.Transfer]
location [Abstract_domain.Queries]

Abstract memory locations associated to left values.

location [Abstract_location.S]

abstract locations

location [Analysis.Results]
location [Transfer_stmt.S]
location [Cvalue_transfer]
logic_assign [Eval]
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_deps [Eva.Eval_terms]

Dependencies needed to evaluate a term or a predicate.

logic_environment [Abstract_domain]

Environment for the logical evaluation of predicates.

logic_evaluation_error [Eval_terms]

Error during the evaluation of a term or a predicate

loops [Traces_domain]

stack of open loops

lvalues [Hcexprs]
M
merge [Per_stmt_slevel]
mode [Domain_mode]

Mode for the analysis of a function f: current is the read/write permission for f., calls is the read/write permission for all functions called from f.

N
node [Traces_domain]
O
offset [Abstract_location.S]

abstract offsets

offsm_or_top [Offsm_value]
or_top [Eval]

For some functions, the special value top (denoting no information) is managed separately.

or_top_or_bottom [Eval]
origin [Abstract_domain.Transfer]
origin [Abstract_domain.Queries]

The origin is used by the domain combiners to track the origin of a value.

origin [Evaluation.S]

Origin of values.

origin [Cvalue_transfer]
origin [Eval.Valuation]

Origin of values.

P
partition [Partition]

Collection of states, each identified by a unique key.

permission [Domain_mode]

Permission for an abstract domain to read/write its state.

pointer_comparison [Abstract_value]
precise_loc [Simpler_domains]
precise_loc [Abstractions]

For the moment, all domains must use precise_loc as their location abstraction, and no new location abstraction can be registered for an analysis.

precise_location [Precise_locs]
precise_location_bits [Precise_locs]
precise_offset [Precise_locs]
predicate_status [Eval_terms]

Evaluating a predicate.

prefix [Cvalue_domain]
R
rationing [Partition]

Rationing are used to keep separate the n first states propagated at a point, by creating unique stamp until the limit is reached.

rcallstack [Gui_callstacks_filters]

List.rev on a callstack, enforced by strong typing outside of this module

record_loc [Eval]

Data record associated to each evaluated left-value.

record_val [Eval]

Data record associated to each evaluated expression.

reduced [Eval]

Most backward evaluation function returns `Bottom if the reduction leads to an invalid state, `Unreduced if no reduction can be performed, or the reduced value.

reductness [Eval]

State of reduction of an abstract value.

result [Builtins]
results [Value_results]

Results

results [Eva.Value_results]
S
s [Alarmset]
scalar_typ [Eval_typ]

Abstraction of scalar types -- in particular, all those that can be involved in a cast.

shape [Hptset.S]

Shape of the set, ie.

signs [Sign_value]
simple_argument [Simpler_domains]

Both the formal argument of a called function and the concrete argument at a call site.

simple_call [Simpler_domains]

Simple information about a function call.

slevel [Per_stmt_slevel]
slevel_annotation [Eva_annotations]
slevel_annotation [Eva.Eva_annotations]

Annotations tweaking the behavior of the -eva-slevel paramter.

split_kind [Partition]

Splits on an expression can be static or dynamic: static splits are processed once: the expression is only evaluated at the split point, and the key is then kept unchanged until a merge., dynamic splits are regularly redone: the expression is re-evaluated, and states are then split or merged accordingly.

split_monitor [Partition]

Split monitor: prevents splits from generating too many states.

split_strategy [Split_strategy]
state [Abstract_domain.S]
state [Abstract_domain.Transfer]
state [Abstract_domain.Queries]

Domain state.

state [Abstract_domain.Lattice]
state [Analysis.Results]
state [Initialization.S]
state [Trace_partitioning.Make]

The states being partitioned

state [Partition.MakeFlow]
state [Transfer_stmt.S]
state [Evaluation.S]

State of abstract domain.

state [Transfer_logic.S]
state [Powerset.S]
state [Traces_domain]
state [Abstract_domain.Store]
states [Transfer_logic.S]
status [Alarmset]
store [Trace_partitioning.Make]

The storage of all states ever met at a control point

str_builtin_sig [Builtins_string]
structure [Structure.Internal]
structure [Structure.Shape]

The gadt, based on keys giving the type of each node.

T
t [Map.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 [Simpler_domains.Minimal]
t [Abstract_domain.Reuse]

Type of states.

t [Numerors_arithmetics]

Type manipulated by the arithmetics

t [Numerors_interval]

Opaque type of an interval.

t [Numerors_float]
t [Numerors_utils.Mode]

Those constructors corresponds to the possible values of the option -eva-numerors-mode

t [Numerors_utils.Rounding]

We only use the rounding to nearest (represented by the constructor Near), the rounding toward +oo (represented by the constructor Up) and the rounding toward -oo (represented by the constructor Down)

t [Numerors_utils.Sign]
t [Numerors_utils.Precisions]

We handle the format defined in C.

t [Partitioning_index.Make]
t [Partition.MakeFlow]
t [Transfer_logic.LogicDomain]
t [Transfer_logic.ActiveBehaviors]
t [Powerset.S]
t [Simple_memory.S]
t [Traces_domain.Loops]
t [Traces_domain.GraphShape]
t [Abstract.Interface]
t [Structure.Internal]
t [Structure.External]
t [Eval.Valuation]
t [Alarmset]
t [Widen_hints_ext]
tank [Trace_partitioning.Make]

The set of states that remains to propagate from a control point.

transition [Traces_domain]
tree [Equality]
trivial [Equality]
truth [Abstract_location]
truth [Abstract_value]

Type for the truth value of an assertion in a value abstraction.

U
unhashconsed_exprs [Hcexprs]
unroll_annotation [Eva_annotations]
unroll_annotation [Eva.Eva_annotations]

Loop unroll annotations.

unroll_limit [Partition]

The unroll limit of a loop.

V
valuation [Abstract_domain]

Results of an evaluation: the results of all intermediate calculation (the value of each (sub)expression and the location of each lvalue) are available to the domain.

valuation [Subdivided_evaluation.Forward_Evaluation]
value [Gui_types.S]
value [Abstract_domain.Transfer]
value [Abstract_domain.Queries]

Numerical values to which the expressions are evaluated.

value [Abstract_location.S]
value [Analysis.Results]
value [Transfer_stmt.S]
value [Abstractions]

Module types of value abstractions: either a single leaf module, or a compound of several modules described by a structure.

value [Evaluation.S]

Numeric values to which the expressions are evaluated.

value [Subdivided_evaluation.Forward_Evaluation]
value [Cvalue_transfer]
value [Simple_memory.S]
value [Eval.Valuation]

Abstract value.

value [Parameter_sig.Map]

Type of the values associated to the keys.

value [Parameter_sig.Multiple_map]
value_reduced_product [Abstractions]

Reduced product between two value abstractions, identified by their keys.

variable_kind [Abstract_domain]
W
warn_mode [CilE]

An argument of type warn_mode can be supplied to some of the access functions in Db.Value (the interface to the value analysis).

widening [Trace_partitioning.Make]

Widening information

with_alarms [Eval]

A type and a set of alarms.

with_info [Abstractions]

Information about a registered abstraction.