Index of values


(>>=) [Eval]
This monad propagates the `Bottom value if needed, and join the alarms of each evaluation.
(>>=.) [Eval]
Use this monad of the following function returns no alarms.
(>>=:) [Eval]
Use this monad if the following function returns a simple value.
_join [Gauges_domain.G.Gauge]

A
a_ignore [CilE]
active [Eval_annots.ActiveBehaviors]
active_behaviors [Eval_annots.ActiveBehaviors]
actualize_formals [Function_args]
add [FCMap.S]
add x y m returns a map containing the same bindings as m, plus a binding of x to y.
add [Equality_sig.S]
add x s returns the equality between all elements of s and x.
add [Partitioning.StateSet]
add [Equality_sig.Set]
add [Hcexprs.BaseToHCESet]
add [Hcexprs.HCEToZone]
add [Gauges_domain.G.Gauge]
add [Gauges_domain.G.Bounds]
add [Eval.Valuation]
add [Alarmset]
! Different semantics according to the kind of alarms map.
add [Hashtbl.S]
add [State_builder.Hashtbl]
Add a new binding.
add [State_set]
Adding elements
add' [Partitioning.StateSet]
add' [Alarmset]
add_binding [Cvalue.Model]
add_binding state loc v simulates the effect of writing v at location loc in state.
add_binding [Eval_op]
Temporary.
add_binding_unspecified [Cvalue.Model]
add_binding_unspecified [Eval_op]
Temporary.
add_initial_binding [Cvalue.Model]
add_kf_caller [Value_results]
add_new_base [Cvalue.Model]
add_statement [State_set]
Update the trace of all the states in the stateset.
add_unsafe_binding [Cvalue.Model]
add_untyped [Cvalue.V]
add_untyped ~factor e1 e2 computes e1+factor*e2 using C semantic for +, i.e.
add_untyped_under [Cvalue.V]
Under-approximating variant of Cvalue.V.add_untyped.
alarm_report [Value_util]
Emit an alarm, either as warning or as a result, according to option AlarmsWarnings.
all [Alarmset]
all alarms: all potential assertions have a Dont_know status.
all_values [Cvalue.V]
all_values ~size v returns true iff v contains all integer values representable in size bits.
all_vars_str [Widen_hints_ext]
String used for hints applying to all variables.
apply [Value_messages.Value_Message_Callback]
apply_on_all_locs [Eval_op]
apply_all_locs f loc state folds f on all the atomic locations in loc, provided there are less than plevel.
are_comparable [Cvalue_forward]
are_comparable [Warn]
assign [Abstract_domain.Transfer]
assign kinstr lv expr v valuation state is the transfer function for the assignment lv = expr for state.
assign [Transfer_stmt.S]
assign [Gauges_domain.D_Impl.Transfer]
assign [Gauges_domain.G]
assign_return [Abstract_domain.Transfer]
assign_return stmt lv kf return value valuation state models on states the effect of the assignment of the return value of a called function at the call site.
assign_return [Gauges_domain.D_Impl.Transfer]
assume [Abstract_domain.Transfer]
Transfer function for an assumption.
assume [Transfer_stmt.S]
assume [Evaluation.S]
assume ~valuation state expr value assumes in the valuation that the expression expr has the value value in the state state, and backward propagates this information to the subterm of expr.
assume [Gauges_domain.D_Impl.Transfer]

B
backward_binop [Abstract_value.S]
Backward evaluation of the binary operation left binop right = result; tries to reduce the argument left and right according to result.
backward_binop [Cvalue_backward]
This function tries to reduce the argument values of a binary operation, given its result.
backward_cast [Abstract_value.S]
Backward evaluation of the cast of the value src_val of type src_typ into the value dst_val of type dst_typ.
backward_cast [Cvalue_backward]
This function tries to reduce the argument of a cast, given the result of the cast.
backward_comp_float_left [Cvalue.V]
backward_comp_int_left [Cvalue.V]
backward_comp_left_from_type [Eval_op]
Reduction of a Cvalue.V.t by ==, !=, >=, >, <= and <.
backward_field [Abstract_location.S]
backward_index [Abstract_location.S]
backward_location [Abstract_domain.Queries]
backward_location state lval typ loc v reduces the location loc of the lvalue lval of type typ, so that only the locations that may have value v are kept.
backward_location [Gauges_domain.D_Impl]
backward_loop [Gauges_domain.G]
backward_mult_int_left [Cvalue.V]
backward_nb [Gauges_domain.G.Bounds]
backward_pointer [Abstract_location.S]
backward_unop [Abstract_value.S]
Backward evaluation of the unary operation unop arg = res; tries to reduce the argument arg according to res.
backward_unop [Cvalue_backward]
This function tries to reduce the argument value of an unary operation, given its result.
backward_variable [Abstract_location.S]
behavior_from_name [Eval_annots.ActiveBehaviors]
behavior_inactive [Eval_annots]
bind_block_locals [Value_util]
Bind all locals of the block to their default value (namely UNINITIALIZED)
bindings [FCMap.S]
Return the list of all bindings of the given map.
bitfield_size [Eval_typ]
bitwise_and [Cvalue.V]
bitwise_not [Cvalue.V]
bitwise_not_size [Cvalue.V]
bitwise_or [Cvalue.V]
bitwise_xor [Cvalue.V]
block_top_addresses_of_locals [Locals_scoping]
Return a function that topifies all references to the variables local to the given blocks.
bottom [Locals_scoping]
bottom_location_bits [Precise_locs]
box_key [Apron_domain]

C
c_labels [Eval_annots]
c_rem [Cvalue.V]
cache_name [Gauges_domain.G]
call [Transfer_stmt.S]
call_stack [Value_util]
callsite_matches [Gui_callstacks_filters]
callstack_matches [Gui_callstacks_filters]
callstacks_at_gui_loc [Gui_eval]
For statements: results are available only if the statement is reachable.
cardinal [FCMap.S]
Return the number of bindings of a map.
cardinal [Equality_sig.S]
Return the number of elements of the equality.
cardinal [Equality_sig.Set]
cardinal_estimate [Cvalue.Model]
cardinal_zero_or_one [Precise_locs]
Should not be used, Precise_locs.valid_cardinal_zero_or_one is almost always more useful
cast [Cvalue.V]
cast ~size ~signed v applies to the abstract value v the conversion to the integer type described by size and signed.
cast [Offsm_value]
cast_double [Cvalue.V]
cast_float [Cvalue.V]
cast_float_to_int [Cvalue.V]
cast_float_to_int_inverse [Cvalue.V]
cast_int_to_float [Cvalue.V]
cast_int_to_float_inverse [Cvalue.V]
cast_lval_if_bitfield [Eval_typ]
if needed, cast the given abstract value to the given size.
change_callstacks [Value_results]
Change the callstacks for the results for which this is meaningful.
change_callstacks [Value.Value_results]
check_arg_size [Function_args]
check_copy_lval [Evaluation.S]
check_fct_assigns [Eval_annots]
check_fct_postconditions [Transfer_logic.S]
check_fct_postconditions [Eval_annots]
Check the postcondition of kf for every behavior, treating them separately if per_behavior is true, merging them otherwise.
check_fct_postconditions_default_behavior [Eval_annots]
check_fct_postconditions_for_behavior [Eval_annots]
Checks the postconditions of b and of the default behavior if it is not b
check_fct_postconditions_of_behavior [Eval_annots]
Check the postcondition of kf for a given behavior b.
check_fct_preconditions [Transfer_logic.S]
check_fct_preconditions [Eval_annots]
check_fct_preconditions_for_behavior [Eval_annots]
Check the precondition of kf for a given behavior b.
check_from [Eval_annots]
Compute the validity status for from in pre_state, assuming the entire clause is assigns asgn \from from.
check_no_recursive_call [Warn]
check_non_overlapping [Abstract_location.S]
Needed for unspecified sequences.
check_non_overlapping [Evaluation.S]
check_non_overlapping [Eval_stmt]
check_unspecified_sequence [Transfer_stmt.S]
check_unspecified_sequence [Eval_stmt]
choose [FCMap.S]
Return one binding of the given map, or raise Not_found if the map is empty.
choose [Equality_sig.S]
Return the representative of the equality.
choose [Equality_sig.Set]
classify_as_scalar [Eval_typ]
classify_pre_post [Gui_eval]
State in which the predicate, found in the given function, should be evaluated
classify_sign [Gauges_domain.G.Bounds]
cleanup_results [Mem_exec2]
Clean all previously stored results
cleanup_results [Mem_exec]
Clean all previously stored results
clear [Hashtbl.S]
clear [State_builder.Hashtbl]
Clear the table.
clear [Stop_at_nth]
clear [State_builder.Ref]
Reset the reference to its default value.
clear_caches [Hptset.S]
Clear all the caches used internally by the functions of this module.
clear_call_stack [Value_util]
Functions dealing with call stacks.
clear_englobing_exprs [Eval.Clear_Valuation]
Removes from the valuation all the subexpressions of expr that contain subexpr, except subexpr itself.
clobbered_set_from_ret [Builtins]
clobbered_set_from_ret state ret can be used for functions that return a pointer to where they have written some data.
code_annotation_loc [Eval_annots]
code_annotation_text [Eval_annots]
combine_base_precise_offset [Precise_locs]
combine_loc_precise_offset [Precise_locs]
compare [FCMap.S]
Total ordering between maps.
compare [Equality_sig.S]
compare [Equality_sig.Set]
compare [Gauges_domain.G.MultipleIterations]
compare [Structure.Key]
compare_gui_callstack [Gui_types]
compare_max_float [Cvalue.V]
compare_max_int [Cvalue.V]
compare_min_float [Cvalue.V]
compare_min_int [Cvalue.V]
compatible_functions [Eval_typ]
Test that two functions types are compatible; used to verify that a call through a function pointer is ok.
compatible_functions [Value_util]
compute [Analysis.Make]
compute [Analysis]
Perform a full analysis, starting from the given kernel_function and with the abstractions specified by the configuration.
compute [Partitioned_dataflow.Computer]
compute [Eval_slevel.Computer]
compute_actual [Function_args]
compute_call_ref [Transfer_stmt.S]
compute_call_ref [Eval_stmt]
compute_from_entry_point [Compute_functions.Make]
compute_non_linear [Eval_non_linear]
compute_using_specification [Abstract_domain.S]
compute_using_specification [Gauges_domain.D_Impl]
compute_using_specification [Eval_behaviors]
Evaluate kf in state with_formals, first by reducing by the preconditions, then by evaluating the assigns, then by reducing by the post-conditions.
configure [Abstractions]
Build a configuration according to the analysis paramaters.
constant [Abstract_value.S]
Returns the abstract value of a litteral constants, and potentially some alarms in case of floating point constants overflow.
contains [Equality_sig.Set]
contains elt set = true iff elt belongs to an equality of set.
contains_c_at [Eval_annots]
contains_non_zero [Cvalue.V]
contains_single_elt [Hptset.S]
contains_zero [Cvalue.V]
conv_comp [Value_util]
conv_relation [Value_util]
conv_status [Eval_annots]
copy [Hashtbl.S]
copy [Datatype.S]
Deep copy: no possible sharing between x and copy x.
copy_lvalue [Evaluation.S]
Computes the value of a lvalue, with possible indeterminateness: the returned value may be uninitialized, or contain escaping addresses.
copy_offsetmap [Eval_op]
Tempory.
create [Transfer_logic.S]
create [Hashtbl.S]
create [Eval_annots.ActiveBehaviors]
create_all_values [Cvalue.V]
create_alloced_return [Library_functions]
create_from_spec [Eval_annots.ActiveBehaviors]
create_key [Structure.Key]
create_new_var [Value_util]
Create and register a new variable inside Frama-C.
ct [Gauges_domain.G.Gauge]
current [Analysis]
The abstractions used in the latest analysis, and its results.
current_kf [Value_util]
The current function is the one on top of the call stack.
current_kf_inout [Transfer_stmt]
current_stmt [Alarmset]
current_stmt [Valarms]
curstate [Value_messages]
cvalue_initial_state [Analysis]
Compute the initial state of the cvalue domain only.
cvalue_key [Main_values]
Key for cvalues.

D
debug_result [Value_util]
deep_fold [Equality_sig.Set]
default [Widen_type]
A default set of hints
default_alarm_report [Value_messages]
default_call [Abstract_domain.Transfer]
default_call [Gauges_domain.D_Impl.Transfer]
default_config [Abstractions]
Default configuration of EVA.
default_offsetmap [Cvalue.Default_offsetmap]
display [Value_perf]
Display a complete summary of performance informations.
distinct_subpart [Cvalue_domain]
div [Cvalue.V]
div_towards_minus_infty [Gauges_domain.G.Bounds]
div_towards_plus_infty [Gauges_domain.G.Bounds]
dkey [Gauges_domain]
dkey [Widen_hints_ext]
dkey_alarm [Value_parameters]
Debug category used when emitting an alarm in "non-warning" mode
dkey_final_states [Value_parameters]
dkey_garbled_mix [Value_parameters]
Debug category used to print garbled mix
dkey_initial_state [Value_parameters]
Debug categories responsible for printing initial and final states of Value.
do_assign [Eval_stmt]
do_promotion [Abstract_value.S]
do_promotion [Evaluation.S]
do_promotion [Cvalue_forward]
do_promotion [Eval_op]
do_warn [Valarms]
dump_args [Builtins_misc]
dump_garbled_mix [Value_util]
print information on the garblex mix created during evaluation
dump_state [Builtins_misc]
Builtins with multiple names; the lookup is done using a distinctive prefix
dump_state_file [Builtins_misc]

E
elements [Equality_sig.Set]
elements_only_left [Equality_sig.Set]
emit [Alarmset]
Emits the alarms according to the given warn mode.
emit_alarm [Builtins]
Emit an ACSL assert (using \warning predicate) to signal that the builtin encountered an alarm described by the string.
emit_message_and_status [Eval_annots]
emit_status [Eval_annots]
emitter [Value_util]
empty [Gui_callstacks_filters]
empty [FCMap.S]
The empty map.
empty [Widen_type]
An empty set of hints
empty [Abstract_domain.S]
Initialization
empty [Partitioning.Partition]
empty [Partitioning.StateSet]
empty [Equality_sig.Set]
empty [Hcexprs.BaseToHCESet]
empty [Hcexprs.HCEToZone]
empty [Gauges_domain.D_Impl]
empty [Gauges_domain.G]
empty [Eval.Valuation]
empty [State_imp]
Creation
empty [State_set]
Creation
empty_wh [Gauges_domain.G.MV]
end_stmt [Alarmset]
end_stmt [Valarms]
enlarge [Gauges_domain.G.Bounds]
enter_loop [Abstract_domain.Transfer]
enter_loop [Transfer_stmt.S]
enter_loop [Gauges_domain.D_Impl.Transfer]
enter_loop [Gauges_domain.G]
enter_scope [Abstract_domain.S]
Scoping: abstract transformers for entering and exiting blocks.
enter_scope [Gauges_domain.D_Impl]
enumerate_valid_bits [Precise_locs]
env_annot [Abstract_domain.Logic]
env_annot [Gauges_domain.D_Impl]
env_annot [Eval_terms]
env_assigns [Eval_terms]
env_current_state [Abstract_domain.Logic]
env_current_state [Gauges_domain.D_Impl]
env_current_state [Eval_terms]
env_only_here [Eval_terms]
Used by auxiliary plugins, that do not supply the other states
env_post_f [Abstract_domain.Logic]
env_post_f [Gauges_domain.D_Impl]
env_post_f [Eval_terms]
env_pre_f [Abstract_domain.Logic]
env_pre_f [Gauges_domain.D_Impl]
env_pre_f [Eval_terms]
epilogue [Separate]
eq_type [Structure.Key]
equal [FCMap.S]
equal cmp m1 m2 tests whether the maps m1 and m2 are equal, that is, contain equal keys and associate them with equal data.
equal [Equality_sig.S]
equal [Hashtbl.HashedType]
The equality predicate used to compare keys.
equal [Equality_sig.Set]
equal [Gauges_domain.G.MultipleIterations]
equal [Gauges_domain.G.Bounds]
equal [Structure.Key]
equal [Alarmset]
equal_gui_after [Gui_types]
equal_gui_offsetmap_res [Gui_types]
equal_gui_res [Gui_types]
equal_loc [Precise_locs]
equal_loc [Abstract_location.S]
equal_offset [Precise_locs]
equal_offset [Abstract_location.S]
eval_and_reduce_p_kind [Eval_annots]
eval_assigns_from [Eval_annots]
eval_binop_float [Eval_op]
eval_binop_int [Eval_op]
eval_by_callstack [Eval_annots]
eval_expr [Analysis.Results]
eval_expr [Eval_exprs]
eval_expr_with_deps_state [Eval_non_linear]
Same functionality as Eval_exprs.eval_expr_with_deps_state.
eval_expr_with_deps_state [Eval_exprs]
eval_float_constant [Cvalue_forward]
eval_float_constant [Eval_op]
The arguments are the approximate float value computed during parsing, the size of the floating-point type, and the string representing the initial constant if available.
eval_function_exp [Evaluation.S]
Evaluation of the function argument of a Call constructor
eval_gauge [Gauges_domain.G]
eval_lval [Eval_exprs]
eval_predicate [Abstract_domain.Logic]
eval_predicate [Gauges_domain.D_Impl]
eval_predicate [Eval_terms]
eval_term [Eval_terms]
eval_term_as_exact_locs [Eval_terms]
eval_tlval [Eval_terms]
eval_tlval_as_location [Eval_terms]
eval_tlval_as_zone [Eval_terms]
eval_tlval_as_zone_under_over [Eval_terms]
Return a pair of (under-approximating, over-approximating) zones.
eval_unop [Eval_op]
eval_varinfo [Abstract_location.S]
evaluate [Evaluation.S]
evaluate ~valuation state expr evaluates the expression expr in the state state, and returns the pair result, alarms, where: alarms are the set of alarms ensuring the soundness of the evaluation;, result is either `Bottom if the evaluation leads to an error, or `Value (valuation, value), where value is the numeric value computed for the expression expr, and valuation contains all the intermediate results of the evaluation. The valuation argument is a cache of already computed expressions. It is empty by default. The reduction argument allows deactivating the backward reduction performed after the forward evaluation.
exists [FCMap.S]
exists p m checks if at least one binding of the map satisfy the predicate p.
exists [Equality_sig.S]
exists p s checks if at least one element of the equality satisfies the predicate p.
exists [Equality_sig.Set]
exists [Alarmset]
exists [State_imp]
exists [State_set]
exists [Parameter_sig.Set]
Is there some element satisfying the given predicate?
exp_ev [Gui_eval]
expr_contains_volatile [Eval_typ]
extend_loc [Domain_lift.Conversion]
extend_val [Domain_lift.Conversion]
extend_val [Location_lift.Conversion]
externalize [Eval_stmt]
extract [Cvalue_domain]
extract_expr [Abstract_domain.Queries]
Query function for compound expressions: eval oracle t exp returns the known value of exp by the state t.
extract_expr [Gauges_domain.D_Impl]
extract_gauge [Gauges_domain.G]
extract_lval [Abstract_domain.Queries]
Query function for lvalues: find oracle t lval typ loc returns the known value stored at the location loc of the left value lval of type typ.
extract_lval [Gauges_domain.D_Impl]

F
filter [FCMap.S]
filter p m returns the map with all the bindings in m that satisfy predicate p.
filter [Equality_sig.S]
filter p s returns the equality between all elements in s that satisfy predicate p.
filter_by_bases [Abstract_domain.S]
Mem exec.
filter_by_bases [Mem_exec2.Domain]
filter_by_bases [Gauges_domain.D_Impl]
filter_if [Separate]
filter_map_inplace [Hashtbl.S]
finalize_call [Abstract_domain.Transfer]
finalize_call stmt call ~pre ~post computes the state after a function call, given the state pre before the call, and the state post at the end of the called function.
finalize_call [Gauges_domain.D_Impl.Transfer]
find [FCMap.S]
find x m returns the current binding of x in m, or raises Not_found if no such binding exists.
find [Cvalue.Model]
find ?conflate_bottom state loc returns the same value as find_indeterminate, but removes the indeterminate flags from the result.
find [Abstract_domain.Valuation]
find [Equality_sig.Set]
find elt set return the (single) equality involving elt that belongs to set, or raise Not_found if no such equality exists.
find [Hcexprs.BaseToHCESet]
may raise Not_found
find [Hcexprs.HCEToZone]
may raise Not_found
find [Eval.Valuation]
find [Alarmset]
Returns the status of a given alarm.
find [Hashtbl.S]
find [Eval_op]
Tempory.
find [State_builder.Hashtbl]
Return the current binding of the given key.
find [Parameter_sig.Map]
Search a given key in the map.
find_all [Hashtbl.S]
find_all [State_builder.Hashtbl]
Return the list of all data associated with the given key.
find_builtin [Builtins]
Find a previously registered builtin.
find_builtin_override [Builtins]
Should the given function be replaced by a call to a builtin
find_default [Hcexprs.BaseToHCESet]
returns the empty set when the key is not bound
find_default [Hcexprs.HCEToZone]
returns the empty set when the key is not bound
find_loc [Abstract_domain.Valuation]
find_loc [Eval.Valuation]
find_lv [Eval_exprs]
find_option [Equality_sig.Set]
Same as find, but return None in the last case.
find_right_value [Cvalue_transfer]
find_subpart [Cvalue_domain]
find_unspecified [Cvalue.Model]
find_unspecified ~conflate_bottom state loc returns the value and flags associated to loc in state.
float_kind [Value_util]
Classify a Cil_types.fkind as either a 32 or 64 floating-point type.
float_zeros [Abstract_value.S]
fold [FCMap.S]
fold f m a computes (f kN dN ... (f k1 d1 a)...), where k1 ... kN are the keys of all bindings in m (in increasing order), and d1 ... dN are the associated data.
fold [Precise_locs]
fold [Equality_sig.S]
fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s, in increasing order.
fold [Abstract_domain.Valuation]
fold [Partitioning.Partition]
fold [Partitioning.StateSet]
fold [Equality_sig.Set]
fold [Eval.Valuation]
fold [Hashtbl.S]
fold [State_imp]
Iterators
fold [State_builder.Hashtbl]
fold [State_set]
Iterators
fold2_join_heterogeneous [Hptset.S]
fold_emitted_alarms [Builtins]
Iteration on special assertions built by the builtins
fold_left2_best_effort [Function_args]
fold_sorted [State_builder.Hashtbl]
for_all [FCMap.S]
for_all p m checks if all the bindings of the map satisfy the predicate p.
for_all [Equality_sig.S]
for_all p s checks if all elements of the equality satisfy the predicate p.
for_all [Equality_sig.Set]
for_all [Alarmset]
force_compute [Analysis]
Perform a full analysis, starting from the main function.
force_compute [Eval_funs]
Perform a full analysis, starting from the main function.
forget [Gauges_domain.G]
forward_binop [Abstract_value.S]
forward_binop context typ binop v1 v2 evaluates the value v1 binop v2, and the alarms resulting from the operations.
forward_binop_float [Cvalue_forward]
forward_binop_float_alarm [Cvalue_forward]
forward_binop_int [Cvalue_forward]
forward_comp_int [Cvalue.V]
forward_field [Abstract_location.S]
Computes the field offset of a fieldinfo, with the given remaining offset.
forward_index [Abstract_location.S]
forward_index typ value offset computes the array index offset of (Index (ind, off)), where the index expression ind evaluates to value and the remaining offset off evaluates to offset.
forward_pointer [Abstract_location.S]
Mem case in the AST: the host is a pointer.
forward_unop [Abstract_value.S]
forward_unop context typ unop v evaluates the value unop v, and the alarms resulting from the operations.
forward_unop [Cvalue_forward]
forward_variable [Abstract_location.S]
Var case in the AST: the host is a variable.
frama_c_memchr_wrapper [Builtins_string]
frama_c_rawmemchr_wrapper [Builtins_string]
frama_c_strchr_wrapper [Builtins_string]
frama_c_strlen_wrapper [Builtins_string]
frama_c_strnlen_wrapper [Builtins_string]
from_callstack [Gui_callstacks_filters]
from_ival [Gauges_domain.G.Bounds]
from_shape [Hptset.S]
Build a set from another elt-indexed map or set.
function_calls_handling [Gauges_domain]

G
gauge_from_state [Gauges_domain.G]
get [Abstract_domain.Interface]
For a key of type k key: if the states of this domain (of type t) contain a part (of type k) from the domain identified by the key, then get key returns an accessor for this part of a state., otherwise, get key returns None.
get [Hcexprs.HCE]
get [Structure.External]
get [State_builder.Ref]
Get the referenced value.
getWidenHints [Widen]
getWidenHints kf s retrieves the set of widening hints related to function kf and statement s.
get_LoadFunctionState [Value_parameters]
get_SaveFunctionState [Value_parameters]
get_function_name [Parameter_sig.String]
returns the given argument only if it is a valid function name (see Parameter_customize.get_c_ified_functions for more information), and abort otherwise.
get_influential_vars [Eval_exprs]
get_initial_state [Abstract_domain.Store]
get_initial_state_by_callstack [Abstract_domain.Store]
get_plain_string [Parameter_sig.String]
always return the argument, even if the argument is not a function name.
get_possible_values [Parameter_sig.String]
What are the acceptable values for this parameter.
get_range [Parameter_sig.Int]
What is the possible range of values for this parameter.
get_results [Value_results]
get_results [Value.Value_results]
get_retres_vi [Library_functions]
Fake varinfo used by Value to store the result of functions without bodies.
get_rounding_mode [Value_util]
get_slevel [Value_util]
get_stmt_state [Analysis.Results]
get_stmt_state [Abstract_domain.Store]
get_stmt_state_by_callstack [Abstract_domain.Store]
get_stmt_widen_hint_terms [Widen_hints_ext]
get_stmt_widen_hint_terms s returns the list of widen hints associated to s.
get_v [Cvalue.V_Or_Uninitialized]
global_state [Abstract_domain.S]
global_state [Gauges_domain.D_Impl]
gui_loc_equal [Gui_types]
gui_loc_loc [Gui_types]
gui_loc_logic_env [Gui_eval]
Logic labels valid at the given location.
gui_selection_data_empty [Gui_eval]
Default value.
gui_selection_equal [Gui_types]

H
handle_overflow [Eval_op]
has_requires [Eval_annots]
hash [Hashtbl.HashedType]
A hashing function on keys.
hash [Gauges_domain.G.MultipleIterations]
hash [Structure.Key]
hash_gui_callstack [Gui_types]
header [Eval_annots.ActiveBehaviors]
hints_from_keys [Widen_type]
Widen hints for a given statement, suitable for function Cvalue.Model.widen.

I
id [Equality.Element]
Identity of a key.
id [Hcexprs.HCE]
ik_attrs_range [Eval_typ]
Range for an integer type with some attributes.
ik_range [Eval_typ]
imprecise_location [Precise_locs]
imprecise_location_bits [Precise_locs]
imprecise_offset [Precise_locs]
inc [Gauges_domain.G]
incr [Stop_at_nth]
incr [Parameter_sig.Int]
Increment the integer.
incr_loop_counter [Abstract_domain.Transfer]
incr_loop_counter [Transfer_stmt.S]
incr_loop_counter [Gauges_domain.D_Impl.Transfer]
indirect_zone_of_lval [Value_util]
Given a function computing the location of lvalues, computes the memory zone on which the offset and the pointer expression (if any) of an lvalue depend.
initial_state [Initialization.S]
initial_state_lib_entry [Initial_state]
initial_state_not_lib_entry [Initial_state]
initial_state_with_formals [Initialization.S]
initialize_var [Abstract_domain.S]
initialize_var [Gauges_domain.D_Impl]
initialize_var_using_type [Abstract_domain.S]
initialize_var_using_type [Cvalue_init]
initialize_var_using_type varinfo state uses the type of varinfo to create an initial value in state.
initialize_var_using_type [Gauges_domain.D_Impl]
initialize_var_using_type [Initial_state]
initialized [Cvalue.V_Or_Uninitialized]
initialized v returns the definitely initialized, non-escaping representant of v.
inject [Cvalue_domain]
inject_address [Abstract_value.S]
Abstract address for the given varinfo.
inject_comp_result [Cvalue.V]
inject_int [Cvalue.V]
inject_int [Abstract_value.S]
inject_ival [Precise_locs]
inject_location_bits [Precise_locs]
inject_range [Gauges_domain.G.Bounds]
inter [Equality_sig.S]
Intersection.
inter [Equality_sig.Set]
inter [Hcexprs.BaseToHCESet]
inter [Hcexprs.HCEToZone]
inter [Alarmset.Status]
inter [Alarmset]
Pointwise intersection of property status: the most precise status is kept.
interp_annot [Transfer_logic.S]
interp_annot [Eval_annots]
interp_boolean [Cvalue.V]
interp_call [Eval_stmt]
intersects [Equality_sig.S]
intersect s s' = true iff the two equalities both involve the same element.
intersects [Hptset.S]
intersects s1 s2 returns true if and only if s1 and s2 have an element in common
interval_key [Main_values]
Key for intervals.
ip_from_precondition [Eval_annots]
is_active [Eval_annots.ActiveBehaviors]
is_active_aux [Eval_annots.ActiveBehaviors]
is_arithmetic [Cvalue.V]
Returns true if the value may not be a pointer.
is_bitfield [Eval_typ]
Bitfields
is_bottom [Cvalue.V_Or_Uninitialized]
is_bottom [Cvalue.V]
is_bottom_loc [Precise_locs]
is_bottom_offset [Precise_locs]
is_const_write_invalid [Value_util]
Detect that the type is const, and that option -global-const is set.
is_empty [FCMap.S]
Test whether a map is empty or not.
is_empty [Partitioning.StateSet]
is_empty [Equality_sig.Set]
is_empty [Alarmset]
Is there an assertion with a non True status ?
is_empty [State_imp]
Information
is_empty [State_set]
Information
is_global [Widen_hints_ext]
is_global wh returns true iff widening hint wh has a "global" prefix.
is_imprecise [Cvalue.V]
is_included [Abstract_domain.Lattice]
Inclusion test.
is_included [Abstract_value.S]
is_included [Hcexprs.HCEToZone]
is_included [Gauges_domain.G.IterationInfo]
is_included [Gauges_domain.G.MC]
is_included [Gauges_domain.G.MV]
is_included [Gauges_domain.G.Bounds]
is_included [Gauges_domain.G]
is_indeterminate [Cvalue.V_Or_Uninitialized]
is_indeterminate v = false implies v only has definitely initialized values and non-escaping addresses.
is_initialized [Cvalue.V_Or_Uninitialized]
is_initialized v = true implies v is definitely initialized.
is_isotropic [Cvalue.V]
is_noesc [Cvalue.V_Or_Uninitialized]
is_noesc v = true implies v has no escaping addresses.
is_non_terminating_instr [Gui_callstacks_filters]
is_non_terminating_instr [Value_results]
Returns true iff there exists executions of the statement that does not always fail/loop (for function calls).
is_reachable_stmt [Gui_callstacks_filters]
is_top_loc [Precise_locs]
is_topint [Cvalue.V]
is_value_zero [Value_util]
Return true iff the argument has been created by Value_util.zero
iter [FCMap.S]
iter f m applies f to all bindings in map m.
iter [Equality_sig.S]
iter f s applies f in turn to all elements of s.
iter [Partitioning.StateSet]
iter [Equality_sig.Set]
iter [Alarmset]
iter [Hashtbl.S]
iter [State_imp]
iter [State_builder.Hashtbl]
iter [State_set]
iter_sorted [State_builder.Hashtbl]

J
join [Widen_type]
join [Abstract_domain.Lattice]
Semi-lattice structure.
join [Abstract_value.S]
join [Partitioning.Partition]
join [Partitioning.StateSet]
join [Gauges_domain.G.MultipleIterations]
join [Gauges_domain.G.MC]
join [Gauges_domain.G.Bounds]
join [Gauges_domain.G]
join [Alarmset.Status]
join [State_imp]
Export
join [State_set]
Export
join_and_is_included [Abstract_domain.Lattice]
Do both operations simultaneously
join_and_is_included [Gauges_domain.G]
join_consecutive_lambda [Gauges_domain.G]
join_disjoint [Gauges_domain.G.MV]
join_final_states [Split_return]
Join the given state_set.
join_gui_offsetmap_res [Gui_types]
join_iterations [Gauges_domain.G]
join_list [Alarmset.Status]
join_list_predicate_status [Eval_terms]
join_predicate_status [Eval_terms]
join_same_lambda [Gauges_domain.G]

K
key [Cvalue_domain]
key [Equality_domain.S]
kf_assigns_only_result_or_volatile [Eval_typ]
returns true if the function assigns only \result or variables that have volatile qualifier (that are usually not tracked by domains anyway).
kf_of_gui_loc [Gui_types]
kf_strategy [Split_return]
ki_of_callstack [Value_messages]
kill_base [Gauges_domain.G]

L
leave_loop [Abstract_domain.Transfer]
leave_loop [Transfer_stmt.S]
leave_loop [Gauges_domain.D_Impl.Transfer]
leave_loop [Gauges_domain.G]
leave_scope [Abstract_domain.S]
leave_scope [Transfer_stmt.Domain]
leave_scope [Gauges_domain.D_Impl]
legacy_config [Abstractions]
Legacy configuration of EVA, with only the cvalue domain enabled.
length [Partitioning.StateSet]
length [Hashtbl.S]
length [State_imp]
length [State_builder.Hashtbl]
Length of the table.
length [State_set]
lift [Gauges_domain.G.Bounds]
load_and_merge_function_state [State_import]
Loads the saved initial global state, and merges it with the given state (locals plus new globals which were not present in the original AST).
loc_bottom [Precise_locs]
loc_size [Precise_locs]
loc_size [Evaluation.S]
loc_to_base [Gauges_domain.G]
loc_top [Precise_locs]
local [Per_stmt_slevel]
Slevel to use in this function
lval_contains_volatile [Eval_typ]
Those two expressions indicate that one l-value contained inside the arguments (or the l-value itself for lval_contains_volatile) has volatile qualifier.
lval_ev [Gui_eval]
lval_to_loc [Eval_exprs]
lval_to_loc_deps_state [Eval_exprs]
lval_to_loc_state [Eval_exprs]
lval_to_precise_loc [Eval_exprs]
lval_to_precise_loc_deps_state [Eval_exprs]
lval_to_precise_loc_state [Eval_exprs]
lval_zone_ev [Gui_eval]
lvaluate [Evaluation.S]
lvaluate ~valuation ~for_writing state lval evaluates the left value lval in the state state.

M
main_initial_state_with_formals [Function_args]
make [Cvalue.V_Or_Uninitialized]
make [Abstractions]
Builds the abstractions according to a configuration.
make_data_all_callstacks [Gui_eval]
make_loc_contiguous [Eval_op]
'Simplify' the location if it represents a contiguous zone: instead of multiple offsets with a small size, change it into a single offset with a size that covers the entire range.
make_precise_loc [Precise_locs]
make_return [Abstract_domain.Transfer]
make_return kf stmt assigned valuation state makes an abstraction of the return value of the function kf.
make_return [Gauges_domain.D_Impl.Transfer]
make_type [Datatype.Hashtbl]
make_volatile [Cvalue_forward]
make_volatile ?typ v makes the value v more general (to account for external modifications), whenever typ is None or when it has type qualifier volatile.
make_volatile [Eval_op]
make_volatile ?typ v makes the value v more general (to account for external modifications), whenever typ is None or when it has type qualifier volatile
malloced_bases [Builtins_malloc]
All bases that have been dynamically created in the current execution.
map [FCMap.S]
map f m returns a map with same domain as m, where the associated value a of all bindings of m has been replaced by the result of the application of f to a.
map [Cvalue.V_Or_Uninitialized]
map [Partitioning.StateSet]
map [State_set]
map2 [Cvalue.V_Or_Uninitialized]
initialized/escaping information is the join of the information on each argument.
map2 [Gauges_domain.G.Gauge]
mapi [FCMap.S]
Same as FCMap.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.
mark_degeneration [Eval_slevel.Computer]
mark_green_and_red [Eval_annots]
mark_invalid_initializers [Eval_annots]
mark_kf_as_called [Value_results]
mark_rte [Eval_annots]
mark_unreachable [Eval_annots]
max_binding [FCMap.S]
Same as FCMap.S.min_binding, but returns the largest binding of the given map.
maybe_warn_completely_indeterminate [Warn]
Print a message about the given location containing a completely indeterminate value.
maybe_warn_div [Warn]
Emit an alarm about a non-null divisor when the supplied value may contain zero.
maybe_warn_indeterminate [Warn]
Warn for unitialized or escaping bits in the value passed as argument.
mem [FCMap.S]
mem x m returns true if m contains a binding for x, and false otherwise.
mem [Equality_sig.S]
mem x s tests whether x belongs to the equality s.
mem [Abstract_domain.Interface]
Tests whether a key belongs to the domain.
mem [Equality_sig.Set]
mem equality set = true iff ∃ eq ∈ set, equality ⊆ eq
mem [Structure.External]
mem [Hashtbl.S]
mem [State_builder.Hashtbl]
mem [Parameter_sig.Map]
mem [Parameter_sig.Set]
Does the given element belong to the set?
mem_builtin [Builtins]
Does the builtin table contain an entry for name?
memo [Datatype.Hashtbl]
memo tbl k f returns the binding of k in tbl.
memo [State_builder.Hashtbl]
Memoization.
merge [FCMap.S]
merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.
merge [Partitioning.StateSet]
merge [Hptset.S]
merge [Per_stmt_slevel]
Slevel merge strategy for this function
merge [Value_results]
merge [State_set]
Merge the two sets together.
merge [Value.Value_results]
merge_after_states_in_db [Value_results]
merge_into [State_set]
Raise Unchanged if the first set was already included in into
merge_referenced_formals [Function_args]
merge_results [Eval_slevel.Computer]
merge_set_return_new [Partitioning.Partition]
merge_set_return_new [State_imp]
merge_states_in_db [Value_results]
min_binding [FCMap.S]
Return the smallest binding of the given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.
msg_status [Eval_annots]
mul [Cvalue.V]
mul [Gauges_domain.G.Gauge]
mul [Gauges_domain.G.Bounds]
mul_ct [Gauges_domain.G.Gauge]
mul_ct [Gauges_domain.G.Bounds]
mv_minus_mc [Gauges_domain.G]

N
narrow [Cvalue.V_Offsetmap]
narrow [Abstract_value.S]
narrow [Gauges_domain.G.Bounds]
narrow [State_set]
narrow_list [State_set]
need_cast [Eval_typ]
return true if the two types are statically distinct, and a cast from one to the other may have an effect on an abstract value.
neg [Gauges_domain.G.Gauge]
neg [Gauges_domain.G.Bounds]
new_alarm [Value_messages]
new_counter [Mem_exec2]
Counter that must be used each time a new call is analyzed, in order to refer to it later
new_counter [Mem_exec]
Counter that must be used each time a new call is analyzed, in order to refer to it later
new_status [Value_messages]
no_memoization_enabled [Mark_noresults]
no_offset [Abstract_location.S]
none [Alarmset]
no alarms: all potential assertions have a True status.
null_ev [Gui_eval]
num_hints [Widen_type]
Define numeric hints for one or all variables (None), for a certain stmt or for all statements (None).

O
octagon_key [Apron_domain]
of_char [Cvalue.V]
of_exp [Hcexprs.HCE]
of_int64 [Cvalue.V]
of_list [Partitioning.StateSet]
of_list [State_set]
of_list_forget_history [State_set]
of_lval [Hcexprs.HCE]
of_string [Split_strategy]
off [Parameter_sig.Bool]
Set the boolean to false.
offset_bottom [Precise_locs]
offset_cardinal_zero_or_one [Abstract_location.S]
Needed for Evaluation.get_influential_vars
offset_top [Precise_locs]
offset_zero [Precise_locs]
offsetmap_contains_imprecision [Warn]
Returns the first eventual imprecise part contained in an offsetmap
offsetmap_contains_local [Locals_scoping]
offsetmap_matches_type [Cvalue_forward]
offsetmap_matches_type [Eval_typ]
offsetmap_matches_type t o returns true if either: o contains a single scalar binding, of the expected scalar type t (float or integer), o contains multiple bindings, pointers, etc., t is not a scalar type.
offsetmap_of_lv [Eval_exprs]
May raise Int_Base.Error_Top
offsetmap_of_v [Eval_op]
Transformation a value into an offsetmap of size sizeof(typ) bytes.
offsetmap_top_addresses_of_locals [Locals_scoping]
offsetmap_top_addresses_of_locals is_local returns a function that topifies all the parts of an offsetmap that contains a pointer verifying is_local.
offsm_key [Offsm_value]
ok [Apron_domain]
Are apron domains available?
on [Parameter_sig.Bool]
Set the boolean to true.
on_cvalue_ival [Gauges_domain.G.Gauge]
one [Cvalue.CardinalEstimate]
opt2 [Gauges_domain.G]
output [Parameter_sig.With_output]
To be used by the plugin to output the results of the option in a controlled way.

P
pair [Equality_sig.S]
The equality between two elements.
parameters_correctness [Value_parameters]
parameters_tuning [Value_parameters]
partially_overlap [Abstract_location.S]
partition [FCMap.S]
partition p m returns a pair of maps (m1, m2), where m1 contains all the bindings of s that satisfy the predicate p, and m2 is the map with all the bindings of s that do not satisfy p.
partition_terminating_instr [Value_results]
Returns the list of terminating callstacks and the list of non-terminating callstacks.
paste_offsetmap [Eval_op]
Temporary.
ploc_key [Main_locations]
Key for precise locs.
polka_equalities_key [Apron_domain]
polka_loose_key [Apron_domain]
polka_strict_key [Apron_domain]
pop_call_stack [Value_util]
post_kind [Eval_annots]
postconditions_mention_result [Value_util]
Does the post-conditions of this specification mention \result?
pp_bhv [Eval_annots.ActiveBehaviors]
pp_callstack [Value_util]
Prints the current callstack.
pp_header [Eval_annots]
pp_p_kind [Eval_annots]
precompute_widen_hints [Widen]
Parses all widening hints defined via the widen_hint syntax extension.
predicate_deps [Eval_terms]
predicate_ev [Gui_eval]
pretty [Widen_type]
Pretty-prints a set of hints (for debug purposes only).
pretty [Cvalue.CardinalEstimate]
pretty [Partitioning.Partition]
pretty [Partitioning.StateSet]
pretty [Gauges_domain.D_Impl]
pretty [Gauges_domain.G.Gauge]
pretty [Gauges_domain.G.Bounds]
pretty [Gauges_domain.G]
pretty [Alarmset]
pretty [State_imp]
pretty [State_set]
pretty_actuals [Value_util]
pretty_callstack [Gui_types]
pretty_callstack_short [Gui_types]
pretty_current_cfunction_name [Value_util]
pretty_debug [Value_types.Callstack]
pretty_debug [Equality_domain.S]
pretty_debug [Equality.Element]
pretty_debug [Hptset.S]
pretty_debug [Hcexprs.HCE]
pretty_debug [Gauges_domain.G.Bounds]
pretty_gui_offsetmap_res [Gui_types]
pretty_gui_res [Gui_types]
pretty_gui_selection [Gui_types]
pretty_iteration_info [Gauges_domain.G]
pretty_loc [Precise_locs]
pretty_loc [Abstract_location.S]
pretty_loc_bits [Precise_locs]
pretty_logic_evaluation_error [Eval_terms]
pretty_long_log10 [Cvalue.CardinalEstimate]
pretty_loop_info [Gauges_domain.G]
pretty_loop_step [Gauges_domain.G]
pretty_offset [Precise_locs]
pretty_offset [Abstract_location.S]
pretty_predicate_status [Eval_terms]
pretty_short [Value_types.Callstack]
Print a call stack without displaying call sites.
pretty_state_as_c_assert [Builtins_nonfree_print_c]
pretty_state_as_c_assignments [Builtins_nonfree_print_c]
pretty_stitched_offsetmap [Eval_op]
pretty_strategies [Split_return]
pretty_typ [Cvalue.V]
print [Structure.Key]
process_inactive_behavior [Eval_annots]
process_inactive_behaviors [Eval_annots]
process_inactive_postconds [Eval_annots]
project [Cvalue_domain]
project [Equality_domain.S]
project_ival [Cvalue.V]
Raises Not_based_on_null if the value may be a pointer.
project_ival_bottom [Cvalue.V]
prologue [Separate]
push_call_stack [Value_util]

R
range_inclusion [Eval_typ]
Check inclusion of two integer ranges.
range_lower_bound [Eval_typ]
range_upper_bound [Eval_typ]
reduce [Abstractions.Value]
reduce [Evaluation.Value]
Inter-reduction of values.
reduce [Evaluation.S]
reduce ~valuation state expr positive evaluates the expresssion expr in the state state, and then reduces the valuation such that the expression expr evaluates to a zero or a non-zero value, according to positive.
reduce_binding [Cvalue.Model]
reduce_binding state loc v refines the value associated to loc in state according to v, by keeping the values common to the existing value and v.
reduce_by_accessed_loc [Eval_exprs]
reduce_by_cond [Eval_exprs]
Never returns Model.bottom.
reduce_by_danglingness [Cvalue.V_Or_Uninitialized]
reduce_by_danglingness dangling v reduces v so that its result r verifies \dangling(r) if dangling is true, and !\dangling(r) otherwise.
reduce_by_initialized_defined [Eval_op]
reduce_by_initializedness [Cvalue.V_Or_Uninitialized]
reduce_by_initializedness initialized v reduces v so that its result r verifies \initialized(r) if initialized is true, and !\initialized(r) otherwise.
reduce_by_predicate [Abstract_domain.Logic]
reduce_by_predicate [Gauges_domain.D_Impl]
reduce_by_predicate [Eval_terms]
reduce_by_valid_loc [Eval_op]
reduce_further [Abstract_domain.Queries]
Given a reduction expr = value, provides more reductions that may be performed.
reduce_further [Gauges_domain.D_Impl]
reduce_indeterminate_binding [Cvalue.Model]
Same behavior as reduce_previous_binding, but takes a value with 'undefined' and 'escaping addresses' flags.
reduce_index_by_array_size [Abstract_location.S]
reduce_index_by_array_size ~size_expr ~index_expr size index reduces the value index to fit into the inverval 0..(size-1).
reduce_loc_by_validity [Abstract_location.S]
reduce_loc_by_validity for_writing bitfield lval loc reduce the location loc by its valid part for a read or write operation, according to the for_writing boolean.
reduce_previous_binding [Cvalue.Model]
reduce_previous_binding state loc v reduces the value associated to loc in state; use with caution, as the inclusion between the new and the old value is not checked.
refine_active [Eval_annots]
register_builtin [Builtins]
Register the given OCaml function as a builtin, that will be used instead of the Cil C function of the same name
register_initial_state [Abstract_domain.Store]
register_malloced_base [Builtins_malloc]
Should not be used by casual users.
register_state_after_stmt [Abstract_domain.Store]
register_state_before_stmt [Abstract_domain.Store]
registered_builtins [Builtins]
Returns a list of the pairs (name, builtin_sig) registered via register_builtin.
reinterpret [Abstract_value.S]
Read the given value with the given type.
reinterpret [Evaluation.S]
reinterpret [Cvalue_forward]
reinterpret [Eval_op]
reinterpret_float [Eval_op]
Read the given value value as a float int of the given fkind.
remember_bases_with_locals [Locals_scoping]
Add the given set of bases to an existing clobbered set
remember_if_locals_in_offsetmap [Locals_scoping]
Same as above with an entire offsetmap
remember_if_locals_in_value [Locals_scoping]
remember_locals_in_value clob loc v adds all bases pointed to by loc to clob if v contains the address of a local or formal
remove [FCMap.S]
remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.
remove [Equality_sig.S]
remove x s returns the equality between all elements of s, except x.
remove [Equality_sig.Set]
remove elt set remove any occurrence of elt in set.
remove [Hcexprs.BaseToHCESet]
remove [Hcexprs.HCEToZone]
remove [Eval.Valuation]
remove [Hashtbl.S]
remove [State_builder.Hashtbl]
remove_coeffs [Gauges_domain.G]
remove_indeterminateness [Cvalue.V_Or_Uninitialized]
Remove 'unitialized' and 'escaping addresses' flags from the argument
remove_loc [Eval.Valuation]
remove_variables [Cvalue.Model]
For variables that are coming from the AST, this is equivalent to uninitializing them.
reorder [Partitioning.StateSet]
reorder [State_set]
Invert the order in which the states are iterated over
replace [Hashtbl.S]
replace [State_builder.Hashtbl]
Add a new binding.
reset [Hashtbl.S]
reset [Value_perf]
Reset the internal state of the module; to call at the very beginning of the analysis.
resolv_func_vinfo [Eval_exprs]
resolve_functions [Abstract_value.S]
resolve_functions ~typ_pointer v finds within v all the functions with a type compatible with typ_pointer.
resolve_functions [Eval_typ]
given (funs, warn) = resolve_functions typ v, funs is the set of functions pointed to by v that have a type compatible with typ.
restrict_loc [Domain_lift.Conversion]
restrict_val [Domain_lift.Conversion]
restrict_val [Location_lift.Conversion]
results [Eval_slevel.Computer]
results_kf_computed [Gui_eval]
Catch the fact that we are in a function for which -no-results or one of its variants is set.
return [Transfer_stmt.S]
returned_value [Library_functions]
reuse [Abstract_domain.S]
reuse [Mem_exec2.Domain]
reuse [Gauges_domain.D_Impl]
reuse_previous_call [Mem_exec2.Make]
reuse_previous_call kf init_state args searches amongst the previous analyzes of kf one that matches the initial state init_state and the values of arguments args.
reuse_previous_call [Mem_exec]
reuse_previous_call (kf, ki) init_state searches amongst the previous analyzes of kf one that matches the initial state init_state.
run [Compute_functions]

S
safe_argument [Backward_formals]
safe_argument e returns true if e (which is supposed to be an actual parameter) is guaranteed to evaluate in the same way before and after the call.
sanitize_v [Gauges_domain.G.Gauge]
save_globals_state [State_import]
Saves the final state of globals variables after the return statement of the function defined via Value_parameters.SaveFunctionState.
self [Equality.Element]
self [Hcexprs.HCE]
set [Abstract_domain.Interface]
For a key of type k key: if the states of this domain (of type t) contain a part (of type k) from the domain identified by the key, then set key d state returns the state state in which this part has been replaced by d., otherwise, set key _ is the identity function.
set [Structure.External]
set [State_builder.Ref]
Change the referenced value.
set_callstacks_filter [Gui_callstacks_filters]
This function must be called when callstacks are focused.
set_current_state [Value_messages]
set_loc [Value_util]
set_output_dependencies [Parameter_sig.With_output]
Set the dependencies for the output of the option.
set_possible_values [Parameter_sig.String]
Set what are the acceptable values for this parameter.
set_range [Parameter_sig.Int]
Set what is the possible range of values for this parameter.
set_results [Value_results]
set_results [Value.Value_results]
set_syntactic_context [Valarms]
shape [Hptset.S]
Export the shape of the set.
shift_left [Cvalue.V]
shift_offset [Precise_locs]
shift_offset_by_singleton [Precise_locs]
shift_right [Cvalue.V]
should_memorize_function [Mark_noresults]
signal_abort [Partitioned_dataflow]
Mark the analysis as aborted.
signal_abort [Eval_slevel]
Mark the analysis as aborted.
singleton [FCMap.S]
singleton x y returns the one-element map that contains a binding y for x.
singleton [Partitioning.StateSet]
singleton [Equality_sig.Set]
singleton [Alarmset]
singleton [State_imp]
singleton [State_set]
singleton' [Partitioning.StateSet]
size [Abstract_location.S]
sizeof_lval_typ [Eval_typ]
Size of the type of a lval, taking into account that the lval might have been a bitfield.
split [FCMap.S]
split x m returns a triple (l, data, r), where l is the map with all the bindings of m whose key is strictly less than x; r is the map with all the bindings of m whose key is strictly greater than x; data is None if m contains no binding for x, or Some v if m binds v to x.
split_by_evaluation [Evaluation.S]
split_disjunction_and_reduce [Eval_terms]
If reduce is true, reduce in all cases.
split_final_states [Transfer_stmt.S]
start_call [Abstract_domain.Transfer]
Decision on a function call: start_call stmt call valuation state decides on the analysis of a call site.
start_call [Cvalue_transfer.Transfer]
start_call [Gauges_domain.D_Impl.Transfer]
start_doing [Value_perf]
start_stmt [Alarmset]
start_stmt [Valarms]
state_top_addresses [Locals_scoping]
state_top_addresses kf clob l state topifies all references to the variables in l.
state_top_addresses_of_locals [Locals_scoping]
state_top_addresses_of_locals exact warn topoffsm clob generalizes topoffsm into a function that topifies a memory state.
stats [Hashtbl.S]
stop_doing [Value_perf]
Call start_doing when finishing analyzing a function.
stop_if_stop_at_first_alarm_mode [Value_util]
storage [Domain_builder.InputDomain]
storage [Domain_store.InputDomain]
store_computed_call [Mem_exec2.Make]
store_computed_call kf init_state args call_results memoizes the fact that calling kf with initial state init_state and arguments args resulted in the results call_results.
store_computed_call [Mem_exec]
store_computed_call (kf, ki) init_state actuals outputs memoizes the fact that calling kf at statement ki, with initial state init_state and arguments actuals resulted in the states outputs; the expressions in the actuals are not used.
store_gauge [Gauges_domain.G]
structural_descr [Gauges_domain.G.MultipleIterations]
structural_descr [Locals_scoping]
structure [Abstract_domain.S_with_Structure]
A structure matching the type of the domain.
structure [Gauges_domain.D_Impl]
structure [Abstract_location.Internal]
structure [Abstract_value.Internal]
structure [Structure.Internal]
sub [Gauges_domain.G.Gauge]
sub [Gauges_domain.G.Bounds]
sub_min_max_cvalue [Gauges_domain.G]
sub_mv [Gauges_domain.G]
sub_untyped_pointwise [Cvalue.V]
See Locations.sub_pointwise.
subset [Equality_sig.S]
subset [Equality_sig.Set]
succ [Gauges_domain.G.MultipleIterations]
succ [Gauges_domain.G.Bounds]

T
tag [Structure.Key]
term_ev [Gui_eval]
tlval_ev [Gui_eval]
tlval_zone_ev [Gui_eval]
to_exp [Hcexprs.HCE]
to_ival [Gauges_domain.G.Bounds]
to_list [Partitioning.Partition]
to_list [Partitioning.StateSet]
to_list [State_imp]
to_list [State_set]
to_set [Partitioning.Partition]
to_set [State_imp]
to_string [Split_strategy]
to_value [Abstract_location.S]
top [Abstract_domain.Lattice]
Greatest element.
top [Abstract_value.S]
top [Gauges_domain.D_Impl]
top [Gauges_domain.G]
top [Locals_scoping]
top_addresses_of_locals [Locals_scoping]
Return two functions that topifies all references to the locals and formals of the given function.
top_int [Abstract_value.S]
tracked_variable [Gauges_domain.G]
translate_exp [Gauges_domain.G]

U
uncheck_add [Partitioning.StateSet]
uninitialize_blocks_locals [Cvalue.Model]
uninitialized [Cvalue.V_Or_Uninitialized]
Returns the canonical representant of a definitely uninitialized value.
union [Equality_sig.S]
Union.
union [Equality_sig.Set]
union [Hcexprs.BaseToHCESet]
union [Hcexprs.HCEToZone]
union [Alarmset]
Pointwise union of property status: the least precise status is kept.
unite [Equality_sig.Set]
unite a b map unites a and b in map.
unsafe_reinterpret [Cvalue_forward]
unspecify_escaping_locals [Cvalue.V_Or_Uninitialized]
update [Abstract_domain.Transfer]
update valuation t updates the state t by the values of expressions and the locations of lvalues stored in valuation.
update [Gauges_domain.D_Impl.Transfer]

V
v_of_offsetmap [Eval_op]
Reads the contents of the offsetmap (assuming it contains sizeof(typ) bytes) as a value of type V.t, then convert the result to type typ
v_uninit_of_offsetmap [Eval_op]
Reads the contents of the offsetmap (assuming it contains sizeof(typ) bytes), and return them as an uninterpreted value.
valid_cardinal_zero_or_one [Precise_locs]
Is the restriction of the given location to its valid part precise enough to perform a strong read, or a strong update.
valid_part [Precise_locs]
Overapproximation of the valid part of the given location for a read or write operation, according to the for_writing boolean.
value_assigned [Eval]
var_hints [Widen_type]
Define a set of bases to widen in priority for a given statement.
var_of_base [Gui_types]
vars_in_gui_res [Gui_types]
verify_assigns_from [Eval_annots]

W
warn_all_mode [CilE]
Emit all messages, including alarms and informative messages regarding the loss of precision.
warn_all_mode [Value_util]
warn_all_quiet_mode [Value_util]
warn_div [Valarms]
division.
warn_escapingaddr [Valarms]
warning to be emitted when two incompatible accesses to a location are done in unspecified order.
warn_float [Warn]
warn_float_addr [Warn]
warn_float_to_int_overflow [Valarms]
warn_imprecise_lval_read [Warn]
warn_inactive [Eval_annots]
warn_incompatible_fun_pointer [Valarms]
warn_indeterminate [Value_util]
warn_index [Valarms]
warn_index w ~positive ~range emits a warning signaling an out of bounds access.
warn_integer_overflow [Valarms]
warn_locals_escape [Warn]
warn_locals_escape_result [Warn]
warn_mem_read [Valarms]
warn_mem_write [Valarms]
warn_modified_result_loc [Warn]
This function should be used to treat a call lv = kf(...).
warn_nan_infinite [Valarms]
warn_none_mode [CilE]
Do not emit any message.
warn_overlap [Warn]
warn_overlap [Valarms]
warn_pointer_comparison [Valarms]
warn on invalid pointer comparison.
warn_pointer_subtraction [Valarms]
warn_reduce_by_accessed_loc [Eval_exprs]
warn_reduce_indeterminate_offsetmap [Warn]
If the supplied offsetmap has an arithmetic type and contains indeterminate bits (uninitialized, or escaping address), raises the corresponding alarm(s) and returns the reduced offsetmap and state.
warn_right_exp_imprecision [Warn]
warn_separated [Valarms]
warn_shift [Valarms]
Warn that the RHS of a shift operator must be positive, and optionnally less than the given size.
warn_shift_left_positive [Valarms]
Warn that the LHS of the left shift operator must be positive.
warn_top [Warn]
Abort the analysis, signaling that Top has been found.
warn_uninitialized [Valarms]
warn_valid_string [Valarms]
warning [Value_messages]
warning_once_current [Value_util]
widen [Abstract_domain.Lattice]
widen h t1 t2 is an over-approximation of join t1 t2.
widen [Gauges_domain.G.MultipleIterations]
widen [Gauges_domain.G.MC]
widen [Gauges_domain.G.MV]
widen [Gauges_domain.G.Bounds]
widen [Gauges_domain.G]
with_alarm_stop_at_first [Value_util]
with_alarms_raise_exn [Value_util]
wrap_double [Eval_op]
wrap_float [Eval_op]
wrap_int [Eval_op]
wrap_ptr [Eval_op]
wrap_size_t [Eval_op]
Specialization of the function above for standard types
write_abstract_value [Eval_op]
write_abstract_value ~with_alarms state lv typ_lv loc_lv v writes v at loc_lv in state, casting v to respect the type typ_lv of lv.
written_formals [Backward_formals]
written_formals kf is an over-approximation of the formals of kf which may be internally overwritten by kf during its call.

Z
zero [Abstract_value.S]
zero [Gauges_domain.G.Bounds]
zero [Value_util]
Retun a zero constant compatible with the type of the argument
zone_of_expr [Value_util]
Given a function computing the location of lvalues, computes the memory zone on which the value of an expression depends.