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.

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 [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_base [Lmap_bitwise.Location_map_bitwise]
add_binding [Cvalue.Model]
add_binding state loc v simulates the effect of writing v at location loc in state.
add_binding [Lmap_bitwise.Location_map_bitwise]
add_binding [Eval_op]
Temporary.
add_binding_loc [Lmap_bitwise.Location_map_bitwise]
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_num_hints [Widen_type]
Add numeric hints for one or all variables (None), for a a certain stmt or for all statements (None).
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.
add_var_hints [Widen_type]
Add a set of bases to widen in priority for a given statement.
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_values [Abstract_value.S]
Creates all abstract values corresponding to the given type.
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 lv expr v valuation state is the transfer function for the assignment lv = expr in state.
assign [Transfer_stmt.S]
assume [Abstract_domain.Transfer]
Transfer function for an assumption.
assume [Transfer_stmt.S]

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_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]
call [Transfer_stmt.S]
call_action [Abstract_domain.Transfer]
Decision on a function call: call_action stmt call valuation state decides on the analysis of the called function; see for details on the action type, which described the analysis.
call_action [Cvalue_transfer.Transfer]
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 [Cvalue_forward]
If needed, cast the given abstract value to the given size.
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_pre_post [Gui_eval]
State in which the predicate, found in the given function, should be evaluated
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 [Lmap_bitwise.Location_map_bitwise]
Clear the caches local to this module.
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_expr [Eval.Clear_Valuation]
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.
close_block [Abstract_domain.S]
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 [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 [Partitioned_dataflow.Computer]
compute [Eval_slevel.Computer]
compute [Mem_lvalue]
Create a new project in which repeated lvalues are accessed through a temporary.
compute_actual [Function_args]
compute_call_ref [Transfer_stmt.S]
compute_call_ref [Eval_stmt]
compute_non_linear [Eval_non_linear]
compute_using_specification [Abstract_domain.S]
compute_using_specification_multiple_behaviors [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.
compute_using_specification_single_behavior [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_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.
current_kf [Value_util]
The current function is the one on top of the call stack.
current_stmt [Alarmset]
current_stmt [Valarms]
curstate [Value_messages]
cvalue_initial_state [Compute_functions]
Compute the initial state of the cvalue domain only.
cvalue_key [Main_values]
Key for cvalues.

D
debug [Equality_term.Atom]
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_config [Abstractions]
Default configuration of EVA.
default_offsetmap [Cvalue.Default_offsetmap]
diff [Equality_sig.Set]
display [Value_perf]
Display a complete summary of performance informations.
distinct_subpart [Cvalue_domain]
div [Cvalue.V]
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]
dump_state [Builtins]
Builtins with multiple names; the lookup is done using a distinctive prefix
dump_state_file [Builtins]

E
elements [Equality_sig.S]
Return the list of all elements of the given equality.
elements [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 [Lmap_bitwise.Location_map_bitwise]
empty [Eval.Valuation]
empty [State_imp]
Creation
empty [State_set]
Creation
empty_map [Lmap_bitwise.Location_map_bitwise]
end_stmt [Alarmset]
end_stmt [Valarms]
enumerate_valid_bits [Precise_locs]
env_annot [Abstract_domain.Logic]
env_annot [Eval_terms]
env_assigns [Eval_terms]
env_current_state [Abstract_domain.Logic]
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 [Eval_terms]
env_pre_f [Abstract_domain.Logic]
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 [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 [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_lval [Eval_exprs]
eval_predicate [Abstract_domain.Logic]
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 [Non_linear_evaluation.Make]
Same functionality as Eva.evaluate.
evaluate [Evaluation.S]
evaluate ~valuation ~indeterminate state exp evaluates the expression exp in the state state, and returns the pair res, alarms, where: alarms are the set of alarms ensuring the soundness of the evaluation;, res is either `Bottom if the evaluation is impossible, or `Value (valuation, value), where value is the numeric value computed for exp, and valuation contains all the intermediate results of the evaluation. About optional arguments:, valuation is a cache of already computed expressions; empty by default., if indeterminate is true, then the lvalues uninitialized or escaping are considered as unreduced (their reductness is not set to Reduced); false by default.
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_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.

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 [Eval.Valuation]
filter_base [Lmap_bitwise.Location_map_bitwise]
filter_by_bases [Abstract_domain.S]
Mem exec.
filter_by_bases [Mem_exec2.Domain]
filter_if [Separate]
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 [Lmap_bitwise.Location_map_bitwise]
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_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.
fix [Equality_term.Atom]
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 [Lmap_bitwise.Location_map_bitwise]
The following fold_* functions, as well as Lmap_bitwise.Location_map_bitwise.map2 take arguments of type map to force their user to handle the cases Top and Bottom explicitly.
fold [Eval.Valuation]
fold [Hashtbl.S]
fold [State_imp]
Iterators
fold [State_builder.Hashtbl]
fold [State_set]
Iterators
fold2_join_heterogeneous [Hptset.S]
fold_base [Lmap_bitwise.Location_map_bitwise]
fold_fuse_same [Lmap_bitwise.Location_map_bitwise]
Same behavior as fold, except if two non-contiguous ranges r1 and r2 of a given base are mapped to the same value.
fold_join_zone [Lmap_bitwise.Location_map_bitwise]
fold_join_zone ~both ~conv ~empty_map ~join ~empty z m folds over the intervals present in z.
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 [Compute_functions]
Perform a full analysis, starting from the main function.
force_compute [Eval_funs]
Perform a full analysis, starting from the main function.
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.
from_callstack [Gui_callstacks_filters]
from_shape [Hptset.S]
Build a set from another elt-indexed map or set.

G
get [Abstract_domain.External]
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 [Equality_term.Atom]
get [Structure.External]
get [State_builder.Ref]
Get the referenced value.
getWidenHints [Widen]
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_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_v [Cvalue.V_Or_Uninitialized]
global_state [Abstract_domain.S]
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 [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 [Equality_term.Atom]
imprecise_location [Precise_locs]
imprecise_location_bits [Precise_locs]
imprecise_offset [Precise_locs]
imprecise_write_msg [Lmap_bitwise.Location_map_bitwise]
incr [Stop_at_nth]
incr [Parameter_sig.Int]
Increment the integer.
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_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 [Initial_state]
initialized [Cvalue.V_Or_Uninitialized]
initialized v returns the definitely initialized, non-escaping representant of v.
inject [Cvalue_domain]
inject_comp_result [Cvalue.V]
inject_int [Cvalue.V]
inject_int [Abstract_value.S]
inject_ival [Precise_locs]
inject_location_bits [Precise_locs]
inter [Equality_sig.S]
Intersection.
inter [Equality_sig.Set]
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]
intersect [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.
is_active [Eval_annots.ActiveBehaviors]
is_active_aux [Eval_annots.ActiveBehaviors]
is_alive [Equality_term.Atom]
Utilitaries
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 [Lmap_bitwise.Location_map_bitwise]
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 [Lmap_bitwise.Location_map_bitwise]
is_empty [Alarmset]
Is there an assertion with a non True status ?
is_empty [State_imp]
Information
is_empty [State_set]
Information
is_fix [Equality_term.Atom]
is_imprecise [Cvalue.V]
is_included [Abstract_domain.Lattice]
Inclusion test.
is_included [Abstract_value.S]
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_old [Equality_term.Atom]
is_reachable_stmt [Gui_callstacks_filters]
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 [Abstract_domain.Lattice]
Semi-lattice structure.
join [Abstract_value.S]
join [Partitioning.Partition]
join [Partitioning.StateSet]
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 [Abstract_value.S]
join_final_states [Split_return]
Join the given state_set.
join_gui_offsetmap_res [Gui_types]
join_list [Alarmset.Status]
join_list_predicate_status [Eval_terms]
join_predicate_status [Eval_terms]

K
key [Cvalue_domain]
key [Equality_domain.S]
kf_of_gui_loc [Gui_types]
kf_strategy [Split_return]
ki_of_callstack [Value_messages]

L
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]
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]
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 [Equality_term.Atom]
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_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 [Value_util]
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 [Lmap_bitwise.Location_map_bitwise]
map [State_set]
map2 [Cvalue.V_Or_Uninitialized]
initialized/escaping information is the join of the information on each argument.
map2 [Lmap_bitwise.Location_map_bitwise]
'map'-like function between two interval maps, implemented as a simultaneous descent in both maps.
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.External]
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]

N
narrow [Cvalue.V_Offsetmap]
narrow [Abstract_value.S]
narrow [State_set]
narrow_list [State_set]
need_cast [Eval_typ]
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]

O
octagon_key [Apron_domain]
of_char [Cvalue.V]
of_exp [Equality_term.Atom]
of_int64 [Cvalue.V]
of_list [Partitioning.StateSet]
of_list [State_set]
of_list_forget_history [State_set]
of_lval [Equality_term.Atom]
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?
old [Equality_term.Atom]
on [Parameter_sig.Bool]
Set the boolean to true.
one [Cvalue.CardinalEstimate]
open_block [Abstract_domain.S]
Scoping: abstract transformers for entering and exiting blocks.
output [Parameter_sig.With_output]
To be used by the plugin to output the results of the option in a controlled way.
overridden_by_builtin [Builtins]
Should the given function be replaced by a call to a builtin

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]
predicate_deps [Eval_terms]
predicate_ev [Gui_eval]
pretty [Cvalue.CardinalEstimate]
pretty [Partitioning.Partition]
pretty [Partitioning.StateSet]
pretty [Alarmset]
pretty [State_imp]
pretty [State_set]
pretty_actuals [Value_util]
pretty_call_stack [Value_util]
pretty_call_stack_short [Value_util]
Print a call stack.
pretty_callstack [Gui_types]
pretty_callstack_short [Gui_types]
pretty_current_cfunction_name [Value_util]
pretty_debug [Equality_domain.S]
pretty_debug [Equality.Element]
pretty_debug [Lmap_bitwise.Location_map_bitwise]
pretty_debug [Equality_term.Atom]
pretty_generic_printer [Lmap_bitwise.Location_map_bitwise]
pretty_gui_offsetmap_res [Gui_types]
pretty_gui_res [Gui_types]
pretty_gui_selection [Gui_types]
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_offset [Precise_locs]
pretty_offset [Abstract_location.S]
pretty_predicate_status [Eval_terms]
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_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
reborn [Equality_term.Atom]
reduce [Abstractions.Value]
reduce [Evaluation.Value]
Inter-reduction of values.
reduce [Evaluation.S]
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 [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_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_malloced_base [Value_util]
These two functions are used to model the calls to malloc and free correctly.
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.
reinterpret_int [Eval_op]
Read the given value value as an int of the given ikind.
release [Equality_term.Atom]
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 [Hashtbl.S]
remove [State_builder.Hashtbl]
remove_base [Lmap_bitwise.Location_map_bitwise]
remove_indeterminateness [Cvalue.V_Or_Uninitialized]
Remove 'unitialized' and 'escaping addresses' flags from the argument
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_call [Abstract_domain.Transfer]
resolve_call stmt ~assigned_lv call valuation ~pre_state ~post_state compute the state after the statement stmt where the lvalue assigned is assigned to the result of the call call.
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_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.

S
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 [Equality_term.Atom]
set [Abstract_domain.External]
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 [Lmap_bitwise.Location_map_bitwise]
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_doing [Value_perf]
start_stmt [Alarmset]
start_stmt [Valarms]
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]
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.
structural_descr [Locals_scoping]
structure [Abstract_domain.Internal]
A structure matching the type of the domain.
structure [Abstract_location.Internal]
structure [Abstract_value.Internal]
structure [Structure.Internal]
sub_untyped_pointwise [Cvalue.V]
See Locations.sub_pointwise.
subset [Equality_sig.S]
subset [Equality_sig.Set]
subst [Equality_sig.S]
subst [Equality_sig.Set]
summarize [Abstract_domain.Transfer]
summarize kf stmt ~returned_lv state returns a summary of the state state at the end of the function kf.

T
tag [Structure.Key]
term_ev [Gui_eval]
terms [Equality_sig.Set]
terms set return the list of elements of equality of set.
tlval_ev [Gui_eval]
tlval_zone_ev [Gui_eval]
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 [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]

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 [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 cached in valuation.

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]
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.
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 [Value_util]
Over-approximation of its formals the given function may write into.

Z
zero [Abstract_value.S]
zero [Value_util]
Retun a zero constant compatible with the type of the argument