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_behaviors [Transfer_logic.ActiveBehaviors]
add [FCMap.S]

add x y m returns a map containing the same bindings as m, plus a binding of x to y.

add [Powerset.S]
add [Equality.Equality]

add x s returns the equality between all elements of s and x.

add [Hcexprs.BaseToHCESet]
add [Hcexprs.HCEToZone]
add [Simple_memory.S]

add loc typ v state binds loc to v in state.

add [Eval.Valuation]
add [State_builder.Hashtbl]

Add a new binding.

add' [Powerset.S]
add_binding [Cvalue.Model]

add_binding state loc v simulates the effect of writing v at location loc in state.

add_indeterminate_binding [Cvalue.Model]
add_kf_caller [Value_results]
add_red_alarm [Red_statuses]
add_red_property [Red_statuses]
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 status associated to Value_parameters.wkey_alarm

all [Alarmset]

all alarms: all potential assertions have a Unknown status.

all_values [Cvalue.V]

all_values ~size v returns true iff v contains all integer values representable in size bits.

alloc_size_ok [Builtins_malloc]
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.

approximate_call [Simpler_domains.Simple_Cvalue]
approximate_call [Simpler_domains.Minimal]
approximate_call [Abstract_domain.Transfer]
are_comparable [Cvalue_forward]
assign [Simpler_domains.Simple_Cvalue]
assign [Simpler_domains.Minimal]
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]
assume [Simpler_domains.Simple_Cvalue]
assume [Simpler_domains.Minimal]
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.

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_false [Cvalue.V]
backward_comp_float_left_true [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_mult_int_left [Cvalue.V]
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]
bindings [FCMap.S]

Return the list of all bindings of the given map.

bitwise_and [Cvalue.V]
bitwise_not [Cvalue.V]
bitwise_not_size [Cvalue.V]
bitwise_or [Cvalue.V]
bitwise_xor [Cvalue.V]
bottom [Locals_scoping]
bottom [Eval.Flagged_Value]
bottom_location_bits [Precise_locs]
box_key [Apron_domain]
builtins [Simple_memory.Value]

A list of builtins for the domain: each builtin is associated with the name of the C function it interprets.

C
c_labels [Eval_annots]
c_rem [Cvalue.V]
call [Transfer_stmt.S]
call_stack [Value_util]
callsite_matches [Gui_callstacks_filters]
callstack_matches [Gui_callstacks_filters]
cardinal [FCMap.S]

Return the number of bindings of a map.

cardinal [Equality.Set]
cardinal [Equality.Equality]

Return the number of elements of the equality.

cardinal_estimate [Cvalue.Model]
cardinal_estimate [Cvalue.V]

cardinal_estimate v ~size returns an estimation of the cardinal of v, knowing that v fits in size bits.

cardinal_zero_or_one [Precise_locs]

Should not be used, Precise_locs.valid_cardinal_zero_or_one is almost always more useful

cast [Abstract_value.S]

Abstract evaluation of casts operators from scr_typ to dst_typ.

cast [Offsm_value]
cast [Cvalue_forward]
cast_float_to_float [Cvalue.V]
cast_float_to_int [Cvalue.V]
cast_float_to_int_alarms [Cvalue_forward]
cast_float_to_int_inverse [Cvalue.V]
cast_int_to_float [Cvalue.V]
cast_int_to_float_inverse [Cvalue.V]
cast_int_to_int [Cvalue.V]

cast_int_to_int ~size ~signed v applies to the abstract value v the conversion to the integer type described by size and signed.

change_callstacks [Value_results]

Change the callstacks for the results for which this is meaningful.

change_callstacks [Value.Value_results]
check_fct_postconditions [Transfer_logic.S]
check_fct_postconditions_for_behaviors [Transfer_logic.S]
check_fct_preconditions [Transfer_logic.S]
check_fct_preconditions_for_behaviors [Transfer_logic.S]
check_non_overlapping [Abstract_location.S]

