A | |
abstraction [Abstractions] | Abstraction to be registered. |
action [Partition] | These actions redefine the partitioning by updating keys or spliting states. |
action [Hptset.S] | |
address [Results] | |
address [Eva.Results] | |
alarm [Alarmset] | |
alarm_behavior [CilE] | |
alarm_category [Summary] | |
alarm_mode [Eval_terms] | Three modes to handle the alarms when evaluating a logical term. |
alarm_or_property [Red_statuses] | |
alarms [Summary] | |
allocation_kind [Eva_annotations] | |
allocation_kind [Eva.Eva_annotations] | |
analysis_status [Function_calls] | |
analysis_target [Function_calls] | What is used for the analysis of a given function: a Cvalue builtin (and other domains use the specification), the function specification, the function body. The boolean indicates whether the resulting states must be recorded at each statement of this function. |
argument [Eval] | Argument of a function call. |
array_segmentation [Eva_annotations] | |
array_segmentation [Eva.Eva_annotations] | |
assigned [Eval] | Assigned values. |
B | |
bioracle [Abstract_memory] | |
bit [Abstract_memory] | |
bound [Abstract_value] | |
bound [Segmentation.Segmentation] | |
bound_kind [Abstract_value] | |
branch [Partition] | Junction branch id in the control flow |
builtin [Builtins] | Type of a cvalue builtin, whose arguments are: the memory state at the beginning of the function call;, the list of arguments of the function call. |
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). |
builtin [Eva.Builtins] | Type of a cvalue builtin, whose arguments are: the memory state at the beginning of the function call;, the list of arguments of the function call. |
builtin_type [Builtins] | |
builtin_type [Eva.Builtins] | |
C | |
cacheable [Builtins] | Can the results of a builtin be cached? See for more details. |
cacheable [Eval] | Can the results of a function call be cached with memexec? |
cacheable [Eva.Builtins] | Can the results of a builtin be cached? See for more details. |
cacheable [Eva.Eval] | Can the results of a function call be cached with memexec? |
call [Builtins] | |
call [Eval] | A function call. |
call_froms [Value_types] | If not None, the froms of the function, and its sure outputs; i.e. |
call_init_state [Equality_domain] | |
call_result [Transfer_stmt.S] | |
call_result [Builtins] | The result of a builtin can be given in different forms. |
call_result [Eva.Builtins] | The result of a builtin can be given in different forms. |
call_return_policy [Partition] | |
call_site [Value_types] | Value call-site. |
call_site [Eval] | A call site: the function called, and the call statement
(or |
callback_result [Value_types] | |
callstack [Value_types] | Value callstacks, as used e.g. |
callstack [Results] | |
callstack [Eval] | |
callstack [Eva.Results] | |
clobbered_set [Locals_scoping] | Set of bases that might contain a reference to a local or formal variable. |
computation_state [Analysis] | |
computation_state [Self] | Computation state of the analysis. |
computation_state [Eva.Analysis] | |
context [Subdivided_evaluation.Forward_Evaluation] | |
coverage [Summary] | |
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 |
domain_scope [Eva_annotations] | |
domain_scope [Eva.Eva_annotations] | |
E | |
edge [Traces_domain] | |
elt [Equality] | The type of the equality elements. |
eq [Structure] | Equality witness between types. |
equality [Equality] | |
error [Results] | |
error [Eva.Results] | |
eval_env [Eval_terms] | Evaluation environment. |
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 [Results] | |
evaluation [Eva.Results] | |
evaluation_context [Abstract_domain] | Context from the engine evaluation about a domain query. |
evaluation_functions [Gui_eval.S] | This is the record that encapsulates all evaluation functions |
events [Summary] | |
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] | Split/merge annotations for value partitioning. |
flow_annotation [Eva.Eva_annotations] | Split/merge annotations for value partitioning. |
formatter [Pretty_memory] | |
full_result [Builtins] | |
full_result [Eva.Builtins] | |
fun_stats [Summary] | |
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] | |
index [Multidim] | |
init_value [Abstract_domain] | Value for the initialization of variables. |
initialization [Abstract_memory] | |
integer_range [Eval_typ] | Abstraction of an integer type, more convenient than an |
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 |
L | |
labels_states [Eval_terms] | |
left_value [Eval] | Lvalue with its location and type. |
loc [Transfer_stmt.S] | |
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 [Typed_memory.Make] | |
location [Analysis.Results] | |
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_dependency [Eval] | The logic dependency of an ACSL assigns clause. |
logic_deps [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 | |
map [Hptset.S] | |
merge [Per_stmt_slevel] | |
mode [Domain_mode] | Mode for the analysis of a function |
N | |
node [Traces_domain] | |
O | |
offset [Abstract_location.S] | abstract offsets |
offsm_or_top [Offsm_value] | |
oracle [Abstract_memory] | |
origin [Abstract_domain.Transfer] | |
origin [Abstract_domain.Queries] | The |
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_location [Precise_locs] | |
precise_location_bits [Precise_locs] | |
precise_offset [Precise_locs] | |
predicate_status [Eval_terms] | Evaluating a predicate. |
prefix [Cvalue_domain] | |
program_stats [Summary] | |
R | |
rationing [Partition] | Rationing are used to keep separate the |
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. |
recursion [Eval] | Information needed to interpret a recursive call. |
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. |
request [Results] | |
request [Eva.Results] | |
result [Results] | |
result [Builtins] | |
result [Eva.Results] | |
results [Eva_results] | |
results [Analysis] | Kind of results for the analysis of a function body. |
results [Function_calls] | |
results [Eva.Eva_results] | |
results [Eva.Analysis] | Kind of results for the analysis of a function body. |
S | |
s [Alarmset] | |
scalar_typ [Eval_typ] | Abstraction of scalar types -- in particular, all those that can be involved in a cast. |
sformat [Pretty_memory] | |
side [Abstract_memory] | |
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. |
size [Abstract_memory] | |
slevel [Per_stmt_slevel] | |
slevel_annotation [Eva_annotations] | Annotations tweaking the behavior of the -eva-slevel parameter. |
slevel_annotation [Eva.Eva_annotations] | Annotations tweaking the behavior of the -eva-slevel parameter. |
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_kind [Eva_annotations] | |
split_kind [Eva.Eva_annotations] | |
split_monitor [Partition] | Split monitor: prevents splits from generating too many states. |
split_strategy [Split_strategy] | |
split_term [Partition] | Splits can be performed according to a C expression or an ACSL predicate. |
split_term [Eva_annotations] | |
split_term [Eva.Eva_annotations] | |
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 [Transfer_stmt.S] | |
state [Transfer_logic.S] | |
state [Evaluation.S] | State of abstract domain. |
state [Trace_partitioning.Make] | The states being partitioned |
state [Partition.MakeFlow] | |
state [Powerset.S] | |
state [Traces_domain] | |
states [Transfer_logic.S] | |
status [Analysis] | |
status [Alarmset] | |
status [Eva.Analysis] | |
statuses [Summary] | |
store [Trace_partitioning.Make] | The storage of all states ever met at a control point |
str_builtin_sig [Builtins_string] | |
structure [Abstract_structure.Disjunction] | |
structure [Structure.Internal] | |
structure [Structure.Shape] | The gadt, based on keys giving the type of each node. |
submemory [Segmentation.Segmentation] | |
submemory [Abstract_structure.Disjunction] | |
submemory [Abstract_structure.Structure] | |
T | |
t [Map.S] | The type of maps from type |
t [Cvalue.V_Or_Uninitialized] | Semantics of the constructors: |
t [Cvalue.CardinalEstimate] | |
t [Simpler_domains.Minimal] | |
t [Abstract_domain.Reuse] | Type of states. |
t [Typed_memory.Value] | |
t [Typed_memory.Make] | |
t [Segmentation.Segmentation] | |
t [Segmentation.Bound] | |
t [Abstract_structure.Disjunction] | |
t [Abstract_structure.Structure] | |
t [Abstract_memory.ProtoMemory] | |
t [Abstract_memory.Bit] | |
t [Abstract_offset] | |
t [Transfer_logic.LogicDomain] | |
t [Function_calls] | |
t [Partitioning_index.Make] | |
t [Partition.MakeFlow] | |
t [Powerset.S] | |
t [Equality_domain] | |
t [Simple_memory.S] | |
t [Traces_domain.Loops] | |
t [Traces_domain.GraphShape] | |
t [Domain_builder.LeafDomain] | |
t [Domain_store.S] | |
t [Abstract.Interface] | |
t [Structure.Internal] | |
t [Structure.External] | |
t [Eval.Valuation] | |
t [Alarmset] | |
t [Widen_hints_ext] | |
t [Active_behaviors] | |
taint_error [Taint_domain] | |
taint_ok [Taint_domain] | |
taint_result [Taint_domain] | |
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] | Loop unroll 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 [Results] | |
value [Typed_memory.Make] | |
value [Abstract_memory.ProtoMemory] | |
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 [Eva.Results] | |
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 |
widening [Trace_partitioning.Make] | Widening information |
with_alarms [Eval] | A type and a set of alarms. |
with_info [Abstractions] | Information about a registered abstraction. |