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 [Partitioning_index.Make]

Adds a state into an index.

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

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

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_flow_annot [Partitioning_annots]
add_indeterminate_binding [Cvalue.Model]
add_kf_caller [Value_results]
add_numerors_value [Numerors_domain]

Builds the product between a given value module and the numerors value module.

add_red_alarm [Red_statuses]
add_red_property [Red_statuses]
add_slevel_annot [Partitioning_annots]
add_unroll_annot [Partitioning_annots]
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_builtin [Builtins]
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]
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.

assume_bounded [Abstract_value.S]
assume_bounded [Cvalue_forward]
assume_comparable [Abstract_value.S]
assume_comparable [Cvalue_forward]
assume_no_overlap [Abstract_location.S]

Assumes that two locations do not overlap.

assume_non_zero [Abstract_value.S]
assume_non_zero [Cvalue_forward]
assume_not_nan [Abstract_value.S]
assume_not_nan [Cvalue_forward]
assume_valid_location [Abstract_location.S]

Assumes that the given location is valid for a read or write operation, according to the for_writing boolean.

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_or [Cvalue.V]
bitwise_signed_not [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 [Offsm_value]
cast_float_to_float [Cvalue.V]
cast_float_to_int [Cvalue.V]
cast_float_to_int [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 [Eva.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_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 [Partition.Key]
compare [Equality.Set]
compare [Equality.Equality]
compare [Structure.Key]
compare_gui_callstack [Gui_types]
compatible_functions [Eval_typ]
compute [Iterator.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.

configure_precision [Value_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]
contents [Trace_partitioning.Make]
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_callbacks [Value_parameters]

Debug category used when using Eva callbacks when recording the results of a function analysis.

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_incompatible_states [Value_parameters]
dkey_initial_state [Value_parameters]

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

dkey_iterator [Value_parameters]

Debug category used to print information about the iteration

dkey_pointer_comparison [Value_parameters]

Debug category used to print information about invalid pointer comparisons

dkey_summary [Value_parameters]
dkey_widening [Value_parameters]

Debug category used to print the usage of widenings.

drain [Trace_partitioning.Make]

Remove all states from the tank, leaving it empty as if it was just created by empty_tank

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 [Partition.MakeFlow]
empty [Partition]
empty [Partitioning_index.Make]

Creates an empty index.

empty [Powerset.S]
empty [Equality.Set]
empty [Eval.Valuation]
empty_flow [Trace_partitioning.Make]
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.

empty_store [Trace_partitioning.Make]
empty_tank [Trace_partitioning.Make]
empty_widening [Trace_partitioning.Make]
enter_loop [Abstract_domain.S]
enter_loop [Trace_partitioning.Make]
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 [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_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]
exceed_rationing [Partition.Key]
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]
expanded [Trace_partitioning.Make]
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
fill [Trace_partitioning.Make]

Fill the states of the flow into the tank, modifying into inplace.

filter [FCMap.S]

filter p m returns the map with all the bindings in m that satisfy predicate p.

filter [Abstract_domain.Recycle]

filter kf kind bases states reduces the state state to only keep properties about bases — it is a projection on the set of bases.

filter [Partition]
filter [Equality.Equality]

filter p s returns the equality between all elements in s that satisfy predicate p.

filter_map [Partition.MakeFlow]
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 [Partition]
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 [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]

Returns the cvalue builtin for a function, if any.

find_default [Hcexprs.BaseToHCESet]

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]
find_under_approximation [Eval_op]
float_hints [Widen_type]

Define floating hints for one or all variables (None), for a certain stmt or for all statements (None).

flow_actions [Partitioning_parameters.Make]
flow_size [Trace_partitioning.Make]
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 typ binop v1 v2 evaluates the value v1 binop v2, resulting from the application of the binary operator binop to the values v1 and v2.

forward_binop_float [Cvalue_forward]
forward_binop_int [Cvalue_forward]
forward_cast [Abstract_value.S]

Abstract evaluation of casts operators from src_type to dst_type.

forward_cast [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 typ unop v evaluates the value unop v, resulting from the application of the unary operator unop to the value v.

forward_unop [Cvalue_forward]
forward_variable [Abstract_location.S]

Var case in the AST: the host is a variable.

frama_c_strchr_wrapper [Builtins_string]
frama_c_strlen_wrapper [Builtins_string]
frama_c_wcschr_wrapper [Builtins_string]
frama_c_wcslen_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_flow_annot [Partitioning_annots]
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 [Eva.Value_results]
get_retres_vi [Library_functions]

Fake varinfo used by Value to store the result of functions.

get_slevel [Value_util]
get_slevel_annot [Partitioning_annots]
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_unroll_annot [Partitioning_annots]
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 [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.

history_size [Partitioning_parameters.Make]
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 [Partition.MakeFlow]
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.

initial_tank [Trace_partitioning.Make]

Build the initial tank for the entry point of a function.

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_comp_result [Cvalue.V]
inject_float [Cvalue.V]
inject_int [Cvalue.V]
inject_int [Abstract_value.S]

Abstract address for the given varinfo.

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]
interpret_truth [Evaluation.S]
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 [Partition.MakeFlow]
is_empty [Partition]
is_empty [Powerset.S]
is_empty [Equality.Set]
is_empty [Alarmset]

Is there an assertion with a non True status ?

is_empty_flow [Trace_partitioning.Make]
is_empty_store [Trace_partitioning.Make]
is_empty_tank [Trace_partitioning.Make]
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 [Partition.MakeFlow]
iter [Partition]
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 [Trace_partitioning.Make]

Join all incoming propagations into the given store.

join [Powerset.S]
join [Simple_memory.Value]
join [Simple_memory.Make_Memory]
join [Eval.Flagged_Value]
join [Alarmset.Status]
join_duplicate_keys [Partition.MakeFlow]
join_gui_offsetmap_res [Gui_types]
join_list [Alarmset.Status]
join_predicate_status [Eval_terms]
K
key [Cvalue_domain]
key [Inout_domain]
key [Locals_scoping]
key [Equality_domain.Make]
kf_of_gui_loc [Gui_types]
kf_strategy [Split_return]
L
leave_loop [Abstract_domain.S]
leave_loop [Trace_partitioning.Make]
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 (and 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 [Partition]
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]
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_parameters.Make]
merge [Partition]
merge [Powerset.S]
merge [Value_results]
merge [Hcexprs.HCEToZone]
merge [Hptset.S]
merge [Per_stmt_slevel]

Slevel merge strategy for this function

merge [Eva.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.

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

new_monitor [Partition]

Creates a new monitor that allows to split up to split_limit states.

new_rationing [Partition]

Creates a new rationing, that can be used successively on several flows.

next_loop_iteration [Trace_partitioning.Make]
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).

numerors_domain [Numerors_domain]

Returns the numerors domain module, if available.

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_partition [Partition.MakeFlow]
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_assignment [Cvalue_offsetmap]

Computes the offsetmap for an assignment: in case of a copy, extracts the offsetmap from the state;, otherwise, translates the value assigned into an offsetmap.

offsetmap_of_loc [Eval_op]

Returns the offsetmap at a precise_location from a state.

offsetmap_of_lval [Cvalue_offsetmap]

offsetmap_of_lval state lval loc extracts from state state the offsetmap at location loc, corresponding to the lvalue lval.

offsetmap_of_v [Eval_op]

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

offsm_key [Offsm_value]
ok [Numerors_domain]

True if the numerors domain is available; False if the MPFR library has not been found.

ok [Apron_domain]

Are apron domains available?

on [Parameter_sig.Bool]

Set the boolean to true.

one [Cvalue.CardinalEstimate]
one [Abstract_value.S]
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]
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 [Partition.Key]
pretty [Partitioning_index.Make]
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_flow [Trace_partitioning.Make]
pretty_gui_after [Gui_types.S]
pretty_gui_offsetmap_res [Gui_types]
pretty_gui_res [Gui_types.S]
pretty_gui_selection [Gui_types]
pretty_hash [Value_types.Callstack]

Print a hash of the callstack when '-kernel-msg-key callstack' is enabled (prints nothing otherwise).

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_print_c]
pretty_state_as_c_assignments [Builtins_print_c]
pretty_status [Alarmset]
pretty_stitched_offsetmap [Eval_op]
pretty_store [Trace_partitioning.Make]
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]
print_summary [Value_results]

