(>>=) [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 [Partitioning_index.Make] | Adds a state into an index. |
add [Powerset.S] | |
add [Equality.Equality] |
|
add [Simple_memory.S] |
|
add [Eval.Valuation] | |
add [State_builder.Hashtbl] | Add a new binding. |
add' [Powerset.S] | |
add_binding [Cvalue.Model] |
|
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_under [Cvalue.V] | Under-approximating variant of |
alarm_report [Value_util] | Emit an alarm, either as warning or as a result, according to
status associated to |
all [Alarmset] | all alarms: all potential assertions have a Unknown status. |
all_values [Cvalue.V] |
|
alloc_size_ok [Builtins_malloc] | |
apply_builtin [Builtins] | |
apply_on_all_locs [Eval_op] |
|
are_comparable [Cvalue_forward] | |
assign [Simpler_domains.Simple_Cvalue] | |
assign [Simpler_domains.Minimal] | |
assign [Abstract_domain.Transfer] |
|
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_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 |
B | |
backward_binop [Abstract_value.S] | Backward evaluation of the binary operation |
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 |
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 |
backward_field [Abstract_location.S] | |
backward_index [Abstract_location.S] | |
backward_location [Abstract_domain.Queries] |
|
backward_mult_int_left [Cvalue.V] | |
backward_pointer [Abstract_location.S] | |
backward_unop [Abstract_value.S] | Backward evaluation of the unary operation |
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_zero_or_one [Precise_locs] | Should not be used, |
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] |
|
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 |
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 |
clobbered_set_from_ret [Builtins] |
|
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_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 |
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_ |
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 |
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 |
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 [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 |
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 [Subdivided_evaluation.Forward_Evaluation] | |
evaluate [Subdivided_evaluation.Make] | |
evaluate_assumes_of_behavior [Transfer_logic.S] | |
evaluate_predicate [Abstract_domain.S] | Evaluates a |
evaluate_predicate [Transfer_logic.LogicDomain] | |
exceed_rationing [Partition.Key] | |
exists [FCMap.S] |
|
exists [Equality.Set] | |
exists [Equality.Equality] |
|
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:
|
extract_lval [Simpler_domains.Simple_Cvalue] | |
extract_lval [Abstract_domain.Queries] | Query function for lvalues:
|
F | |
fill [Trace_partitioning.Make] | Fill the states of the flow into the tank, modifying |
filter [FCMap.S] |
|
filter [Abstract_domain.Recycle] |
|
filter [Partition] | |
filter [Equality.Equality] |
|
filter_map [Partition.MakeFlow] | |
finalize_call [Simpler_domains.Simple_Cvalue] | |
finalize_call [Simpler_domains.Minimal] | |
finalize_call [Abstract_domain.Transfer] |
|
find [FCMap.S] |
|
find [Cvalue.Model] |
|
find [Abstract_domain.Valuation] | |
find [Partition] | |
find [Equality.Set] |
|
find [Simple_memory.S] |
|
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_loc [Abstract_domain.Valuation] | |
find_loc [Eval.Valuation] | |
find_opt [FCMap.S] |
|
find_option [Equality.Set] | Same as |
find_subpart [Cvalue_domain] | |
find_under_approximation [Eval_op] | |
float_hints [Widen_type] | Define floating hints for one or all variables ( |
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 [Precise_locs] | |
fold [Abstract_domain.Valuation] | |
fold [Powerset.S] | |
fold [Equality.Set] | |
fold [Equality.Equality] |
|
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_sorted [State_builder.Hashtbl] | |
for_all [FCMap.S] |
|
for_all [Equality.Set] | |
for_all [Equality.Equality] |
|
for_all [Alarmset] | |
force_compute [Analysis] | Perform a full analysis, starting from the |
forward_binop [Abstract_value.S] |
|
forward_binop_float [Cvalue_forward] | |
forward_binop_int [Cvalue_forward] | |
forward_cast [Abstract_value.S] | Abstract evaluation of casts operators from |
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_pointer [Abstract_location.S] | Mem case in the AST: the host is a pointer. |
forward_unop [Abstract_value.S] |
|
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 |
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 |
G | |
get [Abstract_domain.Interface] | For a key of type |
get [Hcexprs.HCE] | |
get [Structure.External] | |
get [State_builder.Ref] | Get the referenced value. |
getWidenHints [Widen] |
|
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 |
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_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
|
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 |
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_variable [Simpler_domains.Simple_Cvalue] | |
initialize_variable [Simpler_domains.Minimal] | |
initialize_variable [Abstract_domain.S] |
|
initialize_variable_using_type [Abstract_domain.S] | Initializes a variable according to its type. |
initialized [Cvalue.V_Or_Uninitialized] |
|
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] |
|
intersects [Hptset.S] |
|
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 |
is_dynamic [Widen_hints_ext] |
|
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_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_initialized [Cvalue.V_Or_Uninitialized] |
|
is_isotropic [Cvalue.V] | |
is_lval [Hcexprs.HCE] | |
is_noesc [Cvalue.V_Or_Uninitialized] |
|
is_non_terminating_instr [Gui_callstacks_filters] | |
is_non_terminating_instr [Value_results] | Returns |
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 |
iter [FCMap.S] |
|
iter [Partition.MakeFlow] | |
iter [Partition] | |
iter [Powerset.S] | |
iter [Equality.Set] | |
iter [Equality.Equality] |
|
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] |
|
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_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] |
|
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_fundec [Locals_scoping] |
|
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] |
|
map [FCMap.S] |
|
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 |
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 |
mem [FCMap.S] |
|
mem [Abstract_domain.Interface] | Tests whether a key belongs to the domain. |
mem [Equality.Set] |
|
mem [Equality.Equality] |
|
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 [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 |
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 |
need_cast [Eval_typ] | return |
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 |
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] |
|
notify [Alarmset] | Calls the functions registered in the |
null_ev [Gui_eval.S] | |
num_hints [Widen_type] | Define numeric hints for one or all variables ( |
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 |
offset_bottom [Precise_locs] | |
offset_top [Precise_locs] | |
offset_zero [Precise_locs] | |
offsetmap_contains_local [Locals_scoping] | |
offsetmap_matches_type [Eval_typ] |
|
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_v [Eval_op] | Transformation a value into an offsetmap of size |
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 |
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] |
|
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 |
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_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 |
project_ival [Cvalue.V] | Raises |
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_by_danglingness [Cvalue.V_Or_Uninitialized] |
|
reduce_by_enumeration [Subdivided_evaluation.Make] | |
reduce_by_initialized_defined [Eval_op] | |
reduce_by_initializedness [Cvalue.V_Or_Uninitialized] |
|
reduce_by_predicate [Abstract_domain.S] |
|
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 |
reduce_indeterminate_binding [Cvalue.Model] | Same behavior as |
reduce_previous_binding [Cvalue.Model] |
|
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 |
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] |
|
remember_bases_with_locals [Locals_scoping] | Add the given set of bases to an existing clobbered set |
remember_if_locals_in_value [Locals_scoping] |
|
remove [FCMap.S] |
|
remove [Equality.Set] |
|
remove [Equality.Equality] |
|
remove [Simple_memory.S] |
|
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] |
|
reorder [Powerset.S] | |
replace [Partition] | |
replace [Hcexprs.HCE] | Replaces all occurrences of the lvalue |
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] |
|
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 |
returned_value [Library_functions] | |
reuse [Abstract_domain.Recycle] |
|
reuse_previous_call [Mem_exec.Make] |
|
rewrap_integer [Abstract_value.S] |
|
rewrap_integer [Cvalue_forward] | |
S | |
safe_argument [Backward_formals] |
|
save_globals_state [State_import] | Saves the final state of globals variables after the return statement of
the function defined via |
self [Hcexprs.HCE] | |
set [Abstract_domain.Interface] | For a key of type |
set [Structure.External] | |
set [Alarmset] |
|
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 [Powerset.S] | |
singleton [Alarmset] |
|
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
|
slevel [Partitioning_parameters.Make] | |
smashed [Trace_partitioning.Make] | |
split [FCMap.S] |
|
split_return [Trace_partitioning.Make] | |
start_call [Simpler_domains.Simple_Cvalue] | |
start_call [Simpler_domains.Minimal] | |
start_call [Abstract_domain.Transfer] |
|
start_doing [Value_perf] | |
stop_doing [Value_perf] | Call |
storage [Domain_builder.InputDomain] | |
storage [Domain_store.InputDomain] | |
store_computed_call [Mem_exec.Make] |
|
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 |
subset [Equality.Set] | |
subset [Equality.Equality] | |
syntactic_lvalues [Hcexprs] |
|
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 |
top_int [Abstract_value.S] | |
track_variable [Simple_memory.Value] | This function must return |
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] |
|
universal_splits [Partitioning_parameters.Make] | |
unroll [Partitioning_parameters.Make] | |
unspecify_escaping_locals [Cvalue.V_Or_Uninitialized] | |
update [Abstract_domain.Transfer] |
|
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_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 [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] |
|
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. |