Needed for unspecified sequences.

check_non_overlapping [Evaluation.S]
check_unspecified_sequence [Transfer_stmt.S]
choose [FCMap.S]

Return one binding of the given map, or raise Not_found if the map is empty.

choose [Equality.Set]
choose [Equality.Equality]

Return the representative of the equality.

classify_as_scalar [Eval_typ]
classify_pre_post [Gui_eval]

State in which the predicate, found in the given function, should be evaluated

cleanup_results [Mem_exec]

Clean all previously stored results

clear [State_builder.Hashtbl]

Clear the table.

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_default [Gui_callstacks_manager]
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.

combine [Alarmset]

Combines two alarm maps carrying different sets of alarms.

combine_base_precise_offset [Precise_locs]
combine_loc_precise_offset [Precise_locs]
compare [FCMap.S]

Total ordering between maps.

compare [Simpler_domains.Minimal]
compare [Equality.Set]
compare [Equality.Equality]
compare [Structure.Key]
compare_gui_callstack [Gui_types]
compatible_functions [Eval_typ]
compute [Partitioned_dataflow.Computer]
compute_call_ref [Transfer_stmt.S]
compute_from_entry_point [Analysis.Make]
compute_from_entry_point [Compute_functions.Make]

Compute a call to the main function.

compute_from_init_state [Analysis.Make]
compute_from_init_state [Compute_functions.Make]

Compute a call to the main function from the given initial state.

compute_using_specification [Transfer_specification.Make]
configure [Abstractions]

Build a configuration according to the analysis parameters.

constant [Abstract_value.S]

Embeds C constants into value abstractions: returns an abstract value for the given constant.

contains [Equality.Set]

contains elt set = true iff elt belongs to an equality of set.

contains_non_zero [Cvalue.V]
contains_single_elt [Hptset.S]
contains_zero [Cvalue.V]
conv_comp [Value_util]
conv_relation [Value_util]
copy [Datatype.S]

Deep copy: no possible sharing between x and copy x.

copy_lvalue [Analysis.Results]
copy_lvalue [Evaluation.S]

Computes the value of a lvalue, with possible indeterminateness: the returned value may be uninitialized, or contain escaping addresses.

create [Gui_callstacks_manager]

Creates the panel, attaches it to the lower notebook, and returns the display_by_callstack function allowing to display data on it.

create [Transfer_logic.S]
create [Transfer_logic.ActiveBehaviors]
create_all_values [Cvalue.V]
create_from_spec [Transfer_logic.S]
create_key [Structure.Key]
create_new_var [Value_util]

Create and register a new variable inside Frama-C.

current_analyzer [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]
cvalue_initial_state [Analysis]

Return the initial state of the cvalue domain only.

cvalue_key [Main_values]

Key for cvalues.

D
deep_fold [Equality.Set]
default [Widen_type]

A default set of hints

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]
dkey [Widen_hints_ext]
dkey_cvalue_domain [Value_parameters]

Debug category used to print the cvalue domain on Frama_C_dump|show_each functions.

dkey_final_states [Value_parameters]
dkey_garbled_mix [Value_parameters]

Debug category used to print garbled mix

dkey_incompatible_states [Value_parameters]
dkey_initial_state [Value_parameters]

Debug categories responsible for printing initial and final states of Value.

dkey_pointer_comparison [Value_parameters]

Debug category used to print information about invalid pointer comparisons

dump_garbled_mix [Value_util]

print information on the garbled mix created during evaluation

E
elements [Equality.Set]
emit [Alarmset]

Emits the alarms according to the given warn mode, at the given instruction.

emitter [Value_util]
empty [Gui_callstacks_filters]
empty [FCMap.S]

The empty map.

empty [Widen_type]

An empty set of hints

empty [Simpler_domains.Simple_Cvalue]
empty [Simpler_domains.Minimal]
empty [Abstract_domain.S]

The initial state with which the analysis start.