Prints a summary of the analysis.

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_error [Numerors_domain]
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_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]
reinterpret [Cvalue_forward]
reinterpret_as_float [Cvalue.V]
reinterpret_as_int [Cvalue.V]
relate [Abstract_domain.Recycle]

relate kf bases state returns the set of bases bases in relation with bases in state — i.e.

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 [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 [Partition]
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]
report [Red_statuses]
reset [Gui_callstacks_manager]
reset [Value_perf]

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

reset_store [Trace_partitioning.Make]
reset_tank [Trace_partitioning.Make]
reset_widening [Trace_partitioning.Make]
reset_widening_counter [Trace_partitioning.Make]

Resets (or just delays) the widening counter.

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

reuse kf bases current_input previous_output merges the initial state current_input with a final state previous_output from a previous analysis of kf started with an equivalent initial state.

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, assuming 2's complement.

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 [Eva.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 [Iterator]

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]
size [Partition.MakeFlow]
size [Partition]
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 -eva-skip-stdlib-specs

slevel [Partitioning_parameters.Make]
smashed [Trace_partitioning.Make]
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_return [Trace_partitioning.Make]
start_call [Simpler_domains.Simple_Cvalue]
start_call [Simpler_domains.Minimal]
start_call [Abstract_domain.Transfer]

