(>>=) [Eval] |
This monad propagates the `Bottom value if needed, and join the alarms
of each evaluation.
|
(>>=.) [Eval] |
Use this monad of the following function returns no alarms.
|
(>>=:) [Eval] |
Use this monad if the following function returns a simple value.
|
_join [Gauges_domain.G.Gauge] | |
A | |
a_ignore [CilE] | |
active [Eval_annots.ActiveBehaviors] | |
active_behaviors [Eval_annots.ActiveBehaviors] | |
actualize_formals [Function_args] | |
add [FCMap.S] | add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add [Equality_sig.S] | add x s returns the equality between all elements of s and x .
|
add [Partitioning.StateSet] | |
add [Equality_sig.Set] | |
add [Hcexprs.BaseToHCESet] | |
add [Hcexprs.HCEToZone] | |
add [Gauges_domain.G.Gauge] | |
add [Gauges_domain.G.Bounds] | |
add [Eval.Valuation] | |
add [Alarmset] |
! Different semantics according to the kind of alarms map.
|
add [Hashtbl.S] | |
add [State_builder.Hashtbl] |
Add a new binding.
|
add [State_set] |
Adding elements
|
add' [Partitioning.StateSet] | |
add' [Alarmset] | |
add_binding [Cvalue.Model] | add_binding state loc v simulates the effect of writing v at location
loc in state .
|
add_binding [Eval_op] |
Temporary.
|
add_binding_unspecified [Cvalue.Model] | |
add_binding_unspecified [Eval_op] |
Temporary.
|
add_initial_binding [Cvalue.Model] | |
add_kf_caller [Value_results] | |
add_new_base [Cvalue.Model] | |
add_statement [State_set] |
Update the trace of all the states in the stateset.
|
add_unsafe_binding [Cvalue.Model] | |
add_untyped [Cvalue.V] | add_untyped ~factor e1 e2 computes e1+factor*e2 using C semantic
for +, i.e.
|
add_untyped_under [Cvalue.V] |
Under-approximating variant of
Cvalue.V.add_untyped .
|
alarm_report [Value_util] |
Emit an alarm, either as warning or as a result, according to
option AlarmsWarnings.
|
all [Alarmset] |
all alarms: all potential assertions have a Dont_know status.
|
all_values [Cvalue.V] | all_values ~size v returns true iff v contains all integer values
representable in size bits.
|
all_vars_str [Widen_hints_ext] |
String used for hints applying to all variables.
|
apply [Value_messages.Value_Message_Callback] | |
apply_on_all_locs [Eval_op] | apply_all_locs f loc state folds f on all the atomic locations
in loc , provided there are less than plevel .
|
are_comparable [Cvalue_forward] | |
are_comparable [Warn] | |
assign [Abstract_domain.Transfer] | assign kinstr lv expr v valuation state is the transfer function for the
assignment lv = expr for state .
|
assign [Transfer_stmt.S] | |
assign [Gauges_domain.D_Impl.Transfer] | |
assign [Gauges_domain.G] | |
assign_return [Abstract_domain.Transfer] | assign_return stmt lv kf return value valuation state models on states
the effect of the assignment of the return value of a called function at
the call site.
|
assign_return [Gauges_domain.D_Impl.Transfer] | |
assume [Abstract_domain.Transfer] |
Transfer function for an assumption.
|
assume [Transfer_stmt.S] | |
assume [Evaluation.S] | assume ~valuation state expr value assumes in the valuation that
the expression expr has the value value in the state state ,
and backward propagates this information to the subterm of expr .
|
assume [Gauges_domain.D_Impl.Transfer] | |
B | |
backward_binop [Abstract_value.S] |
Backward evaluation of the binary operation
left binop right = result ;
tries to reduce the argument left and right according to result .
|
backward_binop [Cvalue_backward] |
This function tries to reduce the argument values of a binary operation,
given its result.
|
backward_cast [Abstract_value.S] |
Backward evaluation of the cast of the value
src_val of type src_typ
into the value dst_val of type dst_typ .
|
backward_cast [Cvalue_backward] |
This function tries to reduce the argument of a cast, given the result of
the cast.
|
backward_comp_float_left [Cvalue.V] | |
backward_comp_int_left [Cvalue.V] | |
backward_comp_left_from_type [Eval_op] |
Reduction of a
Cvalue.V.t by == , != , >= , > , <= and < .
|
backward_field [Abstract_location.S] | |
backward_index [Abstract_location.S] | |
backward_location [Abstract_domain.Queries] | backward_location state lval typ loc v reduces the location loc of the
lvalue lval of type typ , so that only the locations that may have value
v are kept.
|
backward_location [Gauges_domain.D_Impl] | |
backward_loop [Gauges_domain.G] | |
backward_mult_int_left [Cvalue.V] | |
backward_nb [Gauges_domain.G.Bounds] | |
backward_pointer [Abstract_location.S] | |
backward_unop [Abstract_value.S] |
Backward evaluation of the unary operation
unop arg = res ;
tries to reduce the argument arg according to res .
|
backward_unop [Cvalue_backward] |
This function tries to reduce the argument value of an unary operation,
given its result.
|
backward_variable [Abstract_location.S] | |
behavior_from_name [Eval_annots.ActiveBehaviors] | |
behavior_inactive [Eval_annots] | |
bind_block_locals [Value_util] |
Bind all locals of the block to their default value
(namely UNINITIALIZED)
|
bindings [FCMap.S] |
Return the list of all bindings of the given map.
|
bitfield_size [Eval_typ] | |
bitwise_and [Cvalue.V] | |
bitwise_not [Cvalue.V] | |
bitwise_not_size [Cvalue.V] | |
bitwise_or [Cvalue.V] | |
bitwise_xor [Cvalue.V] | |
block_top_addresses_of_locals [Locals_scoping] |
Return a function that topifies all references to the variables local
to the given blocks.
|
bottom [Locals_scoping] | |
bottom_location_bits [Precise_locs] | |
box_key [Apron_domain] | |
C | |
c_labels [Eval_annots] | |
c_rem [Cvalue.V] | |
cache_name [Gauges_domain.G] | |
call [Transfer_stmt.S] | |
call_stack [Value_util] | |
callsite_matches [Gui_callstacks_filters] | |
callstack_matches [Gui_callstacks_filters] | |
callstacks_at_gui_loc [Gui_eval] |
For statements: results are available only if the statement is reachable.
|
cardinal [FCMap.S] |
Return the number of bindings of a map.
|
cardinal [Equality_sig.S] |
Return the number of elements of the equality.
|
cardinal [Equality_sig.Set] | |
cardinal_estimate [Cvalue.Model] | |
cardinal_zero_or_one [Precise_locs] |
Should not be used,
Precise_locs.valid_cardinal_zero_or_one is almost always more
useful
|
cast [Cvalue.V] | cast ~size ~signed v applies to the abstract value v the conversion
to the integer type described by size and signed .
|
cast [Offsm_value] | |
cast_double [Cvalue.V] | |
cast_float [Cvalue.V] | |
cast_float_to_int [Cvalue.V] | |
cast_float_to_int_inverse [Cvalue.V] | |
cast_int_to_float [Cvalue.V] | |
cast_int_to_float_inverse [Cvalue.V] | |
cast_lval_if_bitfield [Eval_typ] |
if needed, cast the given abstract value to the given size.
|
change_callstacks [Value_results] |
Change the callstacks for the results for which this is meaningful.
|
change_callstacks [Value.Value_results] | |
check_arg_size [Function_args] | |
check_copy_lval [Evaluation.S] | |
check_fct_assigns [Eval_annots] | |
check_fct_postconditions [Transfer_logic.S] | |
check_fct_postconditions [Eval_annots] |
Check the postcondition of
kf for every behavior, treating them
separately if per_behavior is true , merging them otherwise.
|
check_fct_postconditions_default_behavior [Eval_annots] | |
check_fct_postconditions_for_behavior [Eval_annots] |
Checks the postconditions of
b and of the default behavior if it is not
b
|
check_fct_postconditions_of_behavior [Eval_annots] |
Check the postcondition of
kf for a given behavior b .
|
check_fct_preconditions [Transfer_logic.S] | |
check_fct_preconditions [Eval_annots] | |
check_fct_preconditions_for_behavior [Eval_annots] |
Check the precondition of
kf for a given behavior b .
|
check_from [Eval_annots] |
Compute the validity status for
from in pre_state , assuming the
entire clause is assigns asgn \from from .
|
check_no_recursive_call [Warn] | |
check_non_overlapping [Abstract_location.S] |
Needed for unspecified sequences.
|
check_non_overlapping [Evaluation.S] | |
check_non_overlapping [Eval_stmt] | |
check_unspecified_sequence [Transfer_stmt.S] | |
check_unspecified_sequence [Eval_stmt] | |
choose [FCMap.S] |
Return one binding of the given map, or raise
Not_found if
the map is empty.
|
choose [Equality_sig.S] |
Return the representative of the equality.
|
choose [Equality_sig.Set] | |
classify_as_scalar [Eval_typ] | |
classify_pre_post [Gui_eval] |
State in which the predicate, found in the given function,
should be evaluated
|
classify_sign [Gauges_domain.G.Bounds] | |
cleanup_results [Mem_exec2] |
Clean all previously stored results
|
cleanup_results [Mem_exec] |
Clean all previously stored results
|
clear [Hashtbl.S] | |
clear [State_builder.Hashtbl] |
Clear the table.
|
clear [Stop_at_nth] | |
clear [State_builder.Ref] |
Reset the reference to its default value.
|
clear_caches [Hptset.S] |
Clear all the caches used internally by the functions of this module.
|
clear_call_stack [Value_util] |
Functions dealing with call stacks.
|
clear_englobing_exprs [Eval.Clear_Valuation] |
Removes from the valuation all the subexpressions of
expr that contain
subexpr , except subexpr itself.
|
clobbered_set_from_ret [Builtins] | clobbered_set_from_ret state ret can be used for functions that return
a pointer to where they have written some data.
|
code_annotation_loc [Eval_annots] | |
code_annotation_text [Eval_annots] | |
combine_base_precise_offset [Precise_locs] | |
combine_loc_precise_offset [Precise_locs] | |
compare [FCMap.S] |
Total ordering between maps.
|
compare [Equality_sig.S] | |
compare [Equality_sig.Set] | |
compare [Gauges_domain.G.MultipleIterations] | |
compare [Structure.Key] | |
compare_gui_callstack [Gui_types] | |
compare_max_float [Cvalue.V] | |
compare_max_int [Cvalue.V] | |
compare_min_float [Cvalue.V] | |
compare_min_int [Cvalue.V] | |
compatible_functions [Eval_typ] |
Test that two functions types are compatible; used to verify that a call
through a function pointer is ok.
|
compatible_functions [Value_util] | |
compute [Analysis.Make] | |
compute [Analysis] |
Perform a full analysis, starting from the given kernel_function and with
the abstractions specified by the configuration.
|
compute [Partitioned_dataflow.Computer] | |
compute [Eval_slevel.Computer] | |
compute_actual [Function_args] | |
compute_call_ref [Transfer_stmt.S] | |
compute_call_ref [Eval_stmt] | |
compute_from_entry_point [Compute_functions.Make] | |
compute_non_linear [Eval_non_linear] | |
compute_using_specification [Abstract_domain.S] | |
compute_using_specification [Gauges_domain.D_Impl] | |
compute_using_specification [Eval_behaviors] |
Evaluate
kf in state with_formals , first by reducing by the
preconditions, then by evaluating the assigns, then by reducing
by the post-conditions.
|
configure [Abstractions] |
Build a configuration according to the analysis paramaters.
|
constant [Abstract_value.S] |
Returns the abstract value of a litteral constants, and potentially some
alarms in case of floating point constants overflow.
|
contains [Equality_sig.Set] | contains elt set = true iff elt belongs to an equality of set .
|
contains_c_at [Eval_annots] | |
contains_non_zero [Cvalue.V] | |
contains_single_elt [Hptset.S] | |
contains_zero [Cvalue.V] | |
conv_comp [Value_util] | |
conv_relation [Value_util] | |
conv_status [Eval_annots] | |
copy [Hashtbl.S] | |
copy [Datatype.S] |
Deep copy: no possible sharing between
x and copy x .
|
copy_lvalue [Evaluation.S] |
Computes the value of a lvalue, with possible indeterminateness: the
returned value may be uninitialized, or contain escaping addresses.
|
copy_offsetmap [Eval_op] |
Tempory.
|
create [Transfer_logic.S] | |
create [Hashtbl.S] | |
create [Eval_annots.ActiveBehaviors] | |
create_all_values [Cvalue.V] | |
create_alloced_return [Library_functions] | |
create_from_spec [Eval_annots.ActiveBehaviors] | |
create_key [Structure.Key] | |
create_new_var [Value_util] |
Create and register a new variable inside Frama-C.
|
ct [Gauges_domain.G.Gauge] | |
current [Analysis] |
The abstractions used in the latest analysis, and its results.
|
current_kf [Value_util] |
The current function is the one on top of the call stack.
|
current_kf_inout [Transfer_stmt] | |
current_stmt [Alarmset] | |
current_stmt [Valarms] | |
curstate [Value_messages] | |
cvalue_initial_state [Analysis] |
Compute the initial state of the cvalue domain only.
|
cvalue_key [Main_values] |
Key for cvalues.
|
D | |
debug_result [Value_util] | |
deep_fold [Equality_sig.Set] | |
default [Widen_type] |
A default set of hints
|
default_alarm_report [Value_messages] | |
default_call [Abstract_domain.Transfer] | |
default_call [Gauges_domain.D_Impl.Transfer] | |
default_config [Abstractions] |
Default configuration of EVA.
|
default_offsetmap [Cvalue.Default_offsetmap] | |
display [Value_perf] |
Display a complete summary of performance informations.
|
distinct_subpart [Cvalue_domain] | |
div [Cvalue.V] | |
div_towards_minus_infty [Gauges_domain.G.Bounds] | |
div_towards_plus_infty [Gauges_domain.G.Bounds] | |
dkey [Gauges_domain] | |
dkey [Widen_hints_ext] | |
dkey_alarm [Value_parameters] |
Debug category used when emitting an alarm in "non-warning" mode
|
dkey_final_states [Value_parameters] | |
dkey_garbled_mix [Value_parameters] |
Debug category used to print garbled mix
|
dkey_initial_state [Value_parameters] |
Debug categories responsible for printing initial and final states of Value.
|
do_assign [Eval_stmt] | |
do_promotion [Abstract_value.S] | |
do_promotion [Evaluation.S] | |
do_promotion [Cvalue_forward] | |
do_promotion [Eval_op] | |
do_warn [Valarms] | |
dump_args [Builtins_misc] | |
dump_garbled_mix [Value_util] |
print information on the garblex mix created during evaluation
|
dump_state [Builtins_misc] |
Builtins with multiple names; the lookup is done using a distinctive
prefix
|
dump_state_file [Builtins_misc] | |
E | |
elements [Equality_sig.Set] | |
elements_only_left [Equality_sig.Set] | |
emit [Alarmset] |
Emits the alarms according to the given warn mode.
|
emit_alarm [Builtins] |
Emit an ACSL assert (using \warning predicate) to signal that the
builtin encountered an alarm described by the string.
|
emit_message_and_status [Eval_annots] | |
emit_status [Eval_annots] | |
emitter [Value_util] | |
empty [Gui_callstacks_filters] | |
empty [FCMap.S] |
The empty map.
|
empty [Widen_type] |
An empty set of hints
|
empty [Abstract_domain.S] |
Initialization
|
empty [Partitioning.Partition] | |
empty [Partitioning.StateSet] | |
empty [Equality_sig.Set] | |
empty [Hcexprs.BaseToHCESet] | |
empty [Hcexprs.HCEToZone] | |
empty [Gauges_domain.D_Impl] | |
empty [Gauges_domain.G] | |
empty [Eval.Valuation] | |
empty [State_imp] |
Creation
|
empty [State_set] |
Creation
|
empty_wh [Gauges_domain.G.MV] | |
end_stmt [Alarmset] | |
end_stmt [Valarms] | |
enlarge [Gauges_domain.G.Bounds] | |
enter_loop [Abstract_domain.Transfer] | |
enter_loop [Transfer_stmt.S] | |
enter_loop [Gauges_domain.D_Impl.Transfer] | |
enter_loop [Gauges_domain.G] | |
enter_scope [Abstract_domain.S] |
Scoping: abstract transformers for entering and exiting blocks.
|
enter_scope [Gauges_domain.D_Impl] | |
enumerate_valid_bits [Precise_locs] | |
env_annot [Abstract_domain.Logic] | |
env_annot [Gauges_domain.D_Impl] | |
env_annot [Eval_terms] | |
env_assigns [Eval_terms] | |
env_current_state [Abstract_domain.Logic] | |
env_current_state [Gauges_domain.D_Impl] | |
env_current_state [Eval_terms] | |
env_only_here [Eval_terms] |
Used by auxiliary plugins, that do not supply the other states
|
env_post_f [Abstract_domain.Logic] | |
env_post_f [Gauges_domain.D_Impl] | |
env_post_f [Eval_terms] | |
env_pre_f [Abstract_domain.Logic] | |
env_pre_f [Gauges_domain.D_Impl] | |
env_pre_f [Eval_terms] | |
epilogue [Separate] | |
eq_type [Structure.Key] | |
equal [FCMap.S] | equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Equality_sig.S] | |
equal [Hashtbl.HashedType] |
The equality predicate used to compare keys.
|
equal [Equality_sig.Set] | |
equal [Gauges_domain.G.MultipleIterations] | |
equal [Gauges_domain.G.Bounds] | |
equal [Structure.Key] | |
equal [Alarmset] | |
equal_gui_after [Gui_types] | |
equal_gui_offsetmap_res [Gui_types] | |
equal_gui_res [Gui_types] | |
equal_loc [Precise_locs] | |
equal_loc [Abstract_location.S] | |
equal_offset [Precise_locs] | |
equal_offset [Abstract_location.S] | |
eval_and_reduce_p_kind [Eval_annots] | |
eval_assigns_from [Eval_annots] | |
eval_binop_float [Eval_op] | |
eval_binop_int [Eval_op] | |
eval_by_callstack [Eval_annots] | |
eval_expr [Analysis.Results] | |
eval_expr [Eval_exprs] | |
eval_expr_with_deps_state [Eval_non_linear] |
Same functionality as
Eval_exprs.eval_expr_with_deps_state .
|
eval_expr_with_deps_state [Eval_exprs] | |
eval_float_constant [Cvalue_forward] | |
eval_float_constant [Eval_op] |
The arguments are the approximate float value computed during parsing, the
size of the floating-point type, and the string representing the initial
constant if available.
|
eval_function_exp [Evaluation.S] |
Evaluation of the function argument of a
Call constructor
|
eval_gauge [Gauges_domain.G] | |
eval_lval [Eval_exprs] | |
eval_predicate [Abstract_domain.Logic] | |
eval_predicate [Gauges_domain.D_Impl] | |
eval_predicate [Eval_terms] | |
eval_term [Eval_terms] | |
eval_term_as_exact_locs [Eval_terms] | |
eval_tlval [Eval_terms] | |
eval_tlval_as_location [Eval_terms] | |
eval_tlval_as_zone [Eval_terms] | |
eval_tlval_as_zone_under_over [Eval_terms] |
Return a pair of (under-approximating, over-approximating) zones.
|
eval_unop [Eval_op] | |
eval_varinfo [Abstract_location.S] | |
evaluate [Evaluation.S] | evaluate ~valuation state expr evaluates the expression expr in the
state state , and returns the pair result, alarms , where: alarms are the set of alarms ensuring the soundness of the evaluation;, result is either `Bottom if the evaluation leads to an error,
or `Value (valuation, value), where value is the numeric value computed
for the expression expr , and valuation contains all the intermediate
results of the evaluation.
The valuation argument is a cache of already computed expressions.
It is empty by default.
The reduction argument allows deactivating the backward reduction
performed after the forward evaluation.
|
exists [FCMap.S] | exists p m checks if at least one binding of the map
satisfy the predicate p .
|
exists [Equality_sig.S] | exists p s checks if at least one element of the equality
satisfies the predicate p .
|
exists [Equality_sig.Set] | |
exists [Alarmset] | |
exists [State_imp] | |
exists [State_set] | |
exists [Parameter_sig.Set] |
Is there some element satisfying the given predicate?
|
exp_ev [Gui_eval] | |
expr_contains_volatile [Eval_typ] | |
extend_loc [Domain_lift.Conversion] | |
extend_val [Domain_lift.Conversion] | |
extend_val [Location_lift.Conversion] | |
externalize [Eval_stmt] | |
extract [Cvalue_domain] | |
extract_expr [Abstract_domain.Queries] |
Query function for compound expressions:
eval oracle t exp returns the known value of exp by the state t .
|
extract_expr [Gauges_domain.D_Impl] | |
extract_gauge [Gauges_domain.G] | |
extract_lval [Abstract_domain.Queries] |
Query function for lvalues:
find oracle t lval typ loc returns the known value stored at
the location loc of the left value lval of type typ .
|
extract_lval [Gauges_domain.D_Impl] | |
F | |
filter [FCMap.S] | filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter [Equality_sig.S] | filter p s returns the equality between all elements in s
that satisfy predicate p .
|
filter_by_bases [Abstract_domain.S] |
Mem exec.
|
filter_by_bases [Mem_exec2.Domain] | |
filter_by_bases [Gauges_domain.D_Impl] | |
filter_if [Separate] | |
filter_map_inplace [Hashtbl.S] | |
finalize_call [Abstract_domain.Transfer] | finalize_call stmt call ~pre ~post computes the state after a function
call, given the state pre before the call, and the state post at the
end of the called function.
|
finalize_call [Gauges_domain.D_Impl.Transfer] | |
find [FCMap.S] | find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find [Cvalue.Model] | find ?conflate_bottom state loc returns the same value as
find_indeterminate , but removes the indeterminate flags from the
result.
|
find [Abstract_domain.Valuation] | |
find [Equality_sig.Set] | find elt set return the (single) equality involving elt
that belongs to set , or raise Not_found if no such equality exists.
|
find [Hcexprs.BaseToHCESet] |
may raise
Not_found
|
find [Hcexprs.HCEToZone] |
may raise
Not_found
|
find [Eval.Valuation] | |
find [Alarmset] |
Returns the status of a given alarm.
|
find [Hashtbl.S] | |
find [Eval_op] |
Tempory.
|
find [State_builder.Hashtbl] |
Return the current binding of the given key.
|
find [Parameter_sig.Map] |
Search a given key in the map.
|
find_all [Hashtbl.S] | |
find_all [State_builder.Hashtbl] |
Return the list of all data associated with the given key.
|
find_builtin [Builtins] |
Find a previously registered builtin.
|
find_builtin_override [Builtins] |
Should the given function be replaced by a call to a builtin
|
find_default [Hcexprs.BaseToHCESet] |
returns the empty set when the key is not bound
|
find_default [Hcexprs.HCEToZone] |
returns the empty set when the key is not bound
|
find_loc [Abstract_domain.Valuation] | |
find_loc [Eval.Valuation] | |
find_lv [Eval_exprs] | |
find_option [Equality_sig.Set] |
Same as
find , but return None in the last case.
|
find_right_value [Cvalue_transfer] | |
find_subpart [Cvalue_domain] | |
find_unspecified [Cvalue.Model] | find_unspecified ~conflate_bottom state loc returns the value
and flags associated to loc in state .
|
float_kind [Value_util] |
Classify a
Cil_types.fkind as either a 32 or 64 floating-point type.
|
float_zeros [Abstract_value.S] | |
fold [FCMap.S] | fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold [Precise_locs] | |
fold [Equality_sig.S] | fold f s a computes (f xN ... (f x2 (f x1 a))...) ,
where x1 ... xN are the elements of s , in increasing order.
|
fold [Abstract_domain.Valuation] | |
fold [Partitioning.Partition] | |
fold [Partitioning.StateSet] | |
fold [Equality_sig.Set] | |
fold [Eval.Valuation] | |
fold [Hashtbl.S] | |
fold [State_imp] |
Iterators
|
fold [State_builder.Hashtbl] | |
fold [State_set] |
Iterators
|
fold2_join_heterogeneous [Hptset.S] | |
fold_emitted_alarms [Builtins] |
Iteration on special assertions built by the builtins
|
fold_left2_best_effort [Function_args] | |
fold_sorted [State_builder.Hashtbl] | |
for_all [FCMap.S] | for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
for_all [Equality_sig.S] | for_all p s checks if all elements of the equality
satisfy the predicate p .
|
for_all [Equality_sig.Set] | |
for_all [Alarmset] | |
force_compute [Analysis] |
Perform a full analysis, starting from the
main function.
|
force_compute [Eval_funs] |
Perform a full analysis, starting from the
main function.
|
forget [Gauges_domain.G] | |
forward_binop [Abstract_value.S] | forward_binop context typ binop v1 v2 evaluates the value v1 binop v2 ,
and the alarms resulting from the operations.
|
forward_binop_float [Cvalue_forward] | |
forward_binop_float_alarm [Cvalue_forward] | |
forward_binop_int [Cvalue_forward] | |
forward_comp_int [Cvalue.V] | |
forward_field [Abstract_location.S] |
Computes the field offset of a fieldinfo, with the given remaining offset.
|
forward_index [Abstract_location.S] | forward_index typ value offset computes the array index offset of
(Index (ind, off)), where the index expression ind evaluates to value
and the remaining offset off evaluates to offset .
|
forward_pointer [Abstract_location.S] |
Mem case in the AST: the host is a pointer.
|
forward_unop [Abstract_value.S] | forward_unop context typ unop v evaluates the value unop v , and the
alarms resulting from the operations.
|
forward_unop [Cvalue_forward] | |
forward_variable [Abstract_location.S] |
Var case in the AST: the host is a variable.
|
frama_c_memchr_wrapper [Builtins_string] | |
frama_c_rawmemchr_wrapper [Builtins_string] | |
frama_c_strchr_wrapper [Builtins_string] | |
frama_c_strlen_wrapper [Builtins_string] | |
frama_c_strnlen_wrapper [Builtins_string] | |
from_callstack [Gui_callstacks_filters] | |
from_ival [Gauges_domain.G.Bounds] | |
from_shape [Hptset.S] |
Build a set from another
elt -indexed map or set.
|
function_calls_handling [Gauges_domain] | |
G | |
gauge_from_state [Gauges_domain.G] | |
get [Abstract_domain.Interface] |
For a key of type
k key : if the states of this domain (of type t ) contain a part (of type k )
from the domain identified by the key,
then get key returns an accessor for this part of a state., otherwise, get key returns None.
|
get [Hcexprs.HCE] | |
get [Structure.External] | |
get [State_builder.Ref] |
Get the referenced value.
|
getWidenHints [Widen] | getWidenHints kf s retrieves the set of widening hints related to
function kf and statement s .
|
get_LoadFunctionState [Value_parameters] | |
get_SaveFunctionState [Value_parameters] | |
get_function_name [Parameter_sig.String] |
returns the given argument only if it is a valid function name
(see
Parameter_customize.get_c_ified_functions for more information),
and abort otherwise.
|
get_influential_vars [Eval_exprs] | |
get_initial_state [Abstract_domain.Store] | |
get_initial_state_by_callstack [Abstract_domain.Store] | |
get_plain_string [Parameter_sig.String] |
always return the argument, even if the argument is not a function name.
|
get_possible_values [Parameter_sig.String] |
What are the acceptable values for this parameter.
|
get_range [Parameter_sig.Int] |
What is the possible range of values for this parameter.
|
get_results [Value_results] | |
get_results [Value.Value_results] | |
get_retres_vi [Library_functions] |
Fake varinfo used by Value to store the result of functions without
bodies.
|
get_rounding_mode [Value_util] | |
get_slevel [Value_util] | |
get_stmt_state [Analysis.Results] | |
get_stmt_state [Abstract_domain.Store] | |
get_stmt_state_by_callstack [Abstract_domain.Store] | |
get_stmt_widen_hint_terms [Widen_hints_ext] | get_stmt_widen_hint_terms s returns the list of widen hints associated to
s .
|
get_v [Cvalue.V_Or_Uninitialized] | |
global_state [Abstract_domain.S] | |
global_state [Gauges_domain.D_Impl] | |
gui_loc_equal [Gui_types] | |
gui_loc_loc [Gui_types] | |
gui_loc_logic_env [Gui_eval] |
Logic labels valid at the given location.
|
gui_selection_data_empty [Gui_eval] |
Default value.
|
gui_selection_equal [Gui_types] | |
H | |
handle_overflow [Eval_op] | |
has_requires [Eval_annots] | |
hash [Hashtbl.HashedType] |
A hashing function on keys.
|
hash [Gauges_domain.G.MultipleIterations] | |
hash [Structure.Key] | |
hash_gui_callstack [Gui_types] | |
header [Eval_annots.ActiveBehaviors] | |
hints_from_keys [Widen_type] |
Widen hints for a given statement, suitable for function
Cvalue.Model.widen .
|
I | |
id [Equality.Element] |
Identity of a key.
|
id [Hcexprs.HCE] | |
ik_attrs_range [Eval_typ] |
Range for an integer type with some attributes.
|
ik_range [Eval_typ] | |
imprecise_location [Precise_locs] | |
imprecise_location_bits [Precise_locs] | |
imprecise_offset [Precise_locs] | |
inc [Gauges_domain.G] | |
incr [Stop_at_nth] | |
incr [Parameter_sig.Int] |
Increment the integer.
|
incr_loop_counter [Abstract_domain.Transfer] | |
incr_loop_counter [Transfer_stmt.S] | |
incr_loop_counter [Gauges_domain.D_Impl.Transfer] | |
indirect_zone_of_lval [Value_util] |
Given a function computing the location of lvalues, computes the memory zone
on which the offset and the pointer expression (if any) of an lvalue depend.
|
initial_state [Initialization.S] | |
initial_state_lib_entry [Initial_state] | |
initial_state_not_lib_entry [Initial_state] | |
initial_state_with_formals [Initialization.S] | |
initialize_var [Abstract_domain.S] | |
initialize_var [Gauges_domain.D_Impl] | |
initialize_var_using_type [Abstract_domain.S] | |
initialize_var_using_type [Cvalue_init] | initialize_var_using_type varinfo state uses the type of varinfo
to create an initial value in state .
|
initialize_var_using_type [Gauges_domain.D_Impl] | |
initialize_var_using_type [Initial_state] | |
initialized [Cvalue.V_Or_Uninitialized] | initialized v returns the definitely initialized, non-escaping
representant of v .
|
inject [Cvalue_domain] | |
inject_address [Abstract_value.S] |
Abstract address for the given varinfo.
|
inject_comp_result [Cvalue.V] | |
inject_int [Cvalue.V] | |
inject_int [Abstract_value.S] | |
inject_ival [Precise_locs] | |
inject_location_bits [Precise_locs] | |
inject_range [Gauges_domain.G.Bounds] | |
inter [Equality_sig.S] |
Intersection.
|
inter [Equality_sig.Set] | |
inter [Hcexprs.BaseToHCESet] | |
inter [Hcexprs.HCEToZone] | |
inter [Alarmset.Status] | |
inter [Alarmset] |
Pointwise intersection of property status: the most precise status is kept.
|
interp_annot [Transfer_logic.S] | |
interp_annot [Eval_annots] | |
interp_boolean [Cvalue.V] | |
interp_call [Eval_stmt] | |
intersects [Equality_sig.S] | intersect s s' = true iff the two equalities both involve the same
element.
|
intersects [Hptset.S] | intersects s1 s2 returns true if and only if s1 and s2
have an element in common
|
interval_key [Main_values] |
Key for intervals.
|
ip_from_precondition [Eval_annots] | |
is_active [Eval_annots.ActiveBehaviors] | |
is_active_aux [Eval_annots.ActiveBehaviors] | |
is_arithmetic [Cvalue.V] |
Returns true if the value may not be a pointer.
|
is_bitfield [Eval_typ] |
Bitfields
|
is_bottom [Cvalue.V_Or_Uninitialized] | |
is_bottom [Cvalue.V] | |
is_bottom_loc [Precise_locs] | |
is_bottom_offset [Precise_locs] | |
is_const_write_invalid [Value_util] |
Detect that the type is const, and that option
-global-const is set.
|
is_empty [FCMap.S] |
Test whether a map is empty or not.
|
is_empty [Partitioning.StateSet] | |
is_empty [Equality_sig.Set] | |
is_empty [Alarmset] |
Is there an assertion with a non True status ?
|
is_empty [State_imp] |
Information
|
is_empty [State_set] |
Information
|
is_global [Widen_hints_ext] | is_global wh returns true iff widening hint wh has a "global" prefix.
|
is_imprecise [Cvalue.V] | |
is_included [Abstract_domain.Lattice] |
Inclusion test.
|
is_included [Abstract_value.S] | |
is_included [Hcexprs.HCEToZone] | |
is_included [Gauges_domain.G.IterationInfo] | |
is_included [Gauges_domain.G.MC] | |
is_included [Gauges_domain.G.MV] | |
is_included [Gauges_domain.G.Bounds] | |
is_included [Gauges_domain.G] | |
is_indeterminate [Cvalue.V_Or_Uninitialized] | is_indeterminate v = false implies v only has definitely initialized
values and non-escaping addresses.
|
is_initialized [Cvalue.V_Or_Uninitialized] | is_initialized v = true implies v is definitely initialized.
|
is_isotropic [Cvalue.V] | |
is_noesc [Cvalue.V_Or_Uninitialized] | is_noesc v = true implies v has no escaping addresses.
|
is_non_terminating_instr [Gui_callstacks_filters] | |
is_non_terminating_instr [Value_results] |
Returns
true iff there exists executions of the statement that does
not always fail/loop (for function calls).
|
is_reachable_stmt [Gui_callstacks_filters] | |
is_top_loc [Precise_locs] | |
is_topint [Cvalue.V] | |
is_value_zero [Value_util] |
Return
true iff the argument has been created by Value_util.zero
|
iter [FCMap.S] | iter f m applies f to all bindings in map m .
|
iter [Equality_sig.S] | iter f s applies f in turn to all elements of s .
|
iter [Partitioning.StateSet] | |
iter [Equality_sig.Set] | |
iter [Alarmset] | |
iter [Hashtbl.S] | |
iter [State_imp] | |
iter [State_builder.Hashtbl] | |
iter [State_set] | |
iter_sorted [State_builder.Hashtbl] | |
J | |
join [Widen_type] | |
join [Abstract_domain.Lattice] |
Semi-lattice structure.
|
join [Abstract_value.S] | |
join [Partitioning.Partition] | |
join [Partitioning.StateSet] | |
join [Gauges_domain.G.MultipleIterations] | |
join [Gauges_domain.G.MC] | |
join [Gauges_domain.G.Bounds] | |
join [Gauges_domain.G] | |
join [Alarmset.Status] | |
join [State_imp] |
Export
|
join [State_set] |
Export
|
join_and_is_included [Abstract_domain.Lattice] |
Do both operations simultaneously
|
join_and_is_included [Gauges_domain.G] | |
join_consecutive_lambda [Gauges_domain.G] | |
join_disjoint [Gauges_domain.G.MV] | |
join_final_states [Split_return] |
Join the given state_set.
|
join_gui_offsetmap_res [Gui_types] | |
join_iterations [Gauges_domain.G] | |
join_list [Alarmset.Status] | |
join_list_predicate_status [Eval_terms] | |
join_predicate_status [Eval_terms] | |
join_same_lambda [Gauges_domain.G] | |
K | |
key [Cvalue_domain] | |
key [Equality_domain.S] | |
kf_assigns_only_result_or_volatile [Eval_typ] |
returns
true if the function assigns only \result or variables
that have volatile qualifier (that are usually not tracked by domains
anyway).
|
kf_of_gui_loc [Gui_types] | |
kf_strategy [Split_return] | |
ki_of_callstack [Value_messages] | |
kill_base [Gauges_domain.G] | |
L | |
leave_loop [Abstract_domain.Transfer] | |
leave_loop [Transfer_stmt.S] | |
leave_loop [Gauges_domain.D_Impl.Transfer] | |
leave_loop [Gauges_domain.G] | |
leave_scope [Abstract_domain.S] | |
leave_scope [Transfer_stmt.Domain] | |
leave_scope [Gauges_domain.D_Impl] | |
legacy_config [Abstractions] |
Legacy configuration of EVA, with only the cvalue domain enabled.
|
length [Partitioning.StateSet] | |
length [Hashtbl.S] | |
length [State_imp] | |
length [State_builder.Hashtbl] |
Length of the table.
|
length [State_set] | |
lift [Gauges_domain.G.Bounds] | |
load_and_merge_function_state [State_import] |
Loads the saved initial global state, and merges it with the given state
(locals plus new globals which were not present in the original AST).
|
loc_bottom [Precise_locs] | |
loc_size [Precise_locs] | |
loc_size [Evaluation.S] | |
loc_to_base [Gauges_domain.G] | |
loc_top [Precise_locs] | |
local [Per_stmt_slevel] |
Slevel to use in this function
|
lval_contains_volatile [Eval_typ] |
Those two expressions indicate that one l-value contained inside
the arguments (or the l-value itself for
lval_contains_volatile ) has
volatile qualifier.
|
lval_ev [Gui_eval] | |
lval_to_loc [Eval_exprs] | |
lval_to_loc_deps_state [Eval_exprs] | |
lval_to_loc_state [Eval_exprs] | |
lval_to_precise_loc [Eval_exprs] | |
lval_to_precise_loc_deps_state [Eval_exprs] | |
lval_to_precise_loc_state [Eval_exprs] | |
lval_zone_ev [Gui_eval] | |
lvaluate [Evaluation.S] | lvaluate ~valuation ~for_writing state lval evaluates the left value
lval in the state state .
|
M | |
main_initial_state_with_formals [Function_args] | |
make [Cvalue.V_Or_Uninitialized] | |
make [Abstractions] |
Builds the abstractions according to a configuration.
|
make_data_all_callstacks [Gui_eval] | |
make_loc_contiguous [Eval_op] |
'Simplify' the location if it represents a contiguous zone: instead
of multiple offsets with a small size, change it into a single offset
with a size that covers the entire range.
|
make_precise_loc [Precise_locs] | |
make_return [Abstract_domain.Transfer] | make_return kf stmt assigned valuation state makes an abstraction of the
return value of the function kf .
|
make_return [Gauges_domain.D_Impl.Transfer] | |
make_type [Datatype.Hashtbl] | |
make_volatile [Cvalue_forward] | make_volatile ?typ v makes the value v more general (to account for
external modifications), whenever typ is None or when it has type
qualifier volatile .
|
make_volatile [Eval_op] | make_volatile ?typ v makes the value v more general (to account for
external modifications), whenever typ is None or when it has type
qualifier volatile
|
malloced_bases [Builtins_malloc] |
All bases that have been dynamically created in the current execution.
|
map [FCMap.S] | map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map [Cvalue.V_Or_Uninitialized] | |
map [Partitioning.StateSet] | |
map [State_set] | |
map2 [Cvalue.V_Or_Uninitialized] |
initialized/escaping information is the join of the information
on each argument.
|
map2 [Gauges_domain.G.Gauge] | |
mapi [FCMap.S] |
Same as
FCMap.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mark_degeneration [Eval_slevel.Computer] | |
mark_green_and_red [Eval_annots] | |
mark_invalid_initializers [Eval_annots] | |
mark_kf_as_called [Value_results] | |
mark_rte [Eval_annots] | |
mark_unreachable [Eval_annots] | |
max_binding [FCMap.S] |
Same as
FCMap.S.min_binding , but returns the largest binding
of the given map.
|
maybe_warn_completely_indeterminate [Warn] |
Print a message about the given location containing a completely
indeterminate value.
|
maybe_warn_div [Warn] |
Emit an alarm about a non-null divisor when the supplied value may
contain zero.
|
maybe_warn_indeterminate [Warn] |
Warn for unitialized or escaping bits in the value passed
as argument.
|
mem [FCMap.S] | mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [Equality_sig.S] | mem x s tests whether x belongs to the equality s .
|
mem [Abstract_domain.Interface] |
Tests whether a key belongs to the domain.
|
mem [Equality_sig.Set] | mem equality set = true iff ∃ eq ∈ set, equality ⊆ eq
|
mem [Structure.External] | |
mem [Hashtbl.S] | |
mem [State_builder.Hashtbl] | |
mem [Parameter_sig.Map] | |
mem [Parameter_sig.Set] |
Does the given element belong to the set?
|
mem_builtin [Builtins] |
Does the builtin table contain an entry for
name ?
|
memo [Datatype.Hashtbl] | memo tbl k f returns the binding of k in tbl .
|
memo [State_builder.Hashtbl] |
Memoization.
|
merge [FCMap.S] | merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge [Partitioning.StateSet] | |
merge [Hptset.S] | |
merge [Per_stmt_slevel] |
Slevel merge strategy for this function
|
merge [Value_results] | |
merge [State_set] |
Merge the two sets together.
|
merge [Value.Value_results] | |
merge_after_states_in_db [Value_results] | |
merge_into [State_set] |
Raise
Unchanged if the first set was
already included in into
|
merge_referenced_formals [Function_args] | |
merge_results [Eval_slevel.Computer] | |
merge_set_return_new [Partitioning.Partition] | |
merge_set_return_new [State_imp] | |
merge_states_in_db [Value_results] | |
min_binding [FCMap.S] |
Return the smallest binding of the given map
(with respect to the
Ord.compare ordering), or raise
Not_found if the map is empty.
|
msg_status [Eval_annots] | |
mul [Cvalue.V] | |
mul [Gauges_domain.G.Gauge] | |
mul [Gauges_domain.G.Bounds] | |
mul_ct [Gauges_domain.G.Gauge] | |
mul_ct [Gauges_domain.G.Bounds] | |
mv_minus_mc [Gauges_domain.G] | |
N | |
narrow [Cvalue.V_Offsetmap] | |
narrow [Abstract_value.S] | |
narrow [Gauges_domain.G.Bounds] | |
narrow [State_set] | |
narrow_list [State_set] | |
need_cast [Eval_typ] |
return
true if the two types are statically distinct, and a cast
from one to the other may have an effect on an abstract value.
|
neg [Gauges_domain.G.Gauge] | |
neg [Gauges_domain.G.Bounds] | |
new_alarm [Value_messages] | |
new_counter [Mem_exec2] |
Counter that must be used each time a new call is analyzed, in order
to refer to it later
|
new_counter [Mem_exec] |
Counter that must be used each time a new call is analyzed, in order
to refer to it later
|
new_status [Value_messages] | |
no_memoization_enabled [Mark_noresults] | |
no_offset [Abstract_location.S] | |
none [Alarmset] |
no alarms: all potential assertions have a True status.
|
null_ev [Gui_eval] | |
num_hints [Widen_type] |
Define numeric hints for one or all variables (
None ),
for a certain stmt or for all statements (None ).
|
O | |
octagon_key [Apron_domain] | |
of_char [Cvalue.V] | |
of_exp [Hcexprs.HCE] | |
of_int64 [Cvalue.V] | |
of_list [Partitioning.StateSet] | |
of_list [State_set] | |
of_list_forget_history [State_set] | |
of_lval [Hcexprs.HCE] | |
of_string [Split_strategy] | |
off [Parameter_sig.Bool] |
Set the boolean to
false .
|
offset_bottom [Precise_locs] | |
offset_cardinal_zero_or_one [Abstract_location.S] |
Needed for Evaluation.get_influential_vars
|
offset_top [Precise_locs] | |
offset_zero [Precise_locs] | |
offsetmap_contains_imprecision [Warn] |
Returns the first eventual imprecise part contained in an offsetmap
|
offsetmap_contains_local [Locals_scoping] | |
offsetmap_matches_type [Cvalue_forward] | |
offsetmap_matches_type [Eval_typ] | offsetmap_matches_type t o returns true if either: o contains a single scalar binding, of the expected scalar type t
(float or integer), o contains multiple bindings, pointers, etc., t is not a scalar type.
|
offsetmap_of_lv [Eval_exprs] |
May raise
Int_Base.Error_Top
|
offsetmap_of_v [Eval_op] |
Transformation a value into an offsetmap of size
sizeof(typ) bytes.
|
offsetmap_top_addresses_of_locals [Locals_scoping] | offsetmap_top_addresses_of_locals is_local returns a function that
topifies all the parts of an offsetmap that contains a pointer verifying
is_local .
|
offsm_key [Offsm_value] | |
ok [Apron_domain] |
Are apron domains available?
|
on [Parameter_sig.Bool] |
Set the boolean to
true .
|
on_cvalue_ival [Gauges_domain.G.Gauge] | |
one [Cvalue.CardinalEstimate] | |
opt2 [Gauges_domain.G] | |
output [Parameter_sig.With_output] |
To be used by the plugin to output the results of the option
in a controlled way.
|
P | |
pair [Equality_sig.S] |
The equality between two elements.
|
parameters_correctness [Value_parameters] | |
parameters_tuning [Value_parameters] | |
partially_overlap [Abstract_location.S] | |
partition [FCMap.S] | partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
partition_terminating_instr [Value_results] |
Returns the list of terminating callstacks and the list of non-terminating callstacks.
|
paste_offsetmap [Eval_op] |
Temporary.
|
ploc_key [Main_locations] |
Key for precise locs.
|
polka_equalities_key [Apron_domain] | |
polka_loose_key [Apron_domain] | |
polka_strict_key [Apron_domain] | |
pop_call_stack [Value_util] | |
post_kind [Eval_annots] | |
postconditions_mention_result [Value_util] |
Does the post-conditions of this specification mention
\result ?
|
pp_bhv [Eval_annots.ActiveBehaviors] | |
pp_callstack [Value_util] |
Prints the current callstack.
|
pp_header [Eval_annots] | |
pp_p_kind [Eval_annots] | |
precompute_widen_hints [Widen] |
Parses all widening hints defined via the widen_hint syntax extension.
|
predicate_deps [Eval_terms] | |
predicate_ev [Gui_eval] | |
pretty [Widen_type] |
Pretty-prints a set of hints (for debug purposes only).
|
pretty [Cvalue.CardinalEstimate] | |
pretty [Partitioning.Partition] | |
pretty [Partitioning.StateSet] | |
pretty [Gauges_domain.D_Impl] | |
pretty [Gauges_domain.G.Gauge] | |
pretty [Gauges_domain.G.Bounds] | |
pretty [Gauges_domain.G] | |
pretty [Alarmset] | |
pretty [State_imp] | |
pretty [State_set] | |
pretty_actuals [Value_util] | |
pretty_callstack [Gui_types] | |
pretty_callstack_short [Gui_types] | |
pretty_current_cfunction_name [Value_util] | |
pretty_debug [Value_types.Callstack] | |
pretty_debug [Equality_domain.S] | |
pretty_debug [Equality.Element] | |
pretty_debug [Hptset.S] | |
pretty_debug [Hcexprs.HCE] | |
pretty_debug [Gauges_domain.G.Bounds] | |
pretty_gui_offsetmap_res [Gui_types] | |
pretty_gui_res [Gui_types] | |
pretty_gui_selection [Gui_types] | |
pretty_iteration_info [Gauges_domain.G] | |
pretty_loc [Precise_locs] | |
pretty_loc [Abstract_location.S] | |
pretty_loc_bits [Precise_locs] | |
pretty_logic_evaluation_error [Eval_terms] | |
pretty_long_log10 [Cvalue.CardinalEstimate] | |
pretty_loop_info [Gauges_domain.G] | |
pretty_loop_step [Gauges_domain.G] | |
pretty_offset [Precise_locs] | |
pretty_offset [Abstract_location.S] | |
pretty_predicate_status [Eval_terms] | |
pretty_short [Value_types.Callstack] |
Print a call stack without displaying call sites.
|
pretty_state_as_c_assert [Builtins_nonfree_print_c] | |
pretty_state_as_c_assignments [Builtins_nonfree_print_c] | |
pretty_stitched_offsetmap [Eval_op] | |
pretty_strategies [Split_return] | |
pretty_typ [Cvalue.V] | |
print [Structure.Key] | |
process_inactive_behavior [Eval_annots] | |
process_inactive_behaviors [Eval_annots] | |
process_inactive_postconds [Eval_annots] | |
project [Cvalue_domain] | |
project [Equality_domain.S] | |
project_ival [Cvalue.V] |
Raises
Not_based_on_null if the value may be a pointer.
|
project_ival_bottom [Cvalue.V] | |
prologue [Separate] | |
push_call_stack [Value_util] | |
R | |
range_inclusion [Eval_typ] |
Check inclusion of two integer ranges.
|
range_lower_bound [Eval_typ] | |
range_upper_bound [Eval_typ] | |
reduce [Abstractions.Value] | |
reduce [Evaluation.Value] |
Inter-reduction of values.
|
reduce [Evaluation.S] | reduce ~valuation state expr positive evaluates the expresssion expr
in the state state , and then reduces the valuation such that
the expression expr evaluates to a zero or a non-zero value, according
to positive .
|
reduce_binding [Cvalue.Model] | reduce_binding state loc v refines the value associated to
loc in state according to v , by keeping the values common
to the existing value and v .
|
reduce_by_accessed_loc [Eval_exprs] | |
reduce_by_cond [Eval_exprs] |
Never returns
Model.bottom .
|
reduce_by_danglingness [Cvalue.V_Or_Uninitialized] | reduce_by_danglingness dangling v reduces v so that its result r
verifies \dangling(r) if dangling is true , and
!\dangling(r) otherwise.
|
reduce_by_initialized_defined [Eval_op] | |
reduce_by_initializedness [Cvalue.V_Or_Uninitialized] | reduce_by_initializedness initialized v reduces v so that its result
r verifies \initialized(r) if initialized is true , and
!\initialized(r) otherwise.
|
reduce_by_predicate [Abstract_domain.Logic] | |
reduce_by_predicate [Gauges_domain.D_Impl] | |
reduce_by_predicate [Eval_terms] | |
reduce_by_valid_loc [Eval_op] | |
reduce_further [Abstract_domain.Queries] |
Given a reduction
expr = value , provides more reductions that may
be performed.
|
reduce_further [Gauges_domain.D_Impl] | |
reduce_indeterminate_binding [Cvalue.Model] |
Same behavior as
reduce_previous_binding , but takes a value
with 'undefined' and 'escaping addresses' flags.
|
reduce_index_by_array_size [Abstract_location.S] | reduce_index_by_array_size ~size_expr ~index_expr size index reduces
the value index to fit into the inverval 0..(size-1) .
|
reduce_loc_by_validity [Abstract_location.S] | reduce_loc_by_validity for_writing bitfield lval loc reduce the location
loc by its valid part for a read or write operation, according to the
for_writing boolean.
|
reduce_previous_binding [Cvalue.Model] | reduce_previous_binding state loc v reduces the value associated to loc
in state; use with caution, as the inclusion between the new and the
old value is not checked.
|
refine_active [Eval_annots] | |
register_builtin [Builtins] |
Register the given OCaml function as a builtin, that will be used
instead of the Cil C function of the same name
|
register_initial_state [Abstract_domain.Store] | |
register_malloced_base [Builtins_malloc] |
Should not be used by casual users.
|
register_state_after_stmt [Abstract_domain.Store] | |
register_state_before_stmt [Abstract_domain.Store] | |
registered_builtins [Builtins] |
Returns a list of the pairs (name, builtin_sig) registered via
register_builtin .
|
reinterpret [Abstract_value.S] |
Read the given value with the given type.
|
reinterpret [Evaluation.S] | |
reinterpret [Cvalue_forward] | |
reinterpret [Eval_op] | |
reinterpret_float [Eval_op] |
Read the given value value as a float int of the given
fkind .
|
remember_bases_with_locals [Locals_scoping] |
Add the given set of bases to an existing clobbered set
|
remember_if_locals_in_offsetmap [Locals_scoping] |
Same as above with an entire offsetmap
|
remember_if_locals_in_value [Locals_scoping] | remember_locals_in_value clob loc v adds all bases pointed to by loc
to clob if v contains the address of a local or formal
|
remove [FCMap.S] | remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove [Equality_sig.S] | remove x s returns the equality between all elements of s , except x .
|
remove [Equality_sig.Set] | remove elt set remove any occurrence of elt in set .
|
remove [Hcexprs.BaseToHCESet] | |
remove [Hcexprs.HCEToZone] | |
remove [Eval.Valuation] | |
remove [Hashtbl.S] | |
remove [State_builder.Hashtbl] | |
remove_coeffs [Gauges_domain.G] | |
remove_indeterminateness [Cvalue.V_Or_Uninitialized] |
Remove 'unitialized' and 'escaping addresses' flags from the argument
|
remove_loc [Eval.Valuation] | |
remove_variables [Cvalue.Model] |
For variables that are coming from the AST, this is equivalent to
uninitializing them.
|
reorder [Partitioning.StateSet] | |
reorder [State_set] |
Invert the order in which the states are iterated over
|
replace [Hashtbl.S] | |
replace [State_builder.Hashtbl] |
Add a new binding.
|
reset [Hashtbl.S] | |
reset [Value_perf] |
Reset the internal state of the module; to call at the very
beginning of the analysis.
|
resolv_func_vinfo [Eval_exprs] | |
resolve_functions [Abstract_value.S] | resolve_functions ~typ_pointer v finds within v all the functions
with a type compatible with typ_pointer .
|
resolve_functions [Eval_typ] |
given
(funs, warn) = resolve_functions typ v , funs is the set of
functions pointed to by v that have a type compatible with typ .
|
restrict_loc [Domain_lift.Conversion] | |
restrict_val [Domain_lift.Conversion] | |
restrict_val [Location_lift.Conversion] | |
results [Eval_slevel.Computer] | |
results_kf_computed [Gui_eval] |
Catch the fact that we are in a function for which
-no-results or one
of its variants is set.
|
return [Transfer_stmt.S] | |
returned_value [Library_functions] | |
reuse [Abstract_domain.S] | |
reuse [Mem_exec2.Domain] | |
reuse [Gauges_domain.D_Impl] | |
reuse_previous_call [Mem_exec2.Make] | reuse_previous_call kf init_state args searches amongst the previous
analyzes of kf one that matches the initial state init_state and the
values of arguments args .
|
reuse_previous_call [Mem_exec] | reuse_previous_call (kf, ki) init_state searches amongst the previous
analyzes of kf one that matches the initial state init_state .
|
run [Compute_functions] | |
S | |
safe_argument [Backward_formals] | safe_argument e returns true if e (which is supposed to be
an actual parameter) is guaranteed to evaluate in the same way before and
after the call.
|
sanitize_v [Gauges_domain.G.Gauge] | |
save_globals_state [State_import] |
Saves the final state of globals variables after the return statement of
the function defined via
Value_parameters.SaveFunctionState .
|
self [Equality.Element] | |
self [Hcexprs.HCE] | |
set [Abstract_domain.Interface] |
For a key of type
k key : if the states of this domain (of type t ) contain a part (of type k )
from the domain identified by the key,
then set key d state returns the state state in which this part
has been replaced by d ., otherwise, set key _ is the identity function.
|
set [Structure.External] | |
set [State_builder.Ref] |
Change the referenced value.
|
set_callstacks_filter [Gui_callstacks_filters] |
This function must be called when callstacks are focused.
|
set_current_state [Value_messages] | |
set_loc [Value_util] | |
set_output_dependencies [Parameter_sig.With_output] |
Set the dependencies for the output of the option.
|
set_possible_values [Parameter_sig.String] |
Set what are the acceptable values for this parameter.
|
set_range [Parameter_sig.Int] |
Set what is the possible range of values for this parameter.
|
set_results [Value_results] | |
set_results [Value.Value_results] | |
set_syntactic_context [Valarms] | |
shape [Hptset.S] |
Export the shape of the set.
|
shift_left [Cvalue.V] | |
shift_offset [Precise_locs] | |
shift_offset_by_singleton [Precise_locs] | |
shift_right [Cvalue.V] | |
should_memorize_function [Mark_noresults] | |
signal_abort [Partitioned_dataflow] |
Mark the analysis as aborted.
|
signal_abort [Eval_slevel] |
Mark the analysis as aborted.
|
singleton [FCMap.S] | singleton x y returns the one-element map that contains a binding y
for x .
|
singleton [Partitioning.StateSet] | |
singleton [Equality_sig.Set] | |
singleton [Alarmset] | |
singleton [State_imp] | |
singleton [State_set] | |
singleton' [Partitioning.StateSet] | |
size [Abstract_location.S] | |
sizeof_lval_typ [Eval_typ] |
Size of the type of a lval, taking into account that the lval might have
been a bitfield.
|
split [FCMap.S] | split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
split_by_evaluation [Evaluation.S] | |
split_disjunction_and_reduce [Eval_terms] |
If
reduce is true, reduce in all cases.
|
split_final_states [Transfer_stmt.S] | |
start_call [Abstract_domain.Transfer] |
Decision on a function call:
start_call stmt call valuation state decides on the analysis of
a call site.
|
start_call [Cvalue_transfer.Transfer] | |
start_call [Gauges_domain.D_Impl.Transfer] | |
start_doing [Value_perf] | |
start_stmt [Alarmset] | |
start_stmt [Valarms] | |
state_top_addresses [Locals_scoping] | state_top_addresses kf clob l state topifies all references to the
variables in l .
|
state_top_addresses_of_locals [Locals_scoping] | state_top_addresses_of_locals exact warn topoffsm clob generalizes
topoffsm into a function that topifies a memory state.
|
stats [Hashtbl.S] | |
stop_doing [Value_perf] |
Call
start_doing when finishing analyzing a function.
|
stop_if_stop_at_first_alarm_mode [Value_util] | |
storage [Domain_builder.InputDomain] | |
storage [Domain_store.InputDomain] | |
store_computed_call [Mem_exec2.Make] | store_computed_call kf init_state args call_results memoizes the fact
that calling kf with initial state init_state and arguments args
resulted in the results call_results .
|
store_computed_call [Mem_exec] | store_computed_call (kf, ki) init_state actuals outputs memoizes the fact
that calling kf at statement ki , with initial state init_state
and arguments actuals resulted in the states outputs ; the expressions
in the actuals are not used.
|
store_gauge [Gauges_domain.G] | |
structural_descr [Gauges_domain.G.MultipleIterations] | |
structural_descr [Locals_scoping] | |
structure [Abstract_domain.S_with_Structure] |
A structure matching the type of the domain.
|
structure [Gauges_domain.D_Impl] | |
structure [Abstract_location.Internal] | |
structure [Abstract_value.Internal] | |
structure [Structure.Internal] | |
sub [Gauges_domain.G.Gauge] | |
sub [Gauges_domain.G.Bounds] | |
sub_min_max_cvalue [Gauges_domain.G] | |
sub_mv [Gauges_domain.G] | |
sub_untyped_pointwise [Cvalue.V] |
See
Locations.sub_pointwise .
|
subset [Equality_sig.S] | |
subset [Equality_sig.Set] | |
succ [Gauges_domain.G.MultipleIterations] | |
succ [Gauges_domain.G.Bounds] | |
T | |
tag [Structure.Key] | |
term_ev [Gui_eval] | |
tlval_ev [Gui_eval] | |
tlval_zone_ev [Gui_eval] | |
to_exp [Hcexprs.HCE] | |
to_ival [Gauges_domain.G.Bounds] | |
to_list [Partitioning.Partition] | |
to_list [Partitioning.StateSet] | |
to_list [State_imp] | |
to_list [State_set] | |
to_set [Partitioning.Partition] | |
to_set [State_imp] | |
to_string [Split_strategy] | |
to_value [Abstract_location.S] | |
top [Abstract_domain.Lattice] |
Greatest element.
|
top [Abstract_value.S] | |
top [Gauges_domain.D_Impl] | |
top [Gauges_domain.G] | |
top [Locals_scoping] | |
top_addresses_of_locals [Locals_scoping] |
Return two functions that topifies all references to the locals and formals
of the given function.
|
top_int [Abstract_value.S] | |
tracked_variable [Gauges_domain.G] | |
translate_exp [Gauges_domain.G] | |
U | |
uncheck_add [Partitioning.StateSet] | |
uninitialize_blocks_locals [Cvalue.Model] | |
uninitialized [Cvalue.V_Or_Uninitialized] |
Returns the canonical representant of a definitely uninitialized value.
|
union [Equality_sig.S] |
Union.
|
union [Equality_sig.Set] | |
union [Hcexprs.BaseToHCESet] | |
union [Hcexprs.HCEToZone] | |
union [Alarmset] |
Pointwise union of property status: the least precise status is kept.
|
unite [Equality_sig.Set] | unite a b map unites a and b in map .
|
unsafe_reinterpret [Cvalue_forward] | |
unspecify_escaping_locals [Cvalue.V_Or_Uninitialized] | |
update [Abstract_domain.Transfer] | update valuation t updates the state t by the values of expressions
and the locations of lvalues stored in valuation .
|
update [Gauges_domain.D_Impl.Transfer] | |
V | |
v_of_offsetmap [Eval_op] |
Reads the contents of the offsetmap (assuming it contains
sizeof(typ)
bytes) as a value of type V.t, then convert the result to type typ
|
v_uninit_of_offsetmap [Eval_op] |
Reads the contents of the offsetmap (assuming it contains
sizeof(typ)
bytes), and return them as an uninterpreted value.
|
valid_cardinal_zero_or_one [Precise_locs] |
Is the restriction of the given location to its valid part precise enough
to perform a strong read, or a strong update.
|
valid_part [Precise_locs] |
Overapproximation of the valid part of the given location for a read or write
operation, according to the
for_writing boolean.
|
value_assigned [Eval] | |
var_hints [Widen_type] |
Define a set of bases to widen in priority for a given statement.
|
var_of_base [Gui_types] | |
vars_in_gui_res [Gui_types] | |
verify_assigns_from [Eval_annots] | |
W | |
warn_all_mode [CilE] |
Emit all messages, including alarms and informative messages
regarding the loss of precision.
|
warn_all_mode [Value_util] | |
warn_all_quiet_mode [Value_util] | |
warn_div [Valarms] |
division.
|
warn_escapingaddr [Valarms] |
warning to be emitted when two incompatible accesses to a location are
done in unspecified order.
|
warn_float [Warn] | |
warn_float_addr [Warn] | |
warn_float_to_int_overflow [Valarms] | |
warn_imprecise_lval_read [Warn] | |
warn_inactive [Eval_annots] | |
warn_incompatible_fun_pointer [Valarms] | |
warn_indeterminate [Value_util] | |
warn_index [Valarms] | warn_index w ~positive ~range emits a warning signaling an out of bounds
access.
|
warn_integer_overflow [Valarms] | |
warn_locals_escape [Warn] | |
warn_locals_escape_result [Warn] | |
warn_mem_read [Valarms] | |
warn_mem_write [Valarms] | |
warn_modified_result_loc [Warn] |
This function should be used to treat a call
lv = kf(...) .
|
warn_nan_infinite [Valarms] | |
warn_none_mode [CilE] |
Do not emit any message.
|
warn_overlap [Warn] | |
warn_overlap [Valarms] | |
warn_pointer_comparison [Valarms] |
warn on invalid pointer comparison.
|
warn_pointer_subtraction [Valarms] | |
warn_reduce_by_accessed_loc [Eval_exprs] | |
warn_reduce_indeterminate_offsetmap [Warn] |
If the supplied offsetmap has an arithmetic type and contains indeterminate
bits (uninitialized, or escaping address), raises the corresponding alarm(s)
and returns the reduced offsetmap and state.
|
warn_right_exp_imprecision [Warn] | |
warn_separated [Valarms] | |
warn_shift [Valarms] |
Warn that the RHS of a shift operator must be positive, and optionnally
less than the given size.
|
warn_shift_left_positive [Valarms] |
Warn that the LHS of the left shift operator must be positive.
|
warn_top [Warn] |
Abort the analysis, signaling that Top has been found.
|
warn_uninitialized [Valarms] | |
warn_valid_string [Valarms] | |
warning [Value_messages] | |
warning_once_current [Value_util] | |
widen [Abstract_domain.Lattice] | widen h t1 t2 is an over-approximation of join t1 t2 .
|
widen [Gauges_domain.G.MultipleIterations] | |
widen [Gauges_domain.G.MC] | |
widen [Gauges_domain.G.MV] | |
widen [Gauges_domain.G.Bounds] | |
widen [Gauges_domain.G] | |
with_alarm_stop_at_first [Value_util] | |
with_alarms_raise_exn [Value_util] | |
wrap_double [Eval_op] | |
wrap_float [Eval_op] | |
wrap_int [Eval_op] | |
wrap_ptr [Eval_op] | |
wrap_size_t [Eval_op] |
Specialization of the function above for standard types
|
write_abstract_value [Eval_op] | write_abstract_value ~with_alarms state lv typ_lv loc_lv v
writes v at loc_lv in state , casting v to respect the type
typ_lv of lv .
|
written_formals [Backward_formals] | written_formals kf is an over-approximation of the formals of kf
which may be internally overwritten by kf during its call.
|
Z | |
zero [Abstract_value.S] | |
zero [Gauges_domain.G.Bounds] | |
zero [Value_util] |
Retun a zero constant compatible with the type of the argument
|
zone_of_expr [Value_util] |
Given a function computing the location of lvalues, computes the memory zone
on which the value of an expression depends.
|