empty [Partitioning.S]
empty [Powerset.S]
empty [Equality.Set]
empty [Hcexprs.BaseToHCESet]
empty [Hcexprs.HCEToZone]
empty [Eval.Valuation]
empty_lvalues [Hcexprs]
empty_spec_for_recursive_call [Recursion]

Generate an empty spec assigns \nothing or assigns \result \from \nothing, to be used to "approximate" the results of a recursive call.

enter_loop [Abstract_domain.S]
enter_scope [Simpler_domains.Simple_Cvalue]
enter_scope [Simpler_domains.Minimal]
enter_scope [Abstract_domain.S]

Scoping: abstract transformers for entering and exiting blocks.

enter_scope [Transfer_stmt.S]
enumerate_valid_bits [Precise_locs]
env_annot [Eval_terms]
env_assigns [Eval_terms]
env_current_state [Eval_terms]
env_only_here [Eval_terms]

Used by auxiliary plugins, that do not supply the other states

env_post_f [Eval_terms]
env_pre_f [Eval_terms]
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 [Hashtbl.HashedType]

The equality predicate used to compare keys.

equal [Transfer_logic.LogicDomain]
equal [Equality.Set]
equal [Equality.Equality]
equal [Structure.Key]
equal [Eval.Flagged_Value]
equal [Alarmset]

Are two maps equal?

equal_gui_after [Gui_types.S]
equal_gui_offsetmap_res [Gui_types]
equal_gui_res [Gui_types.S]
equal_loc [Precise_locs]
equal_loc [Abstract_location.S]
equal_offset [Precise_locs]
equal_offset [Abstract_location.S]
eval_expr [Analysis.Results]
eval_float_constant [Cvalue_forward]
eval_function_exp [Analysis.Results]
eval_function_exp [Evaluation.S]

Evaluation of the function argument of a Call constructor

eval_lval_to_loc [Analysis.Results]
eval_precond [Cvalue_transfer]
eval_predicate [Eval_terms]
eval_term [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_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.

evaluate [Subdivided_evaluation.Forward_Evaluation]
evaluate [Subdivided_evaluation.Make]
evaluate_assumes_of_behavior [Transfer_logic.S]
evaluate_predicate [Abstract_domain.S]

Evaluates a predicate to a logical status in the current state.

evaluate_predicate [Transfer_logic.LogicDomain]
exists [FCMap.S]

exists p m checks if at least one binding of the map satisfy the predicate p.

exists [Equality.Set]
exists [Equality.Equality]

exists p s checks if at least one element of the equality satisfies the predicate p.

exists [Alarmset]
exists [Parameter_sig.Set]

Is there some element satisfying the given predicate?

exp_ev [Gui_eval.S]
expr_contains_volatile [Eval_typ]
extend_loc [Domain_lift.Conversion]
extend_val [Domain_lift.Conversion]
extend_val [Location_lift.Conversion]
extract [Cvalue_domain]
extract_expr [Simpler_domains.Simple_Cvalue]
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 [Simpler_domains.Simple_Cvalue]
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.Equality]

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_exec.Domain]
finalize_call [Simpler_domains.Simple_Cvalue]
finalize_call [Simpler_domains.Minimal]
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.

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.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]
find [Hcexprs.HCEToZone]
find [Simple_memory.S]

find loc typ state returns the join of the abstract values stored in the locations abstracted to by loc in state, assuming the result has type typ.

find [Eval.Valuation]
find [Alarmset]

Returns the status of a given alarm.

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 [State_builder.Hashtbl]

Return the list of all data associated with the given key.

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_indeterminate [Cvalue.Model]

find_indeterminate ~conflate_bottom state loc returns the value and flags associated to loc in state.

find_loc [Abstract_domain.Valuation]
find_loc [Eval.Valuation]
find_opt [FCMap.S]

find x m returns the current binding of x in m, or return None if no such binding exists.

find_option [Equality.Set]

Same as find, but return None in the last case.