start_call stmt call valuation state returns an initial state for the analysis of a called function.

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.

store_size [Trace_partitioning.Make]
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]
tank_size [Trace_partitioning.Make]
term_ev [Gui_eval.S]
tlval_ev [Gui_eval.S]
tlval_zone_ev [Gui_eval.S]
to_exp [Hcexprs.HCE]
to_list [Partition.MakeFlow]
to_list [Partition]
to_list [Powerset.S]
to_lval [Hcexprs.HCE]
to_partition [Partition.MakeFlow]
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.

transfer [Trace_partitioning.Make]

Apply a transfer function to all the states of a propagation.

transfer_keys [Partition.MakeFlow]
transfer_states [Partition.MakeFlow]
treat_statement_assigns [Transfer_specification.Make]
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 [Partition.MakeFlow]
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.

universal_splits [Partitioning_parameters.Make]
unroll [Partitioning_parameters.Make]
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 (without any access, or for a read or write access).

value_assigned [Eval]
value_key [Numerors_domain]
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]
warn_right_imprecision [Cvalue_offsetmap]

warn_right_imprecision lval loc offsm is used for the assignment of the lvalue lval pointing to the location loc; it warns if the offsetmap offsm contains a garbled mix.

warn_unsupported_spec [Library_functions]

Warns on functions from the frama-c libc with unsupported specification.

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 [Trace_partitioning.Make]

Widen a flow.

widen [Simple_memory.Value]
widen [Simple_memory.Make_Memory]
widening_delay [Partitioning_parameters.Make]
widening_period [Partitioning_parameters.Make]
wkey_alarm [Value_parameters]

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

wkey_builtins_missing_spec [Value_parameters]

Warning category used for "cannot use builtin due to missing spec"

wkey_builtins_override [Value_parameters]

Warning category used for "definition overridden by builtin"

wkey_garbled_mix [Value_parameters]

Warning category used to print garbled mix

wkey_libc_unsupported_spec [Value_parameters]

Warning category used for calls to libc functions whose specification is currently unsupported.

wkey_locals_escaping [Value_parameters]

Warning category used for the warning "locals escaping scope".

wkey_loop_unroll [Value_parameters]

Warning category used for "loop not completely unrolled"

wkey_missing_loop_unroll [Value_parameters]

Warning category used to identify loops without unroll annotations

wkey_missing_loop_unroll_for [Value_parameters]

Warning category used to identify for loops without unroll annotations

wkey_signed_overflow [Value_parameters]

Warning category for signed overflows

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]
zero [Partition.Key]

Initial key: no partitioning.

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.