(>>=) [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] | |
abs [Numerors_interval] | |
abs [Numerors_float] |
Absolute value
|
active_behaviors [Transfer_logic.ActiveBehaviors] | |
add [Map.S] | add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add [Numerors_arithmetics.Arithmetic.Backward] | |
add [Numerors_arithmetics.Arithmetic.Forward] | |
add [Numerors_interval] |
These functions perform arithmetic operations on intervals using the
precision <prec>.
|
add [Numerors_float] |
The following functions perform floating-point arithmetic operations at
the precision <prec> and using the rounding mode <rnd>.
|
add [Partitioning_index.Make] |
Adds a state into an index.
|
add [Powerset.S] | |
add [Equality.Equality] | add x s returns the equality between all elements of s and x .
|
add [Simple_memory.S] | add loc typ v state binds loc to v in state.
|
add [Eval.Valuation] | |
add [State_builder.Hashtbl] |
Add a new binding.
|
add' [Powerset.S] | |
add_binding [Cvalue.Model] | add_binding state loc v simulates the effect of writing v at location
loc in state .
|
add_flow_annot [Eva_annotations] | |
add_indeterminate_binding [Cvalue.Model] | |
add_kf_caller [Value_results] | |
add_nan [Numerors_interval] |
Add NaN into the interval
|
add_red_alarm [Red_statuses] | |
add_red_property [Red_statuses] | |
add_slevel_annot [Eva_annotations] | |
add_subdivision_annot [Eva_annotations] | |
add_unroll_annot [Eva_annotations] | |
add_untyped [Cvalue.V] | add_untyped ~factor e1 e2 computes e1+factor*e2 using C semantic
for +, i.e.
|
add_untyped_under [Cvalue.V] |
Under-approximating variant of
Cvalue.V.add_untyped .
|
alarm_report [Value_util] |
Emit an alarm, either as warning or as a result, according to
status associated to
Value_parameters.wkey_alarm
|
all [Alarmset] |
all alarms: all potential assertions have a Unknown status.
|
all [Domain_mode.Mode] |
Default mode: all permissions are granted.
|
all_values [Cvalue.V] | all_values ~size v returns true iff v contains all integer values
representable in size bits.
|
alloc_size_ok [Builtins_malloc] | |
apply [Numerors_arithmetics] |
Apply an operation on each fields of the operands
|
apply_builtin [Builtins] | |
apply_on_all_locs [Eval_op] | apply_all_locs f loc state folds f on all the atomic locations
in loc , provided there are less than plevel .
|
apply_sign [Numerors_float] |
Returns a element containing the same value as <dst> but with the sign
of <src>
|
are_comparable [Cvalue_forward] | |
assign [Simpler_domains.Simple_Cvalue] | |
assign [Simpler_domains.Minimal] | |
assign [Abstract_domain.Transfer] | assign kinstr lv expr v valuation state is the transfer function for the
assignment lv = expr for state .
|
assign [Transfer_stmt.S] | |
assume [Simpler_domains.Simple_Cvalue] | |
assume [Simpler_domains.Minimal] | |
assume [Abstract_domain.Transfer] |
Transfer function for an assumption.
|
assume [Transfer_stmt.S] | |
assume [Evaluation.S] | assume ~valuation state expr value assumes in the valuation that
the expression expr has the value value in the state state ,
and backward propagates this information to the subterm of expr .
|
assume_bounded [Cvalue_forward] | |
assume_bounded [Abstract_value.S] | |
assume_comparable [Cvalue_forward] | |
assume_comparable [Abstract_value.S] | |
assume_no_overlap [Abstract_location.S] |
Assumes that two locations do not overlap.
|
assume_non_zero [Cvalue_forward] | |
assume_non_zero [Abstract_value.S] | |
assume_not_nan [Cvalue_forward] | |
assume_not_nan [Abstract_value.S] | |
assume_pointer [Cvalue_forward] | |
assume_pointer [Abstract_value.S] |
Assumes that the abstract value only represents well-formed pointer values:
pointers either to an element of an array object or one past the last
element of an array object.
|
assume_valid_location [Abstract_location.S] |
Assumes that the given location is valid for a read or write operation,
according to the
for_writing boolean.
|
B | |
backward_add [Numerors_interval] |
These functions perform backward propagation for arithmetic
|
backward_binop [Cvalue_backward] |
This function tries to reduce the argument values of a binary operation,
given its result.
|
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_cast [Cvalue_backward] |
This function tries to reduce the argument of a cast, given the result of
the cast.
|
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_comp_float_left_false [Cvalue.V] | |
backward_comp_float_left_true [Cvalue.V] | |
backward_comp_int_left [Cvalue.V] | |
backward_comp_left_from_type [Eval_op] |
Reduction of a
Cvalue.V.t by == , != , >= , > , <= and < .
|
backward_div [Numerors_interval] | |
backward_field [Abstract_location.S] | |
backward_ge [Numerors_interval] | |
backward_gt [Numerors_interval] | |
backward_index [Abstract_location.S] | |
backward_le [Numerors_interval] |
These functions perform backward propagation on intervals using the
precision <prec>
|
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_lt [Numerors_interval] | |
backward_mul [Numerors_interval] | |
backward_mult_int_left [Cvalue.V] | |
backward_pointer [Abstract_location.S] | |
backward_sub [Numerors_interval] | |
backward_unop [Cvalue_backward] |
This function tries to reduce the argument value of an unary operation,
given its result.
|
backward_unop [Abstract_value.S] |
Backward evaluation of the unary operation
unop arg = res ;
tries to reduce the argument arg according to res .
|
backward_variable [Abstract_location.S] | |
bindings [Map.S] |
Return the list of all bindings of the given map.
|
bitwise [Abstractions.Config] | |
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 [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 [Map.S] |
Return the number of bindings of a map.
|
cardinal [Equality.Set] | |
cardinal [Equality.Equality] |
Return the number of elements of the equality.
|
cardinal_estimate [Cvalue.Model] | |
cardinal_estimate [Cvalue.V] | cardinal_estimate v ~size returns an estimation of the cardinal
of v , knowing that v fits in size bits.
|
cardinal_zero_or_one [Precise_locs] |
Should not be used,
Precise_locs.valid_cardinal_zero_or_one is almost always more
useful
|
cast [Offsm_value] | |
cast_float_to_float [Cvalue.V] | |
cast_float_to_int [Cvalue.V] | |
cast_float_to_int [Cvalue_forward] | |
cast_float_to_int_inverse [Cvalue.V] | |
cast_int_to_float [Cvalue.V] | |
cast_int_to_float_inverse [Cvalue.V] | |
cast_int_to_int [Cvalue.V] | cast_int_to_int ~size ~signed v applies to the abstract value v the
conversion to the integer type described by size and signed .
|
change_callstacks [Value_results] |
Change the callstacks for the results for which this is meaningful.
|
change_callstacks [Eva.Value_results] | |
change_prec [Numerors_arithmetics] |
Return a new value with the same fields as the input but with
an <approx> field with the given precision
|
change_prec [Numerors_interval] |
Change the precision of the bounds
|
change_prec [Numerors_float] |
Change the precision
|
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 [Map.S] |
Return one binding of the given map, or raise
Not_found if
the map is empty.
|
choose [Equality.Set] | |
choose [Equality.Equality] |
Return the representative of the equality.
|
choose_opt [Map.S] |
Return one binding of the given map, or
None if
the map is empty.
|
classify_as_scalar [Eval_typ] | |
classify_pre_post [Gui_eval] |
State in which the predicate, found in the given function,
should be evaluated
|
cleanup_results [Mem_exec] |
Clean all previously stored results
|
clear [State_builder.Hashtbl] |
Clear the table.
|
clear [State_builder.Ref] |
Reset the reference to its default value.
|
clear_caches [Hptset.S] |
Clear all the caches used internally by the functions of this module.
|
clear_call_stack [Value_util] |
Functions dealing with call stacks.
|
clear_default [Gui_callstacks_manager] | |
clear_englobing_exprs [Eval.Clear_Valuation] |
Removes from the valuation all the subexpressions of
expr that contain
subexpr , except subexpr itself.
|
clobbered_set_from_ret [Builtins] | clobbered_set_from_ret state ret can be used for functions that return
a pointer to where they have written some data.
|
combine [Alarmset] |
Combines two alarm maps carrying different sets of alarms.
|
combine_base_precise_offset [Precise_locs] | |
combine_loc_precise_offset [Precise_locs] | |
compare [Map.S] |
Total ordering between maps.
|
compare [Simpler_domains.Minimal] | |
compare [Numerors_arithmetics] | |
compare [Numerors_interval] |
Comparison functions
|
compare [Numerors_float] |
Comparison functions
|
compare [Numerors_utils.Sign] | |
compare [Numerors_utils.Precisions] | |
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 [Auto_loop_unroll.Make] | |
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] |
Creates the configuration according to the analysis parameters.
|
configure_precision [Value_parameters] | |
constant [Abstract_value.S] |
Embeds C constants into value abstractions: returns an abstract value
for the given constant.
|
contains [Equality.Set] | contains elt set = true iff elt belongs to an equality of set .
|
contains_a_zero [Numerors_interval] |
Check if there is a zero between the bounds of its input (without
considering the signs
|
contains_infinity [Numerors_interval] |
Check if its input contains at least an infinite bound
|
contains_nan [Numerors_interval] |
Check if its input contains at least a NaN value
|
contains_neg_zero [Numerors_interval] |
Check if there is a negative zero between the bounds of its input
|
contains_non_zero [Cvalue.V] | |
contains_pos_zero [Numerors_interval] |
Check if there is a positive zero between the bounds of its input
|
contains_single_elt [Hptset.S] | |
contains_strictly_neg [Numerors_interval] |
Check if there is at least a strictly negative value in its input
|
contains_strictly_pos [Numerors_interval] |
Check if there is at least a strictly positive value in its input
|
contains_zero [Cvalue.V] | |
contents [Trace_partitioning.Make] | |
conv_comp [Value_util] | |
conv_relation [Value_util] | |
copy [Datatype.S] |
Deep copy: no possible sharing between
x and copy x .
|
copy_lvalue [Analysis.Results] | |
copy_lvalue [Evaluation.S] |
Computes the value of a lvalue, with possible indeterminateness: the
returned value may be uninitialized, or contain escaping addresses.
|
cos [Numerors_float] | |
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 [Numerors_arithmetics] |
Create a record from intervals
|
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 [Traces_domain] | |
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 [Abstractions.Config] | |
cvalue_initial_state [Analysis] |
Return the initial state of the cvalue domain only.
|
D | |
dbetween [Numerors_value] |
Returns the abstraction corresponding to the join of the approximation of
the inputs.
|
deep_fold [Equality.Set] | |
default [Widen_type] |
A default set of hints
|
default [Abstractions.Config] |
The default configuration of Eva.
|
default_offsetmap [Cvalue.Default_offsetmap] | |
denormalized [Numerors_utils.Precisions] |
Returns the integer corresponding to the exponent of the denormalized
numbers of the given precision.
|
display [Value_perf] |
Display a complete summary of performance informations.
|
distinct_subpart [Cvalue_domain] | |
div [Cvalue.V] | |
div [Numerors_arithmetics.Arithmetic.Backward] | |
div [Numerors_arithmetics.Arithmetic.Forward] | |
div [Numerors_interval] | |
div [Numerors_float] | |
dkey [Widen_hints_ext] | |
dkey_callbacks [Value_parameters] |
Debug category used when using Eva callbacks when recording the results of
a function analysis.
|
dkey_cvalue_domain [Value_parameters] |
Debug category used to print the cvalue domain on Frama_C_
dump|show _each
functions.
|
dkey_final_states [Value_parameters] | |
dkey_incompatible_states [Value_parameters] | |
dkey_initial_state [Value_parameters] |
Debug categories responsible for printing initial and final states of Value.
|
dkey_iterator [Value_parameters] |
Debug category used to print information about the iteration
|
dkey_pointer_comparison [Value_parameters] |
Debug category used to print information about invalid pointer comparisons
|
dkey_summary [Value_parameters] | |
dkey_widening [Value_parameters] |
Debug category used to print the usage of widenings.
|
drain [Trace_partitioning.Make] |
Remove all states from the tank, leaving it empty as if it was just
created by
empty_tank
|
dump_garbled_mix [Value_util] |
print information on the garbled mix created during evaluation
|
dynamic_register [Abstractions] |
Register a dynamic abstraction: the abstraction is built by applying
the last argument when starting an analysis, if the -eva-domains option
has been set to
name .
|
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 [Map.S] |
The empty map.
|
empty [Widen_type] |
An empty set of hints
|
empty [Simpler_domains.Simple_Cvalue] | |
empty [Simpler_domains.Minimal] | |
empty [Abstract_domain.S] |
The initial state with which the analysis start.
|
empty [Partitioning_index.Make] |
Creates an empty index.
|
empty [Partition.MakeFlow] | |
empty [Partition] | |
empty [Powerset.S] | |
empty [Equality.Set] | |
empty [Eval.Valuation] | |
empty_flow [Trace_partitioning.Make] | |
empty_lvalues [Hcexprs] | |
empty_spec_for_recursive_call [Recursion] |
Generate an empty spec
assigns \nothing or
assigns \result \from \nothing , to be used to "approximate" the
results of a recursive call.
|
empty_store [Trace_partitioning.Make] | |
empty_tank [Trace_partitioning.Make] | |
empty_widening [Trace_partitioning.Make] | |
enabled_domains [Value_parameters] |
Returns the list (name, descr) of currently enabled domains.
|
enabled_domains [Eva.Value_parameters] |
Returns the list (name, descr) of currently enabled abstract domains.
|
enlarge [Numerors_interval] |
Enlarge the bounds of the interval by taking the previous float of the lower
bound and the following float of the upper bound
|
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] |
Introduces a list of variables in the state.
|
enter_scope [Transfer_stmt.S] | |
entry_formals [Traces_domain] | |
enumerate_valid_bits [Precise_locs] | |
env_annot [Eval_terms] | |
env_annot [Eva.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] | |
epsilon [Numerors_interval] |
Returns the interval
-epsilon ; +epsilon for the input precision
|
eq [Numerors_interval] | |
eq [Numerors_float] | |
eq [Numerors_utils.Rounding] | |
eq [Numerors_utils.Sign] | |
eq [Numerors_utils.Precisions] | |
eq_structure [Structure.Shape] | |
eq_type [Structure.Key] | |
equal [Map.S] | equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Hashtbl.HashedType] |
The equality predicate used to compare keys.
|
equal [Transfer_logic.LogicDomain] | |
equal [Equality.Set] | |
equal [Equality.Equality] | |
equal [Structure.Key] | |
equal [Eval.Flagged_Value] | |
equal [Alarmset] |
Are two maps equal?
|
equal_gui_after [Gui_types.S] | |
equal_gui_offsetmap_res [Gui_types] | |
equal_gui_res [Gui_types.S] | |
equal_loc [Precise_locs] | |
equal_loc [Abstract_location.S] | |
equal_offset [Precise_locs] | |
equal_offset [Abstract_location.S] | |
equality [Abstractions.Config] | |
eval_expr [Analysis.Results] | |
eval_float_constant [Cvalue_forward] | |
eval_function_exp [Analysis.Results] | |
eval_function_exp [Evaluation.S] |
Evaluation of the function argument of a
Call constructor
|
eval_lval_to_loc [Analysis.Results] | |
eval_predicate [Eval_terms] | |
eval_term [Eval_terms] | |
eval_tlval_as_location [Eval_terms] | |
eval_tlval_as_zone [Eval_terms] | |
eval_tlval_as_zone_under_over [Eval_terms] |
Return a pair of (under-approximating, over-approximating) zones.
|
eval_varinfo [Abstract_location.S] | |
evaluate [Evaluation.S] | evaluate ~valuation state expr evaluates the expression expr in the
state state , and returns the pair result, alarms , where: alarms are the set of alarms ensuring the soundness of the evaluation;, result is either `Bottom if the evaluation leads to an error,
or `Value (valuation, value), where value is the numeric value computed
for the expression expr , and valuation contains all the intermediate
results of the evaluation.
Optional arguments are: valuation is a cache of already computed expressions; empty by default., reduction allows the deactivation of the backward reduction performed
after the forward evaluation; true by default., subdivnb is the maximum number of subdivisions performed on non-linear
sub-expressions of expr . If a lvalue occurs several times in expr ,
its value can be split up to subdivnb times to gain more precision.
Set to the value of the option -eva-subdivide-non-linear by default.
|
evaluate [Subdivided_evaluation.Forward_Evaluation] | |
evaluate [Subdivided_evaluation.Make] | |
evaluate_assumes_of_behavior [Transfer_logic.S] | |
evaluate_predicate [Abstract_domain.S] |
Evaluates a
predicate to a logical status in the current state .
|
evaluate_predicate [Transfer_logic.LogicDomain] | |
exceed_rationing [Partition.Key] | |
exists [Map.S] | exists p m checks if at least one binding of the map
satisfies the predicate p .
|
exists [Equality.Set] | |
exists [Equality.Equality] | exists p s checks if at least one element of the equality
satisfies the predicate p .
|
exists [Alarmset] | |
exists [Parameter_sig.Set] |
Is there some element satisfying the given predicate?
|
exp [Numerors_value] | |
exp [Numerors_arithmetics.Arithmetic.Forward] | |
exp [Numerors_interval] | |
exp [Numerors_float] | |
exp_ev [Gui_eval.S] | |
expanded [Trace_partitioning.Make] | |
exponent [Numerors_float] |
Returns the exponent of its input
|
exponent [Numerors_utils.Precisions] |
Returns the number of bits of the exponent of the given precision.
|
expr_contains_volatile [Eval_typ] | |
extend_loc [Domain_lift.Conversion] | |
extend_val [Domain_lift.Conversion] | |
extend_val [Location_lift.Conversion] | |
extract_expr [Simpler_domains.Simple_Cvalue] | |
extract_expr [Abstract_domain.Queries] |
Query function for compound expressions:
eval oracle t exp returns the known value of exp by the state t .
|
extract_lval [Simpler_domains.Simple_Cvalue] | |
extract_lval [Abstract_domain.Queries] |
Query function for lvalues:
find oracle t lval typ loc returns the known value stored at
the location loc of the left value lval of type typ .
|
F | |
fill [Trace_partitioning.Make] |
Fill the states of the flow into the tank, modifying
into inplace.
|
filter [Map.S] | filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter [Abstract_domain.Reuse] | filter kf kind bases states reduces the state state to only keep
properties about bases — it is a projection on the set of bases .
|
filter [Partition] | |
filter [Equality.Equality] | filter p s returns the equality between all elements in s
that satisfy predicate p .
|
filter_map [Partition.MakeFlow] | |
finalize_call [Simpler_domains.Simple_Cvalue] | |
finalize_call [Simpler_domains.Minimal] | |
finalize_call [Abstract_domain.Transfer] | finalize_call stmt call ~pre ~post computes the state after a function
call, given the state pre before the call, and the state post at the
end of the called function.
|
find [Map.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 [Partition] | |
find [Equality.Set] | find elt set return the (single) equality involving elt
that belongs to set , or raise Not_found if no such equality exists.
|
find [Simple_memory.S] | find loc typ state returns the join of the abstract values stored
in the locations abstracted to by loc in state , assuming the
result has type typ .
|
find [Eval.Valuation] | |
find [Alarmset] |
Returns the status of a given alarm.
|
find [State_builder.Hashtbl] |
Return the current binding of the given key.
|
find [Parameter_sig.Map] |
Search a given key in the map.
|
find [Parameter_sig.Multiple_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_first [Map.S] | find_first f m , where f is a monotonically increasing function,
returns the binding of m with the lowest key k such that f k ,
or raises Not_found if no such key exists.
|
find_first_opt [Map.S] | find_first_opt f m , where f is a monotonically increasing function,
returns an option containing the binding of m with the lowest key k
such that f k , or None if no such key exists.
|
find_indeterminate [Cvalue.Model] | find_indeterminate ~conflate_bottom state loc returns the value
and flags associated to loc in state .
|
find_last [Map.S] | find_last f m , where f is a monotonically decreasing function,
returns the binding of m with the highest key k such that f k ,
or raises Not_found if no such key exists.
|
find_last_opt [Map.S] | find_last_opt f m , where f is a monotonically decreasing function,
returns an option containing the binding of m with the highest key k
such that f k , or None if no such key exists.
|
find_loc [Eval.Valuation] | |
find_opt [Map.S] | find_opt x m returns Some v if the current binding of x
in m is v , or None if no such binding exists.
|
find_option [Equality.Set] |
Same as
find , but return None in the last case.
|
find_subpart [Cvalue_domain] | |
find_under_approximation [Eval_op] | |
float_hints [Widen_type] |
Define floating hints for one or all variables (
None ),
for a certain stmt or for all statements (None ).
|
flow_actions [Partitioning_parameters.Make] | |
flow_size [Trace_partitioning.Make] | |
focus_on_callstacks [Gui_callstacks_filters] | |
focus_selection_tab [Gui_callstacks_manager] | |
focused_callstacks [Gui_callstacks_filters] | |
fold [Map.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 [Powerset.S] | |
fold [Equality.Set] | |
fold [Equality.Equality] | fold f s a computes (f xN ... (f x2 (f x1 a))...) ,
where x1 ... xN are the elements of s , in increasing order.
|
fold [Simple_memory.S] |
Fold on base value pairs.
|
fold [Eval.Valuation] | |
fold [State_builder.Hashtbl] | |
fold2_join_heterogeneous [Hptset.S] | |
fold_dynamic_bases [Builtins_malloc] | fold_dynamic_bases f init folds f to each dynamically allocated base,
with initial accumulator init .
|
fold_sorted [State_builder.Hashtbl] | |
for_all [Map.S] | for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
for_all [Equality.Set] | |
for_all [Equality.Equality] | for_all p s checks if all elements of the equality
satisfy the predicate p .
|
for_all [Alarmset] | |
force_compute [Analysis] |
Perform a full analysis, starting from the
main function.
|
forward_binop [Abstract_value.S] | forward_binop typ binop v1 v2 evaluates the value v1 binop v2 ,
resulting from the application of the binary operator binop to the
values v1 and v2 .
|
forward_binop_float [Cvalue_forward] | |
forward_binop_int [Cvalue_forward] | |
forward_cast [Cvalue_forward] | |
forward_cast [Abstract_value.S] |
Abstract evaluation of casts operators from
src_type to dst_type .
|
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_interaction [Numerors_arithmetics] |
Handling of forward interactions
|
forward_pointer [Abstract_location.S] |
Mem case in the AST: the host is a pointer.
|
forward_unop [Cvalue_forward] | |
forward_unop [Abstract_value.S] | forward_unop typ unop v evaluates the value unop v , resulting from the
application of the unary operator unop to the value v .
|
forward_variable [Abstract_location.S] |
Var case in the AST: the host is a variable.
|
frama_c_memchr_off_wrapper [Builtins_string] | |
frama_c_strchr_wrapper [Builtins_string] | |
frama_c_strlen_wrapper [Builtins_string] | |
frama_c_wcschr_wrapper [Builtins_string] | |
frama_c_wcslen_wrapper [Builtins_string] | |
frama_c_wmemchr_off_wrapper [Builtins_string] | |
free_automatic_bases [Builtins_malloc] |
Performs the equivalent of
free for each location that was allocated via
alloca() in the current function (as per Value_util.call_stack () ).
|
freeable [Builtins_malloc] |
Evaluates the ACSL predicate \freeable(value): holds if and only if the
value points to an allocated memory block that can be safely released using
the C function free.
|
from_callstack [Gui_callstacks_filters] | |
from_cvalue [Gui_types.Make] | |
from_shape [Hptset.S] |
Build a set from another
elt -indexed map or set.
|
G | |
gauges [Abstractions.Config] | |
ge [Numerors_arithmetics.Backward_Comparisons] | |
ge [Numerors_interval] | |
ge [Numerors_float] | |
get [Numerors_utils.Mode] | |
get [Numerors_utils.Precisions] |
Returns the number of bits of the significand of the given precision,
counting the implicit one.
|
get [Hcexprs.HCE] | |
get [Abstract.Interface] |
For a key of type
k key : if the values of type t contain a subpart of type k from a module
identified by the key, then get key returns an accessor for it., otherwise, get key returns None.
|
get [Structure.External] | |
get [State_builder.Ref] |
Get the referenced value.
|
getWidenHints [Widen] | getWidenHints kf s retrieves the set of widening hints related to
function kf and statement s .
|
get_LoadFunctionState [Value_parameters] | |
get_SaveFunctionState [Value_parameters] | |
get_all [Red_statuses] | |
get_bounds [Numerors_interval] |
Returns the bounds of its inputs
|
get_cvalue [Gui_types.Make] | |
get_cvalue [Abstract.Domain.External] |
Special accessors for the main cvalue domain.
|
get_cvalue_or_bottom [Abstract.Domain.External] | |
get_cvalue_or_top [Abstract.Domain.External] | |
get_exponents [Numerors_interval] |
Returns the exponent of the bounds ot its input
|
get_flow_annot [Eva_annotations] | |
get_function_name [Parameter_sig.String] |
returns the given argument only if it is a valid function name
(see
Parameter_customize.get_c_ified_functions for more information),
and abort otherwise.
|
get_global_state [Abstract_domain.Store] |
Allows accessing the states inferred by an Eva analysis after it has
been computed with the domain enabled.
|
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_max_absolute_error [Numerors_value] | |
get_max_exponent [Numerors_interval] |
Returns the biggest exponent of its input
|
get_max_relative_error [Numerors_value] | |
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 [Eva_annotations] | |
get_stmt_state [Analysis.Results] | |
get_stmt_state [Abstract_domain.Store] | |
get_stmt_state_by_callstack [Analysis.Results] | |
get_stmt_state_by_callstack [Abstract_domain.Store] | |
get_stmt_widen_hint_terms [Widen_hints_ext] | get_stmt_widen_hint_terms s returns the list of widen hints associated to
s .
|
get_subdivision [Value_util] | |
get_subdivision_annot [Eva_annotations] | |
get_unroll_annot [Eva_annotations] | |
get_v [Cvalue.V_Or_Uninitialized] | |
globals [Traces_domain] | |
gt [Numerors_arithmetics.Backward_Comparisons] | |
gt [Numerors_interval] | |
gt [Numerors_float] | |
gui_loc_equal [Gui_types] | |
gui_loc_loc [Gui_types] | |
gui_loc_logic_env [Gui_eval] |
Logic labels valid at the given location.
|
gui_selection_data_empty [Gui_eval] |
Default value.
|
gui_selection_equal [Gui_types] | |
H | |
has_requires [Eval_annots] | |
hash [Simpler_domains.Minimal] | |
hash [Hashtbl.HashedType] |
A hashing function on keys.
|
hash [Structure.Key] | |
hash_gui_callstack [Gui_types] | |
height_expr [Value_util] |
Computes the height of an expression, that is the maximum number of nested
operations in this expression.
|
height_lval [Value_util] |
Computes the height of an lvalue.
|
hints_from_keys [Widen_type] |
Widen hints for a given statement, suitable for function
Cvalue.Model.widen .
|
history_size [Partitioning_parameters.Make] | |
I | |
id [Hcexprs.HCE] | |
ik_attrs_range [Eval_typ] |
Range for an integer type with some attributes.
|
ik_range [Eval_typ] | |
imprecise_location [Precise_locs] | |
imprecise_location_bits [Precise_locs] | |
imprecise_offset [Precise_locs] | |
incr [Parameter_sig.Int] |
Increment the integer.
|
incr_loop_counter [Abstract_domain.S] | |
indirect_zone_of_lval [Value_util] |
Given a function computing the location of lvalues, computes the memory zone
on which the offset and the pointer expression (if any) of an lvalue depend.
|
initial [Partition.MakeFlow] | |
initial_state [Compute_functions.Make] | |
initial_state [Initialization.S] |
Compute the initial state for an analysis.
|
initial_state_with_formals [Initialization.S] |
Compute the initial state for an analysis (as in
Initialization.S.initial_state ),
but also bind the formal parameters of the function given as argument.
|
initial_tank [Trace_partitioning.Make] |
Build the initial tank for the entry point of a function.
|
initialize_local_variable [Initialization.S] |
Initializes a local variable in the current state.
|
initialize_var_using_type [Cvalue_init] | initialize_var_using_type varinfo state uses the type of varinfo
to create an initial value in state .
|
initialize_variable [Simpler_domains.Simple_Cvalue] | |
initialize_variable [Simpler_domains.Minimal] | |
initialize_variable [Abstract_domain.S] | initialize_variable lval loc ~initialized init_value state initializes
the value of the location loc of lvalue lval in state with:
– bits 0 if init_value = Zero;
– any bits if init_value = Top.
|
initialize_variable_using_type [Abstract_domain.S] |
Initializes a variable according to its type.
|
initialized [Cvalue.V_Or_Uninitialized] | initialized v returns the definitely initialized, non-escaping
representant of v .
|
inject_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] | |
inout [Abstractions.Config] | |
inter [Equality.Set] | |
inter [Equality.Equality] |
Intersection.
|
inter [Hcexprs.BaseToHCESet] | |
inter [Hcexprs.HCEToZone] | |
inter [Alarmset.Status] | |
inter [Alarmset] |
Pointwise intersection of property status: the most precise status is kept.
|
interp_annot [Transfer_logic.S] | |
interp_boolean [Cvalue.V] | |
interpret_truth [Evaluation.S] | |
intersects [Equality.Equality] | intersect s s' = true iff the two equalities both involve the same
element.
|
intersects [Hptset.S] | intersects s1 s2 returns true if and only if s1 and s2
have an element in common
|
is_a_zero [Numerors_float] |
Check if its input is a zero (positive or negative)
|
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_builtin_overridden [Builtins] |
Is a given function replaced by a builtin?
|
is_const_write_invalid [Value_util] |
Detect that the type is const, and that option
-global-const is set.
|
is_dynamic [Widen_hints_ext] | is_dynamic wh returns true iff widening hint wh has a "dynamic" prefix.
|
is_empty [Map.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_finite [Numerors_interval] |
Check if the bounds of its input are finite
|
is_global [Widen_hints_ext] | is_global wh returns true iff widening hint wh has a "global" prefix.
|
is_imprecise [Cvalue.V] | |
is_included [Simpler_domains.Simple_Cvalue] | |
is_included [Simpler_domains.Minimal] | |
is_included [Abstract_domain.Lattice] |
Inclusion test.
|
is_included [Numerors_arithmetics] | |
is_included [Numerors_interval] |
Lattice functions.
|
is_included [Hcexprs.HCEToZone] | |
is_included [Simple_memory.Value] | |
is_included [Simple_memory.Make_Memory] | |
is_included [Abstract_value.S] | |
is_indeterminate [Cvalue.V_Or_Uninitialized] | is_indeterminate v = false implies v only has definitely initialized
values and non-escaping addresses.
|
is_inf [Numerors_float] |
Check if its input is an infinite value
|
is_initialized [Cvalue.V_Or_Uninitialized] | is_initialized v = true implies v is definitely initialized.
|
is_isotropic [Cvalue.V] | |
is_lval [Hcexprs.HCE] | |
is_nan [Numerors_interval] |
Check if the interval contains only NaN values
|
is_nan [Numerors_float] |
Check if its input is a NaN
|
is_neg [Numerors_float] |
Check if its input is negative (is_neg NaN = false)
|
is_neg [Numerors_utils.Sign] | |
is_neg_inf [Numerors_interval] |
Check if the bounds of its input are negative infinites
|
is_neg_zero [Numerors_interval] |
Check if the bounds of its input are negative zeros
|
is_neg_zero [Numerors_float] |
Check if its input is a negative zero
|
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_pos [Numerors_float] |
Check if its input is positive (is_pos NaN = true)
|
is_pos [Numerors_utils.Sign] | |
is_pos_inf [Numerors_interval] |
Check if the bounds of its input are positive infinites
|
is_pos_zero [Numerors_interval] |
Check if the bounds of its input are positive zeros
|
is_pos_zero [Numerors_float] |
Check if its input is a positive zero
|
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_strictly_neg [Numerors_interval] |
Check if all the values of its input are negatives
|
is_strictly_neg [Numerors_float] |
Check if its input is strictly negative (non zero)
|
is_strictly_pos [Numerors_interval] |
Check if all the values of its input are positives
|
is_strictly_pos [Numerors_float] |
Check if its input is strictly positive (non zero)
|
is_top_loc [Precise_locs] | |
is_topint [Cvalue.V] | |
is_value_zero [Value_util] |
Return
true iff the argument has been created by Value_util.normalize_as_cond
|
is_zero [Numerors_interval] |
Check if the bounds of its input are both zero (without considering their
signs)
|
iter [Map.S] | iter f m applies f to all bindings in map m .
|
iter [Partition.MakeFlow] | |
iter [Partition] | |
iter [Powerset.S] | |
iter [Equality.Set] | |
iter [Equality.Equality] | iter f s applies f in turn to all elements of s .
|
iter [Alarmset] | |
iter [State_builder.Hashtbl] | |
iter_sorted [State_builder.Hashtbl] | |
J | |
join [Widen_type] | |
join [Simpler_domains.Simple_Cvalue] | |
join [Simpler_domains.Minimal] | |
join [Abstract_domain.Lattice] |
Semi-lattice structure.
|
join [Numerors_arithmetics] |
Lattice methods
|
join [Numerors_interval] | |
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 [Traces_domain.Graph] | |
join [Abstract_value.S] | |
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 [Abstract_location.Leaf] |
The key identifies the module and the type
t of abstract locations.
|
key [Abstract_domain.Leaf] |
The key identifies the domain and the type
t of its states.
|
key [Abstract_value.Leaf] |
The key identifies the module and the type
t of abstract values.
|
kf_of_gui_loc [Gui_types] | |
kf_strategy [Split_return] | |
L | |
le [Numerors_arithmetics.Backward_Comparisons] | |
le [Numerors_interval] | |
le [Numerors_float] | |
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] |
Removes a list of local and formal variables from the state.
|
legacy [Abstractions.Config] |
The configuration corresponding to the old "Value" analysis,
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 [Numerors_value] | |
log [Numerors_arithmetics.Arithmetic.Forward] | |
log [Numerors_interval] | |
log [Numerors_float] | |
log_category [Abstract_domain.S] |
Category for the messages about the domain.
|
logic_assign [Abstract_domain.S] | logic_assign None loc state removes from state all inferred properties
that depend on the memory location loc .
|
lt [Numerors_arithmetics.Backward_Comparisons] | |
lt [Numerors_interval] | |
lt [Numerors_float] | |
lval_as_offsm_ev [Gui_eval.S] | |
lval_contains_volatile [Eval_typ] |
Those two expressions indicate that one l-value contained inside
the arguments (and the l-value itself for
lval_contains_volatile ) has
volatile qualifier.
|
lval_ev [Gui_eval.S] | |
lval_to_exp [Value_util] |
This function is memoized to avoid creating too many expressions
|
lval_zone_ev [Gui_eval.S] | |
lvaluate [Evaluation.S] | lvaluate ~valuation ~for_writing state lval evaluates the left value
lval in the state state .
|
lvalues_only_left [Equality.Set] | |
M | |
machine_delta [Numerors_float] |
This function returns a float of precision ?prec containing the machine
delta of the mandatory precision parameter also divided by two for the same
reason as machine_epsilon.
|
machine_epsilon [Numerors_float] |
This function returns a float of precision ?prec containing the machine
epsilon divided by two for the mandatory precision parameter.
|
make [Cvalue.V_Or_Uninitialized] | |
make [Abstractions] |
Builds the abstractions according to a configuration.
|
make [Main_locations.PLoc] | |
make_data_all_callstacks [Gui_eval.S] | |
make_data_for_lvalue [Gui_callstacks_manager.Input] | |
make_env [Eval_terms] | |
make_escaping [Locals_scoping] | make_escaping ~exact ~escaping ~on_escaping ~within state changes all
references to the variables in escaping to "escaping address".
|
make_escaping_fundec [Locals_scoping] | make_escaping_fundec fdec clob l state changes all references to the
local or formal variables in l to "escaping".
|
make_finite [Numerors_interval] |
Replace the infinite bounds of its input into the maximum float of the
precision.
|
make_loc_contiguous [Eval_op] |
'Simplify' the location if it represents a contiguous zone: instead
of multiple offsets with a small size, change it into a single offset
with a size that covers the entire range.
|
make_panel [Gui_red] |
Add a tab to the main GUI (for red alarms), and return its widget.
|
make_precise_loc [Precise_locs] | |
make_type [Datatype.Hashtbl] | |
make_volatile [Cvalue_forward] | make_volatile ?typ v makes the value v more general (to account for
external modifications), whenever typ is None or when it has type
qualifier volatile .
|
map [Map.S] | map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map [Cvalue.V_Or_Uninitialized] | |
map [Partition] | |
map [Powerset.S] | |
map2 [Cvalue.V_Or_Uninitialized] |
initialized/escaping information is the join of the information
on each argument.
|
map_or_bottom [Powerset.S] | |
mapi [Map.S] |
Same as
Map.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mark_green_and_red [Eval_annots] | |
mark_invalid_initializers [Eval_annots] | |
mark_kf_as_called [Value_results] | |
mark_rte [Eval_annots] | |
mark_unreachable [Eval_annots] | |
max [Numerors_float] | |
max [Numerors_utils.Precisions] | |
max_binding [Map.S] |
Same as
Map.S.min_binding , but returns the largest binding
of the given map.
|
max_binding_opt [Map.S] |
Same as
Map.S.min_binding_opt , but returns the largest binding
of the given map.
|
maximal_neg_float [Numerors_float] |
Maximal negative float in the precision
|
maximal_pos_float [Numerors_float] |
Maximal positive float in the precision
|
mem [Map.S] | mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [Abstractions.Config] |
Returns true if the given flag is in the configuration.
|
mem [Equality.Set] | mem equality set = true iff ∃ eq ∈ set, equality ⊆ eq
|
mem [Equality.Equality] | mem x s tests whether x belongs to the equality s .
|
mem [Abstract.Interface] |
Tests whether a key belongs to the module.
|
mem [Structure.External] | |
mem [State_builder.Hashtbl] | |
mem [Parameter_sig.Map] | |
mem [Parameter_sig.Multiple_map] | |
mem [Parameter_sig.Set] |
Does the given element belong to the set?
|
memo [State_builder.Hashtbl] |
Memoization.
|
merge [Map.S] | merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge [Partitioning_parameters.Make] | |
merge [Partition] | |
merge [Powerset.S] | |
merge [Value_results] | |
merge [Hcexprs.HCEToZone] | |
merge [Hptset.S] | |
merge [Per_stmt_slevel] |
Slevel merge strategy for this function
|
merge [Eva.Value_results] | |
min [Numerors_float] | |
min [Numerors_utils.Precisions] | |
min_binding [Map.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.
|
min_binding_opt [Map.S] |
Return the smallest binding of the given map
(with respect to the
Ord.compare ordering), or None
if the map is empty.
|
mul [Cvalue.V] | |
mul [Numerors_arithmetics.Arithmetic.Backward] | |
mul [Numerors_arithmetics.Arithmetic.Forward] | |
mul [Numerors_interval] | |
mul [Numerors_float] | |
mul [Numerors_utils.Sign] | |
N | |
name [Simpler_domains.Minimal] | |
nan [Numerors_interval] |
Returns an interval containing only NaN values at the precision <prec>
|
narrow [Cvalue.V_Offsetmap] | |
narrow [Abstract_domain.Lattice] |
Over-approximation of the intersection of two abstract states (called meet
in the literature).
|
narrow [Numerors_arithmetics] | |
narrow [Numerors_interval] | |
narrow [Simple_memory.Value] | |
narrow [Abstract_value.S] | |
narrow_reinterpret [Cvalue.V_Offsetmap] |
See the corresponding functions in
Offsetmap_sig .
|
nearest_elt_ge [Datatype.Set] | |
nearest_elt_le [Datatype.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 [Numerors_arithmetics.Arithmetic.Backward] | |
neg [Numerors_arithmetics.Arithmetic.Forward] | |
neg [Numerors_interval] |
These functions perform mathematic unidimensionnal operations of intervals
using the precision <prec>
|
neg [Numerors_float] |
Negation
|
neg [Numerors_utils.Sign] | |
neg_inf [Numerors_interval] |
Returns the interval
-oo ; -oo at the precision <prec>
|
neg_inf [Numerors_float] |
Returns a t element representing a negative infinite value
|
neg_zero [Numerors_float] |
Returns a t element representing a negative zero value
|
new_counter [Mem_exec] |
Counter that must be used each time a new call is analyzed, in order
to refer to it later
|
new_monitor [Partition] |
Creates a new monitor that allows to split up to
split_limit states.
|
new_rationing [Partition] |
Creates a new rationing, that can be used successively on several flows.
|
next_float [Numerors_float] |
Returns the following floating point number of the same precision
|
next_loop_iteration [Trace_partitioning.Make] | |
no_memoization_enabled [Mark_noresults] | |
no_offset [Abstract_location.S] | |
none [Alarmset] |
no alarms: all potential assertions have a True status.
|
normalize_as_cond [Value_util] | normalize_as_cond e positive returns the expression corresponding to
e != 0 when positive is true, and e == 0 otherwise.
|
notify [Alarmset] |
Calls the functions registered in the
warn_mode according to the
set of alarms.
|
null_ev [Gui_eval.S] | |
num_hints [Widen_type] |
Define numeric hints for one or all variables (
None ),
for a certain stmt or for all statements (None ).
|
O | |
octagon [Apron_domain] | |
octagon [Abstractions.Config] | |
of_char [Cvalue.V] | |
of_exp [Hcexprs.HCE] | |
of_fkind [Numerors_utils.Precisions] |
Returns the precision associated to the Cil construction fkind, which
represents the C floating point type
|
of_float [Numerors_float] | |
of_floats [Numerors_interval] | |
of_floats_without_rounding [Numerors_interval] |
Works in the same way as of_floats but the bounds are rounded toward
nearest
|
of_int [Numerors_float] |
The functions of_<typ> ~rnd ~prec x return a float of precision <prec>
containing the value of x (of type <typ>) rounding to <rnd>.
|
of_int [Numerors_utils.Sign] | |
of_int64 [Cvalue.V] | |
of_ints [Numerors_value] | |
of_ints [Numerors_interval] |
The function of_<typ> ~prec (x, y) returns the interval
x' ; y' where
x' is a Numerors float containing the value of x (of type <typ>) rounded
toward -oo and y' is a Numerors float containing the value of y rounded
toward +oo.
|
of_list [Powerset.S] | |
of_lval [Hcexprs.HCE] | |
of_numerors_floats [Numerors_interval] |
Returns the interval corresponding to the given bounds.
|
of_partition [Partition.MakeFlow] | |
of_string [Numerors_float] | |
of_string [Parameter_sig.Multiple_value_datatype] | |
of_string [Split_strategy] | |
of_strings [Numerors_interval] | |
off [Parameter_sig.Bool] |
Set the boolean to
false .
|
offset_bottom [Precise_locs] | |
offset_top [Precise_locs] | |
offset_zero [Precise_locs] | |
offsetmap_contains_local [Locals_scoping] | |
offsetmap_matches_type [Eval_typ] | offsetmap_matches_type t o returns true if either: o contains a single scalar binding, of the expected scalar type t
(float or integer), o contains multiple bindings, pointers, etc., t is not a scalar type.
|
offsetmap_of_assignment [Cvalue_offsetmap] |
Computes the offsetmap for an assignment: in case of a copy, extracts the offsetmap from the state;, otherwise, translates the value assigned into an offsetmap.
|
offsetmap_of_loc [Eval_op] |
Returns the offsetmap at a precise_location from a state.
|
offsetmap_of_lval [Cvalue_offsetmap] | offsetmap_of_lval state lval loc extracts from state state the offsetmap
at location loc , corresponding to the lvalue lval .
|
offsetmap_of_v [Eval_op] |
Transformation a value into an offsetmap of size
sizeof(typ) bytes.
|
on [Parameter_sig.Bool] |
Set the boolean to
true .
|
one [Cvalue.CardinalEstimate] | |
one [Abstract_value.S] | |
output [Parameter_sig.With_output] |
To be used by the plugin to output the results of the option
in a controlled way.
|
P | |
pair [Equality.Equality] |
The equality between two elements.
|
parameters_correctness [Value_parameters] | |
parameters_tuning [Value_parameters] | |
partition [Map.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 .
|
polka_equality [Apron_domain] | |
polka_loose [Apron_domain] | |
polka_strict [Apron_domain] | |
pop_call_stack [Value_util] | |
pos_inf [Numerors_interval] |
Returns the interval
+oo ; +oo at the precision <prec>
|
pos_inf [Numerors_float] |
Returns a t element representing a positive infinite value
|
pos_zero [Numerors_interval] |
Returns the interval
+0 ; +0 at the precision <prec>
|
pos_zero [Numerors_float] |
Returns a t element representing a positive zero value
|
post_analysis [Abstract_domain.Internal] |
This function is called after the analysis.
|
postconditions_mention_result [Value_util] |
Does the post-conditions of this specification mention
\result ?
|
pow [Numerors_float] | |
pow_int [Numerors_float] | |
pp_callstack [Value_util] |
Prints the current callstack.
|
pp_hvars [Widen_hints_ext] | |
prec [Numerors_arithmetics] |
Return the precision of the <approx> field
|
prec [Numerors_interval] |
Returns the precisions of the bounds of its input
|
prec [Numerors_float] |
Returns the precision of its input
|
precompute_widen_hints [Widen] |
Parses all widening hints defined via the widen_hint syntax extension.
|
predicate_deps [Eval_terms] | |
predicate_deps [Eva.Eval_terms] | predicate_deps env p computes the logic dependencies needed to evaluate
p in the given evaluation environment env .
|
predicate_ev [Gui_eval.S] | |
predicate_with_red [Gui_eval.S] | |
prepare_builtins [Builtins] |
Prepares the builtins to be used for an analysis.
|
pretty [Widen_type] |
Pretty-prints a set of hints (for debug purposes only).
|
pretty [Cvalue.CardinalEstimate] | |
pretty [Simpler_domains.Minimal] | |
pretty [Numerors_arithmetics] |
Pretty printer
|
pretty [Numerors_interval] | |
pretty [Numerors_float] | |
pretty [Numerors_utils.Rounding] | |
pretty [Numerors_utils.Sign] | |
pretty [Numerors_utils.Precisions] | |
pretty [Partitioning_index.Make] | |
pretty [Partition.Key] | |
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 [Numerors_value] | |
pretty_debug [Equality_domain.Make] | |
pretty_debug [Hptset.S] | |
pretty_debug [Hcexprs.HCE] | |
pretty_debug [Simple_memory.Value] |
Can be equal to
pretty
|
pretty_debug [Sign_value] | |
pretty_flow [Trace_partitioning.Make] | |
pretty_gui_after [Gui_types.S] | |
pretty_gui_offsetmap_res [Gui_types] | |
pretty_gui_res [Gui_types.S] | |
pretty_gui_selection [Gui_types] | |
pretty_hash [Value_types.Callstack] |
Print a hash of the callstack when '-kernel-msg-key callstack'
is enabled (prints nothing otherwise).
|
pretty_loc [Precise_locs] | |
pretty_loc [Abstract_location.S] | |
pretty_loc_bits [Precise_locs] | |
pretty_logic_evaluation_error [Eval_terms] | |
pretty_long_log10 [Cvalue.CardinalEstimate] | |
pretty_offset [Precise_locs] | |
pretty_offset [Abstract_location.S] | |
pretty_offsetmap [Eval_op] | |
pretty_predicate_status [Eval_terms] | |
pretty_short [Value_types.Callstack] |
Print a call stack without displaying call sites.
|
pretty_state_as_c_assert [Builtins_print_c] | |
pretty_state_as_c_assignments [Builtins_print_c] | |
pretty_status [Alarmset] | |
pretty_stitched_offsetmap [Eval_op] | |
pretty_store [Trace_partitioning.Make] | |
pretty_strategies [Split_return] | |
pretty_typ [Cvalue.V] | |
pretty_typ [Abstract_value.S] |
Pretty the abstract value assuming it has the type given as argument.
|
prev_float [Numerors_float] |
Returns the previous floating point number of the same precision
|
print [Structure.Key] | |
print_summary [Value_results] |
Prints a summary of the analysis.
|
printer [Abstractions.Config] | |
process_inactive_behaviors [Transfer_logic] | |
product_category [Domain_product] | |
project [Equality_domain.Make] | |
project_float [Cvalue.V] |
Raises
Not_based_on_null if the value may be a pointer.
|
project_ival [Cvalue.V] |
Raises
Not_based_on_null if the value may be a pointer.
|
project_ival_bottom [Cvalue.V] | |
push_call_stack [Value_util] | |
R | |
range_inclusion [Eval_typ] |
Checks inclusion of two integer ranges.
|
range_lower_bound [Eval_typ] | |
range_upper_bound [Eval_typ] | |
rbetween [Numerors_value] |
Returns the abstraction corresponding to the join of the approximation of
the inputs.
|
reduce [Numerors_value] |
Reduction of an error value according to a floating-point interval.
|
reduce [Abstractions.Value] | |
reduce [Evaluation.Value] |
Inter-reduction of values.
|
reduce [Evaluation.S] | reduce ~valuation state expr positive evaluates the expression expr
in the state state , and then reduces the valuation such that
the expression expr evaluates to a zero or a non-zero value, according
to positive .
|
reduce_by_danglingness [Cvalue.V_Or_Uninitialized] | reduce_by_danglingness dangling v reduces v so that its result r
verifies \dangling(r) if dangling is true , and
!\dangling(r) otherwise.
|
reduce_by_enumeration [Subdivided_evaluation.Make] | |
reduce_by_initialized_defined [Eval_op] | |
reduce_by_initializedness [Cvalue.V_Or_Uninitialized] | reduce_by_initializedness initialized v reduces v so that its result
r verifies \initialized(r) if initialized is true , and
!\initialized(r) otherwise.
|
reduce_by_predicate [Abstract_domain.S] | reduce_by_predicate env state pred b reduces the current state by
assuming that the predicate pred evaluates to b .
|
reduce_by_predicate [Transfer_logic.LogicDomain] | |
reduce_by_predicate [Eval_terms] | |
reduce_by_valid_loc [Eval_op] | |
reduce_further [Abstract_domain.Queries] |
Given a reduction
expr = value , provides more reductions that may
be performed.
|
reduce_indeterminate_binding [Cvalue.Model] |
Same behavior as
reduce_previous_binding , but takes a value
with 'undefined' and 'escaping addresses' flags.
|
reduce_previous_binding [Cvalue.Model] | reduce_previous_binding state loc v reduces the value associated to loc
in state; use with caution, as the inclusion between the new and the
old value is not checked.
|
register [Abstractions] |
Registers an abstract domain.
|
register_builtin [Builtins] | register_builtin name ?replace ?typ f registers the ocaml function f
as a builtin to be used instead of the C function of name name .
|
register_domain [Value_parameters] |
Registers available domain names for the -eva-domains option.
|
register_global_state [Abstract_domain.Store] | |
register_hook [Analysis] |
Registers a hook that will be called each time the
current analyzer
is changed.
|
register_hook [Abstractions] |
Register a hook modifying the three abstractions after their building by
the engine, before the start of each analysis.
|
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] | |
register_value_reduction [Abstractions] |
Register a reduction function for a value reduced product.
|
reinterpret [Cvalue_forward] | |
reinterpret_as_float [Cvalue.V] | |
reinterpret_as_int [Cvalue.V] | |
relate [Abstract_domain.Reuse] | relate kf bases state returns the set of bases bases in relation with
bases in state — i.e.
|
remember_bases_with_locals [Locals_scoping] |
Add the given set of bases to an existing clobbered set
|
remember_if_locals_in_value [Locals_scoping] | remember_locals_in_value clob loc v adds all bases pointed to by loc
to clob if v contains the address of a local or formal
|
remove [Map.S] | remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove [Equality.Set] | remove lval set remove any expression e such that lval belongs to
syntactic_lval e from the set of equalities set .
|
remove [Equality.Equality] | remove x s returns the equality between all elements of s , except x .
|
remove [Simple_memory.S] | remove loc state drops all information on the locations pointed to
by loc from state .
|
remove [Eval.Valuation] | |
remove [State_builder.Hashtbl] | |
remove_indeterminateness [Cvalue.V_Or_Uninitialized] |
Remove 'uninitialized' and 'escaping addresses' flags from the argument
|
remove_loc [Eval.Valuation] | |
remove_variables [Cvalue.Model] |
For variables that are coming from the AST, this is equivalent to
uninitializing them.
|
remove_variables [Simple_memory.S] | remove_variables list state drops all information about the variables
in list from state.
|
reorder [Powerset.S] | |
replace [Partition] | |
replace [Hcexprs.HCE] |
Replaces all occurrences of the lvalue
late by the expression heir .
|
replace [State_builder.Hashtbl] |
Add a new binding.
|
replace_val [Location_lift.Conversion] | |
report [Red_statuses] | |
reset [Gui_callstacks_manager] | |
reset [Value_perf] |
Reset the internal state of the module; to call at the very
beginning of the analysis.
|
reset_store [Trace_partitioning.Make] | |
reset_tank [Trace_partitioning.Make] | |
reset_widening [Trace_partitioning.Make] | |
reset_widening_counter [Trace_partitioning.Make] |
Resets (or just delays) the widening counter.
|
resolve_functions [Abstract_value.S] | resolve_functions v returns the list of functions that may be pointed to
by the abstract value v (representing a function pointer).
|
restrict_loc [Domain_lift.Conversion] | |
restrict_val [Domain_lift.Conversion] | |
restrict_val [Location_lift.Conversion] | |
results_kf_computed [Gui_eval] |
Catch the fact that we are in a function for which
-no-results or one
of its variants is set.
|
returned_value [Library_functions] | |
reuse [Abstract_domain.Reuse] | reuse kf bases current_input previous_output merges the initial state
current_input with a final state previous_output from a previous
analysis of kf started with an equivalent initial state.
|
reuse_previous_call [Mem_exec.Make] | reuse_previous_call kf init_state args searches amongst the previous
analyzes of kf one that matches the initial state init_state and the
values of arguments args .
|
rewrap_integer [Cvalue_forward] | |
rewrap_integer [Abstract_value.S] | rewrap_integer irange t wraps around the abstract value t to fit the
integer range irange , assuming 2's complement.
|
S | |
safe_argument [Backward_formals] | safe_argument e returns true if e (which is supposed to be
an actual parameter) is guaranteed to evaluate in the same way before and
after the call.
|
save_globals_state [State_import] |
Saves the final state of globals variables after the return statement of
the function defined via
Value_parameters.SaveFunctionState .
|
self [Hcexprs.HCE] | |
set [Abstract.Interface] |
For a key of type
k key : if the values of type t contain a subpart of type k from a module
identified by the key, then set key v t returns the value t in which
this subpart has been replaced by v ., otherwise, set key _ is the identity function.
|
set [Structure.External] | |
set [Alarmset] | set alarm status t binds the alarm to the status in the map t .
|
set [State_builder.Ref] |
Change the referenced value.
|
set_absolute_to_top [Numerors_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_relative_to_top [Numerors_value] | |
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 [Numerors_float] |
Returns the sign of its input.
|
sign [Abstractions.Config] | |
signal_abort [Iterator] |
Mark the analysis as aborted.
|
significand [Numerors_float] |
Returns the significand of its input.
|
sin [Numerors_float] | |
singleton [Map.S] | singleton x y returns the one-element map that contains a binding y
for x .
|
singleton [Powerset.S] | |
singleton [Alarmset] | singleton ?status alarm creates the map set alarm status none :
alarm has a by default an unkown status (which can be overridden through
status ), and all others have a True status.
|
singleton' [Powerset.S] | |
size [Abstract_location.S] | |
size [Partition.MakeFlow] | |
size [Partition] | |
sizeof_lval_typ [Eval_typ] |
Size of the type of a lval, taking into account that the lval might have
been a bitfield.
|
skip_specifications [Value_util] |
Should we skip the specifications of this function, according to
-eva-skip-stdlib-specs
|
slevel [Partitioning_parameters.Make] | |
smashed [Trace_partitioning.Make] | |
split [Map.S] | split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
split_return [Trace_partitioning.Make] | |
sqrt [Numerors_value] | |
sqrt [Numerors_arithmetics.Arithmetic.Forward] | |
sqrt [Numerors_interval] | |
sqrt [Numerors_float] | |
square [Numerors_interval] | |
square [Numerors_float] | |
start [Traces_domain] | |
start_call [Simpler_domains.Simple_Cvalue] | |
start_call [Simpler_domains.Minimal] | |
start_call [Abstract_domain.Transfer] | start_call stmt call valuation state returns an initial state
for the analysis of a called function.
|
start_doing [Value_perf] | |
stop_doing [Value_perf] |
Call
start_doing when finishing analyzing a function.
|
storage [Domain_builder.InputDomain] | |
storage [Domain_store.InputDomain] | |
store_computed_call [Mem_exec.Make] | store_computed_call kf init_state args call_results memoizes the fact
that calling kf with initial state init_state and arguments args
resulted in the results call_results .
|
store_size [Trace_partitioning.Make] | |
structural_descr [Locals_scoping] | |
structure [Abstract.Domain.Internal] | |
structure [Abstract.Location.Internal] | |
structure [Abstract.Value.Internal] | |
structure [Structure.Internal] | |
sub [Numerors_arithmetics.Arithmetic.Backward] | |
sub [Numerors_arithmetics.Arithmetic.Forward] | |
sub [Numerors_interval] | |
sub [Numerors_float] | |
sub_untyped_pointwise [Cvalue.V] |
See
Locations.sub_pointwise .
|
subset [Equality.Set] | |
subset [Equality.Equality] | |
symbolic_locations [Abstractions.Config] | |
syntactic_lvalues [Hcexprs] | syntactic_lvalues e returns the set of lvalues that appear in the
expression e .
|
T | |
tag [Structure.Key] | |
tan [Numerors_float] | |
tank_size [Trace_partitioning.Make] | |
term_ev [Gui_eval.S] | |
tlval_ev [Gui_eval.S] | |
tlval_zone_ev [Gui_eval.S] | |
to_domain_valuation [Evaluation.S] |
Evaluation functions store the results of an evaluation into
Valuation.t
maps.
|
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 [Parameter_sig.Multiple_value_datatype] | |
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 [Numerors_interval] |
Returns the interval
-oo ; +oo with NaNs at the precision <prec>
|
top [Transfer_logic.LogicDomain] | |
top [Locals_scoping] | |
top [Simple_memory.Value] | |
top [Simple_memory.Make_Memory] |
The top abstraction, which maps all variables to
V.top .
|
top [Abstract_value.S] | |
top_int [Abstract_value.S] | |
traces [Abstractions.Config] | |
track_variable [Simple_memory.Value] |
This function must return
true if the given variable should be
tracked by the domain.
|
transfer [Trace_partitioning.Make] |
Apply a transfer function to all the states of a propagation.
|
transfer_keys [Partition.MakeFlow] | |
transfer_states [Partition.MakeFlow] | |
treat_statement_assigns [Transfer_specification.Make] | |
U | |
uncheck_add [Powerset.S] | |
uninitialize_blocks_locals [Cvalue.Model] | |
uninitialized [Cvalue.V_Or_Uninitialized] |
Returns the canonical representant of a definitely uninitialized value.
|
union [Map.S] | union f m1 m2 computes a map whose keys is the union of keys
of m1 and of m2 .
|
union [Partition.MakeFlow] | |
union [Equality.Set] | |
union [Equality.Equality] |
Union.
|
union [Hcexprs.BaseToHCESet] | |
union [Hcexprs.HCEToZone] | |
union [Alarmset] |
Pointwise union of property status: the least precise status is kept.
|
unite [Equality.Set] | unite (a, a_set) (b, b_set) map unites a and b in map .
|
universal_splits [Partitioning_parameters.Make] | |
unroll [Partitioning_parameters.Make] | |
unspecify_escaping_locals [Cvalue.V_Or_Uninitialized] | |
update [Abstract_domain.Transfer] | update valuation t updates the state t with the values of expressions
and the locations of lvalues available in the valuation record.
|
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] | |
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_imprecise_lval_read [Warn] | |
warn_locals_escape [Warn] | |
warn_none_mode [CilE] |
Do not emit any message.
|
warn_right_exp_imprecision [Warn] | |
warn_right_imprecision [Cvalue_offsetmap] | warn_right_imprecision lval loc offsm is used for the assignment of the
lvalue lval pointing to the location loc ; it warns if the offsetmap
offsm contains a garbled mix.
|
warn_unsupported_spec [Library_functions] |
Warns on functions from the frama-c libc with unsupported specification.
|
warning_once_current [Value_util] | |
widen [Simpler_domains.Simple_Cvalue] | |
widen [Simpler_domains.Minimal] | |
widen [Abstract_domain.Lattice] | widen h t1 t2 is an over-approximation of join t1 t2 .
|
widen [Trace_partitioning.Make] |
Widen a flow.
|
widen [Simple_memory.Value] | |
widen [Simple_memory.Make_Memory] | |
widening_delay [Partitioning_parameters.Make] | |
widening_period [Partitioning_parameters.Make] | |
wkey_alarm [Value_parameters] |
Warning category used when emitting an alarm in "warning" mode.
|
wkey_builtins_missing_spec [Value_parameters] |
Warning category used for "cannot use builtin due to missing spec"
|
wkey_builtins_override [Value_parameters] |
Warning category used for "definition overridden by builtin"
|
wkey_experimental [Value_parameters] |
Warning category for experimental domains or features.
|
wkey_garbled_mix [Value_parameters] |
Warning category used to print garbled mix
|
wkey_invalid_assigns [Value_parameters] |
Warning category for 'completely invalid' assigns clause
|
wkey_libc_unsupported_spec [Value_parameters] |
Warning category used for calls to libc functions whose specification
is currently unsupported.
|
wkey_locals_escaping [Value_parameters] |
Warning category used for the warning "locals escaping scope".
|
wkey_loop_unroll [Value_parameters] |
Warning category used for "loop not completely unrolled"
|
wkey_missing_loop_unroll [Value_parameters] |
Warning category used to identify loops without unroll annotations
|
wkey_missing_loop_unroll_for [Value_parameters] |
Warning category used to identify for loops without unroll annotations
|
wkey_signed_overflow [Value_parameters] |
Warning category for signed overflows
|
wrap_double [Eval_op] | |
wrap_float [Eval_op] | |
wrap_int [Eval_op] | |
wrap_long_long [Eval_op] | |
wrap_ptr [Eval_op] | |
wrap_size_t [Eval_op] |
Specialization of the function above for standard types
|
written_formals [Backward_formals] | written_formals kf is an over-approximation of the formals of kf
which may be internally overwritten by kf during its call.
|
Z | |
zero [Numerors_arithmetics] |
Return a value with all fields to zero.
|
zero [Numerors_interval] |
Returns the interval
-0 ; +0 at the precision <prec>
|
zero [Partition.Key] |
Initial key: no partitioning.
|
zero [Abstract_value.S] | |
zone_of_expr [Value_util] |
Given a function computing the location of lvalues, computes the memory zone
on which the value of an expression depends.
|