find_subpart [Cvalue_domain]
float_zeros [Abstract_value.S]
focus_on_callstacks [Gui_callstacks_filters]
focus_selection_tab [Gui_callstacks_manager]
focused_callstacks [Gui_callstacks_filters]
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 [Abstract_domain.Valuation]
fold [Powerset.S]
fold [Equality.Set]
fold [Equality.Equality]

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s, in increasing order.

fold [Simple_memory.S]

Fold on base value pairs.

fold [Eval.Valuation]
fold [State_builder.Hashtbl]
fold2_join_heterogeneous [Hptset.S]
fold_dynamic_bases [Builtins_malloc]

fold_dynamic_bases f init folds f to each dynamically allocated base, with initial accumulator init.

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.Set]
for_all [Equality.Equality]

for_all p s checks if all elements of the equality satisfy the predicate p.

for_all [Alarmset]
force_compute [Analysis]

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_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]
frama_c_wcschr_wrapper [Builtins_string]
frama_c_wcslen_wrapper [Builtins_string]
frama_c_wmemchr_wrapper [Builtins_string]
free_automatic_bases [Builtins_malloc]

Performs the equivalent of free for each location that was allocated via alloca() in the current function (as per Value_util.call_stack ()).

freeable [Builtins_malloc]

Evaluates the ACSL predicate \freeable(value): holds if and only if the value points to an allocated memory block that can be safely released using the C function free.

from_callstack [Gui_callstacks_filters]
from_cvalue [Gui_types.Make]
from_shape [Hptset.S]

Build a set from another elt-indexed map or set.

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_all [Red_statuses]
get_cvalue [Gui_types.Make]
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_global_state [Abstract_domain.Store]
get_initial_state [Abstract_domain.Store]
get_initial_state_by_callstack [Analysis.Results]
get_initial_state_by_callstack [Abstract_domain.Store]
get_kinstr_state [Analysis.Results]
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.

get_slevel [Value_util]
get_stmt_state [Analysis.Results]
get_stmt_state [Abstract_domain.Store]
get_stmt_state_by_callstack [Analysis.Results]
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]
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
has_requires [Eval_annots]
hash [Simpler_domains.Minimal]
hash [Hashtbl.HashedType]

A hashing function on keys.

hash [Structure.Key]
hash_gui_callstack [Gui_types]
height_expr [Value_util]

Computes the height of an expression, that is the maximum number of nested operations in this expression.

height_lval [Value_util]

Computes the height of an lvalue.

hints_from_keys [Widen_type]

Widen hints for a given statement, suitable for function Cvalue.Model.widen.

I
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]
incr [Parameter_sig.Int]

Increment the integer.

incr_loop_counter [Abstract_domain.S]
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 [Compute_functions.Make]
initial_state [Initialization.S]

Compute the initial state for an analysis.

initial_state_with_formals [Initialization.S]

Compute the initial state for an analysis (as in Initialization.S.initial_state), but also bind the formal parameters of the function given as argument.

initialize_local_variable [Initialization.S]

Initializes a local variable in the current state.

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_variable [Simpler_domains.Simple_Cvalue]
initialize_variable [Simpler_domains.Minimal]
initialize_variable [Abstract_domain.S]

initialize_variable lval loc ~initialized init_value state initializes the value of the location loc of lvalue lval in state with: bits 0 if init_value = Zero;, any bits if init_value = Top. The boolean initialized is true if the location is initialized, and false if the location may be not initialized.

initialize_variable_using_type [Abstract_domain.S]

Initializes a variable according to its type.

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_float [Cvalue.V]
inject_int [Cvalue.V]
inject_int [Abstract_value.S]
inject_ival [Precise_locs]
inject_location_bits [Precise_locs]
inter [Equality.Set]
inter [Equality.Equality]

Intersection.

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_boolean [Cvalue.V]
intersects [Equality.Equality]

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.

introduce_globals [Simpler_domains.Simple_Cvalue]
introduce_globals [Simpler_domains.Minimal]
introduce_globals [Abstract_domain.S]

Introduces the list of global variables in the state.

is_active [Transfer_logic.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_dynamic [Widen_hints_ext]

is_dynamic wh returns true iff widening hint wh has a "dynamic" prefix.

is_empty [FCMap.S]

Test whether a map is empty or not.

is_empty [Powerset.S]
is_empty [Equality.Set]
is_empty [Alarmset]

Is there an assertion with a non True status ?

is_global [Widen_hints_ext]

is_global wh returns true iff widening hint wh has a "global" prefix.

is_imprecise [Cvalue.V]
is_included [Simpler_domains.Simple_Cvalue]
is_included [Simpler_domains.Minimal]
is_included [Abstract_domain.Lattice]

Inclusion test.

is_included [Abstract_value.S]
is_included [Hcexprs.HCEToZone]
is_included [Simple_memory.Value]
is_included [Simple_memory.Make_Memory]
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_lval [Hcexprs.HCE]
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_recursive_call [Recursion]

Given the current state of the call stack, detect whether the given given function would start a recursive cycle.

is_red_in_callstack [Red_statuses]
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.normalize_as_cond

iter [FCMap.S]

iter f m applies f to all bindings in map m.

iter [Powerset.S]
iter [Equality.Set]
iter [Equality.Equality]

iter f s applies f in turn to all elements of s.

iter [Alarmset]
iter [State_builder.Hashtbl]
iter_sorted [State_builder.Hashtbl]
J
join [Widen_type]
join [Simpler_domains.Simple_Cvalue]
join [Simpler_domains.Minimal]
join [Abstract_domain.Lattice]

Semi-lattice structure.

join [Abstract_value.S]
join [Partitioning.S]
join [Powerset.S]
join [Simple_memory.Value]
join [Simple_memory.Make_Memory]
join [Eval.Flagged_Value]
join [Alarmset.Status]
join_gui_offsetmap_res [Gui_types]
join_list [Alarmset.Status]
join_predicate_status [Eval_terms]
K
key [Cvalue_domain]
key [Inout_domain]
key [Equality_domain.Make]
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]
L
leave_loop [Abstract_domain.S]
leave_scope [Simpler_domains.Simple_Cvalue]
leave_scope [Simpler_domains.Minimal]
leave_scope [Abstract_domain.S]
legacy_config [Abstractions]

Legacy configuration of Eva, with only the cvalue domain enabled.

length [Powerset.S]
length [State_builder.Hashtbl]

Length of the table.

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_top [Precise_locs]
local [Per_stmt_slevel]

Slevel to use in this function

log_category [Abstract_domain.S_with_Structure]

Category for the messages about the domain.

logic_assign [Abstract_domain.S]

logic_assign from loc_asgn pre state applies the effect of the assigns ... \from ... clause from to state.

lval_as_offsm_ev [Gui_eval.S]
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.S]
lval_to_exp [Value_util]

This function is memoized to avoid creating too many expressions

lval_zone_ev [Gui_eval.S]
lvaluate [Evaluation.S]

lvaluate ~valuation ~for_writing state lval evaluates the left value lval in the state state.

lvalues_only_left [Equality.Set]
M
make [Cvalue.V_Or_Uninitialized]
make [Abstractions]

Builds the abstractions according to a configuration.

make [Main_locations.PLoc]
make_data_all_callstacks [Gui_eval.S]
make_data_for_lvalue [Gui_callstacks_manager.Input]
make_env [Eval_terms]
make_escaping [Locals_scoping]

make_escaping ~exact ~escaping ~on_escaping ~within state changes all references to the variables in escaping to "escaping address".

make_escaping_fundec [Locals_scoping]

make_escaping_fundec fdec clob l state changes all references to the local or formal variables in l to "escaping".

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_panel [Gui_red]

Add a tab to the main GUI (for red alarms), and return its widget.

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.

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 [Powerset.S]
map2 [Cvalue.V_Or_Uninitialized]

initialized/escaping information is the join of the information on each argument.

map_or_bottom [Powerset.S]
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_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.

mem [FCMap.S]

mem x m returns true if m contains a binding for x, and false otherwise.

mem [Abstract_domain.Interface]

Tests whether a key belongs to the domain.

mem [Equality.Set]

mem equality set = true iff ∃ eq ∈ set, equality ⊆ eq

mem [Equality.Equality]

mem x s tests whether x belongs to the equality s.

mem [Structure.External]
mem [State_builder.Hashtbl]
mem [Parameter_sig.Set]

Does the given element belong to the set?

mem [Parameter_sig.Map]
mem_builtin [Builtins]

Does the builtin table contain an entry for name?

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 [Powerset.S]
merge [Value_results]
merge [Hptset.S]
merge [Per_stmt_slevel]

Slevel merge strategy for this function

merge [Value.Value_results]
merge_set_return_new [Partitioning.S]
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.

mul [Cvalue.V]
N
name [Simpler_domains.Minimal]
narrow [Cvalue.V_Offsetmap]
narrow [Abstract_domain.Lattice]

Over-approximation of the intersection of two abstract states (called meet in the literature).

narrow [Abstract_value.S]
narrow [Simple_memory.Value]
narrow_reinterpret [Cvalue.V_Offsetmap]

See the corresponding functions in Offsetmap_sig.

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.

new_counter [Mem_exec]

Counter that must be used each time a new call is analyzed, in order to refer to it later

no_memoization_enabled [Mark_noresults]
no_offset [Abstract_location.S]
none [Alarmset]

no alarms: all potential assertions have a True status.

normalize_as_cond [Value_util]

normalize_as_cond e positive returns the expression corresponding to e != 0 when positive is true, and e == 0 otherwise.

notify [Alarmset]

Calls the functions registered in the warn_mode according to the set of alarms.

null_ev [Gui_eval.S]
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 [Powerset.S]
of_lval [Hcexprs.HCE]
of_string [Split_strategy]
off [Parameter_sig.Bool]

Set the boolean to false.

offset_bottom [Precise_locs]
offset_top [Precise_locs]
offset_zero [Precise_locs]
offsetmap_contains_local [Locals_scoping]
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_loc [Eval_op]

Returns the offsetmap at a precise_location from a state.

offsetmap_of_v [Eval_op]

Transformation a value into an offsetmap of size sizeof(typ) bytes.

offsm_key [Offsm_value]
ok [Apron_domain]

Are apron domains available?

on [Parameter_sig.Bool]

Set the boolean to true.

one [Cvalue.CardinalEstimate]
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.Equality]

The equality between two elements.

parameters_abstractions [Value_parameters]
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.

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_analysis [Abstract_domain.Internal]

This function is called after the analysis.

postconditions_mention_result [Value_util]

Does the post-conditions of this specification mention \result?

pp_callstack [Value_util]

Prints the current callstack.

pp_hvars [Widen_hints_ext]
precompute_widen_hints [Widen]

Parses all widening hints defined via the widen_hint syntax extension.

predicate_deps [Eval_terms]
predicate_ev [Gui_eval.S]
predicate_with_red [Gui_eval.S]
pretty [Widen_type]

Pretty-prints a set of hints (for debug purposes only).

pretty [Cvalue.CardinalEstimate]
pretty [Simpler_domains.Minimal]
pretty [Partitioning.S]
pretty [Powerset.S]
pretty [Eval.Flagged_Value]
pretty [Alarmset]
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.Make]
pretty_debug [Hptset.S]
pretty_debug [Hcexprs.HCE]
pretty_debug [Simple_memory.Value]

Can be equal to pretty

pretty_debug [Sign_value]
pretty_gui_after [Gui_types.S]
pretty_gui_offsetmap_res [Gui_types]
pretty_gui_res [Gui_types.S]
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_offsetmap [Eval_op]
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_status [Alarmset]
pretty_stitched_offsetmap [Eval_op]
pretty_strategies [Split_return]
pretty_typ [Cvalue.V]
pretty_typ [Abstract_value.S]

Pretty the abstract value assuming it has the type given as argument.

print [Structure.Key]
process_inactive_behaviors [Transfer_logic]
product_category [Domain_product]
project [Cvalue_domain]
project [Equality_domain.Make]
project_float [Cvalue.V]

Raises Not_based_on_null if the value may be a pointer.

project_ival [Cvalue.V]

Raises Not_based_on_null if the value may be a pointer.

project_ival_bottom [Cvalue.V]
push_call_stack [Value_util]
R
range_inclusion [Eval_typ]

Checks 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 expression 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_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_enumeration [Subdivided_evaluation.Make]
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.S]

reduce_by_predicate env state pred b reduces the current state by assuming that the predicate pred evaluates to b.

reduce_by_predicate [Transfer_logic.LogicDomain]
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 interval 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.

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_dynamic_abstraction [Abstractions]
register_global_state [Abstract_domain.Store]
register_hook [Analysis]

Registers a hook that will be called each time the current analyzer is changed.

register_initial_state [Abstract_domain.Store]
register_state_after_stmt [Abstract_domain.Store]
register_state_before_stmt [Abstract_domain.Store]
register_to_zone_functions [Gui_callstacks_filters]
registered_builtins [Builtins]

Returns a list of the pairs (name, builtin_sig) registered via register_builtin.

reinterpret [Cvalue_forward]
reinterpret_as_float [Cvalue.V]
reinterpret_as_int [Cvalue.V]
remember_bases_with_locals [Locals_scoping]

Add the given set of bases to an existing clobbered set

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

remove lval set remove any expression e such that lval belongs to syntactic_lval e from the set of equalities set.

remove [Equality.Equality]

remove x s returns the equality between all elements of s, except x.

remove [Hcexprs.BaseToHCESet]
remove [Hcexprs.HCEToZone]
remove [Simple_memory.S]

remove loc state drops all information on the locations pointed to by loc from state.

remove [Eval.Valuation]
remove [State_builder.Hashtbl]
remove_indeterminateness [Cvalue.V_Or_Uninitialized]

Remove 'uninitialized' 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.

remove_variables [Simple_memory.S]

remove_variables list state drops all information about the variables in list from state.

reorder [Powerset.S]
replace [Hcexprs.HCE]

Replaces all occurrences of the lvalue late by the expression heir.

replace [State_builder.Hashtbl]

Add a new binding.

replace_val [Location_lift.Conversion]
reset [Gui_callstacks_manager]
reset [Value_perf]

Reset the internal state of the module; to call at the very beginning of the analysis.

resolve_functions [Abstract_value.S]

resolve_functions v returns the list of functions that may be pointed to by the abstract value v (representing a function pointer).

restrict_float [Abstract_value.S]

restrict_float expr fkind t removes NaN from the abstract value t.

restrict_float [Cvalue_forward]
restrict_loc [Domain_lift.Conversion]
restrict_val [Domain_lift.Conversion]
restrict_val [Location_lift.Conversion]
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.

returned_value [Library_functions]
reuse [Abstract_domain.S]
reuse [Mem_exec.Domain]
reuse_previous_call [Mem_exec.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.

rewrap_integer [Abstract_value.S]

rewrap_integer irange t wraps around the abstract value t to fit the integer range irange.

rewrap_integer [Cvalue_forward]
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.

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 [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 [Alarmset]

set alarm status t binds the alarm to the status in the map t.

set [State_builder.Ref]

Change the referenced value.

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]
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]
show_expr [Simpler_domains.Simple_Cvalue]

Pretty printer.

show_expr [Simpler_domains.Minimal]
show_expr [Abstract_domain.Transfer]

Called on the Frama_C_show_each directives.

sign_key [Sign_value]
signal_abort [Partitioned_dataflow]

Mark the analysis as aborted.

singleton [FCMap.S]

singleton x y returns the one-element map that contains a binding y for x.

singleton [Powerset.S]
singleton [Alarmset]

singleton ?status alarm creates the map set alarm status none: alarm has a by default an unkown status (which can be overridden through status), and all others have a True status.

singleton' [Powerset.S]
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.

skip_specifications [Value_util]

Should we skip the specifications of this function, according to -val-skip-stdlib-specs

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_final_states [Transfer_stmt.S]
start_call [Simpler_domains.Simple_Cvalue]
start_call [Simpler_domains.Minimal]
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_doing [Value_perf]
stop_doing [Value_perf]

Call start_doing when finishing analyzing a function.

storage [Domain_builder.InputDomain]
storage [Domain_store.InputDomain]
store_computed_call [Mem_exec.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.

structural_descr [Locals_scoping]
structure [Abstract_domain.S_with_Structure]

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.Set]
subset [Equality.Equality]
syntactic_lvalues [Hcexprs]

syntactic_lvalues e returns the set of lvalues that appear in the expression e.

T
tag [Structure.Key]
term_ev [Gui_eval.S]
tlval_ev [Gui_eval.S]
tlval_zone_ev [Gui_eval.S]
to_exp [Hcexprs.HCE]
to_list [Partitioning.S]
to_list [Powerset.S]
to_lval [Hcexprs.HCE]
to_set [Partitioning.S]
to_string [Split_strategy]
to_value [Abstract_location.S]
top [Simpler_domains.Simple_Cvalue]
top [Simpler_domains.Minimal]
top [Abstract_domain.Lattice]

Greatest element.

top [Abstract_location.S]
top [Abstract_value.S]
top [Transfer_logic.LogicDomain]
top [Locals_scoping]
top [Simple_memory.Value]
top [Simple_memory.Make_Memory]

The top abstraction, which maps all variables to V.top.

top_int [Abstract_value.S]
track_variable [Simple_memory.Value]

This function must return true if the given variable should be tracked by the domain.

treat_statement_assigns [Transfer_specification.Make]
truncate_integer [Abstract_value.S]

truncate_integer expr irange t truncates the abstract value t to the integer range irange.

truncate_integer [Cvalue_forward]
U
uncheck_add [Powerset.S]
uninitialize_blocks_locals [Cvalue.Model]
uninitialized [Cvalue.V_Or_Uninitialized]

Returns the canonical representant of a definitely uninitialized value.

union [Equality.Set]
union [Equality.Equality]

Union.

union [Hcexprs.BaseToHCESet]
union [Hcexprs.HCEToZone]
union [Alarmset]

Pointwise union of property status: the least precise status is kept.

unite [Equality.Set]

unite (a, a_set) (b, b_set) map unites a and b in map.

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.

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

vars_in_gui_res [Gui_types.S]
W
warn_definitions_overridden_by_builtins [Builtins]

Emits warnings for each function definition that will be overridden by an Eva built-in.

warn_imprecise_lval_read [Warn]
warn_locals_escape [Warn]
warn_none_mode [CilE]

Do not emit any message.

warn_right_exp_imprecision [Warn]
warning_once_current [Value_util]
widen [Simpler_domains.Simple_Cvalue]
widen [Simpler_domains.Minimal]
widen [Abstract_domain.Lattice]

widen h t1 t2 is an over-approximation of join t1 t2.

widen [Simple_memory.Value]
widen [Simple_memory.Make_Memory]
wkey_alarm [Value_parameters]

Warning category used when emitting an alarm in "warning" mode.

wrap_double [Eval_op]
wrap_float [Eval_op]
wrap_int [Eval_op]
wrap_long_long [Eval_op]
wrap_ptr [Eval_op]
wrap_size_t [Eval_op]

Specialization of the function above for standard types

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