Index of values


A
a_ignore [CilE]
access_value_of_expr [Register]
access_value_of_location [Register]
access_value_of_lval [Register]
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 [Hashtbl.S]
add [State_builder.Hashtbl]
Add a new binding.
add [State_set]
Adding elements
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_code_transformation_after_cleanup [File]
Same as above, but the hook is applied after clean up.
add_code_transformation_before_cleanup [File]
add_code_transformation_before_cleanup name hook adds an hook in the corresponding category that will be called during the normalization of a linked file, before clean up and removal of temps and unused declarations.
add_initial_binding [Cvalue.Model]
add_kf_caller [Value_results]
add_new_base [Cvalue.Model]
add_num_hints [Widen_type]
Add numeric hints for one or all variables (None), for a a certain stmt or for all statements (None).
add_retres_to_state [Library_functions]
add_statement [State_set]
Update the trace of all the states in the stateset.
add_untyped [Cvalue.V]
add_untyped_under [Cvalue.V]
add_var_hints [Widen_type]
Add a set of bases to widen in priority for a given statement.
all_values [Cvalue.V]
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 [Warn]
assigns_inputs_to_zone [Register]
assigns_outputs_aux [Register]
assigns_outputs_to_locations [Register]
assigns_outputs_to_zone [Register]

B
behavior_from_name [Eval_annots.ActiveBehaviors]
behavior_inactive [Eval_annots]
bind_block_locals [Value_util]
Bind all locals of the the block to their default value (namely UNINITIALIZED)
bindings [FCMap.S]
Return the list of all bindings of the given map.
bitwise_and [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 [Mem_lvalue.LatticeDirty]
bottom_location_bits [Precise_locs]

C
c_labels [Eval_annots]
c_rem [Cvalue.V]
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_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_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_lval_if_bitfield [Eval_typ]
if needed, cast the given abstract value to the given size.
check_arg_size [Function_args]
check_fct_assigns [Eval_annots]
check_fct_postconditions [Eval_annots]
check_fct_preconditions [Eval_annots]
Check the precondition of kf.
check_no_recursive_call [Warn]
Check that kf is not already present in the call stack
check_non_overlapping [Eval_stmt]
check_unspecified_sequence [Eval_stmt]
choose [FCMap.S]
Return one binding of the given map, or raise Not_found if the map is empty.
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 [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_call_stack [Value_util]
Functions dealing with call stacks.
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 [Mem_lvalue.GraphDeps.V]
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]
compute [Eval_slevel.Computer]
compute [Mem_lvalue]
compute_actual [Function_args]
compute_call_ref [Eval_stmt]
compute_non_linear [Eval_non_linear]
contains_c_at [Eval_annots]
contains_non_zero [Cvalue.V]
contains_zero [Cvalue.V]
conv_status [Eval_annots]
copy [Hashtbl.S]
copy [Datatype.S]
Deep copy: no possible sharing between x and copy x.
copy_offsetmap [Eval_op]
Tempory.
copy_ppt [Mem_lvalue]
create [Hashtbl.S]
create [Eval_annots.ActiveBehaviors]
create_all_values [Cvalue.V]
create_from_spec [Eval_annots.ActiveBehaviors]
create_initialized_var [Cvalue.Default_offsetmap]
create_new_var [Value_util]
Create and register a new variable inside Frama-C.
create_project_from_visitor [File]
Return a new project with a new cil file representation by visiting the file of the current project.
create_rebuilt_project_from_visitor [File]
Like File.create_project_from_visitor, but the new generated cil file is generated into a temp .i or .c file according to preprocess, then re-built by Frama-C in the returned project.
current_kf [Value_util]
The current function is the one on top of the call stack.
current_stmt [Valarms]
curstate [Value_messages]

D
debug [Mem_lvalue]
debug_result [Value_util]
default [Widen_type]
A default set of hints
default_alarm_report [Value_messages]
default_offsetmap [Cvalue.Default_offsetmap]
dirties [Mem_lvalue.Compute]
Does the evaluation of stmt modifies the eventual value of X.lv?
display [Register]
display [Value_perf]
Display a complete summary of performance informations.
display_results [Register]
div [Cvalue.V]
dkey_card [Register]
do_assign [Eval_stmt]
do_promotion [Eval_op]
do_warn [Valarms]
dump_args [Builtins]
dump_state [Builtins]
Builtins with multiple names; the lookup is done using a distinctive prefix
dump_state_file [Builtins]
dup_spec_status [Mem_lvalue]
Assumes the current project is old_prj

E
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 [State_imp]
Creation
empty [State_set]
Creation
end_stmt [Valarms]
enumerate_valid_bits [Precise_locs]
env_annot [Eval_terms]
env_assigns [Eval_terms]
env_current_state [Eval_terms]
env_only_here [Eval_terms]
Used by auxiliary plugins, that do not supply the other states
env_post_f [Eval_terms]
env_pre_f [Eval_terms]
epilogue [Separate]
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 [Mem_lvalue.GraphDeps.V]
equal_gui_after [Gui_types]
equal_gui_offsetmap_res [Gui_types]
equal_gui_res [Gui_types]
eval_and_reduce_pre_post [Eval_annots]
eval_binop_float [Eval_op]
eval_binop_int [Eval_op]
eval_by_callstack [Eval_annots]
eval_comp [Cvalue.V]
Can only be called on the 6 comparison operators
eval_error_reason [Register]
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 [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_lval [Eval_exprs]
eval_predicate [Register]
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]
exists [FCMap.S]
exists p m checks if at least one binding of the map satisfy the predicate p.
exists [State_imp]
exists [State_set]
exists [Parameter_sig.Set]
Is there some element satisfying the given predicate?
exp_ev [Gui_eval]
expr_to_kernel_function [Register]
expr_to_kernel_function_state [Register]
externalize [Eval_stmt]

F
filter [FCMap.S]
filter p m returns the map with all the bindings in m that satisfy predicate p.
filter_if [Separate]
filter_le_ge_lt_gt_float [Cvalue.V]
filter_le_ge_lt_gt_int [Cvalue.V]
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 [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_deps_term_no_transitivity_state [Register]
find_lv [Eval_exprs]
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.
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 [Hashtbl.S]
fold [State_imp]
Iterators
fold [State_builder.Hashtbl]
fold [State_set]
Iterators
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.
from_callstack [Gui_callstacks_filters]
from_filename [File]
Build a file from its name.

G
get [Builtins_nonfree_malloc.Dynamic_Alloc_Bases]
get [State_builder.Ref]
Get the referenced value.
getWidenHints [Widen]
get_all [File]
Return the list of toplevel files.
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_name [File]
File name.
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_preprocessor_command [File]
Return the preprocessor command to use.
get_range [Parameter_sig.Int]
What is the possible range of values for this parameter.
get_rounding_mode [Value_util]
get_slevel [Value_util]
get_suffixes [File]
get_v [Cvalue.V_Or_Uninitialized]
good_emitter [Mem_lvalue]
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 [Mem_lvalue.GraphDeps.V]
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
imprecise_location [Precise_locs]
imprecise_location_bits [Precise_locs]
imprecise_offset [Precise_locs]
incr [Stop_at_nth]
incr [Parameter_sig.Int]
Increment the integer.
init [Mem_lvalue.Compute]
init_from_c_files [File]
Initialize the cil file representation of the current project.
init_from_cmdline [File]
Initialize the cil file representation with the file given on the command line.
init_project_from_cil_file [File]
Initialize the cil file representation with the given file for the given project from the current one.
init_project_from_visitor [File]
init_project_from_visitor prj vis initialize the cil file representation of prj.
initial_state_lib_entry [Initial_state]
initial_state_not_lib_entry [Initial_state]
initialize_var_using_type [Initial_state]
initialize_var_using_type varinfo state uses the type of varinfo to create an initial value in state.
initialized [Cvalue.V_Or_Uninitialized]
initialized v returns the definitely initialized, non-escaping representant of v.
inject_int [Cvalue.V]
inject_location_bits [Precise_locs]
instrument [Mem_lvalue]
interp_annot [Eval_annots]
interp_boolean [Cvalue.V]
interp_call [Eval_stmt]
is_active [Eval_annots.ActiveBehaviors]
is_active_aux [Eval_annots.ActiveBehaviors]
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 [State_imp]
Information
is_empty [State_set]
Information
is_imprecise [Cvalue.V]
is_included [Mem_lvalue.LatticeDirty]
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_topint [Cvalue.V]
iter [FCMap.S]
iter f m applies f to all bindings in map m.
iter [Hashtbl.S]
iter [State_imp]
iter [State_builder.Hashtbl]
iter [State_set]
iter_sorted [State_builder.Hashtbl]
iter_succ [Mem_lvalue.GraphDeps]
iter_vertex [Mem_lvalue.GraphDeps]

J
join [Mem_lvalue.LatticeDirty]
join [State_imp]
Export
join [State_set]
Export
join_and_is_included [Mem_lvalue.LatticeDirty]
join_final_states [Split_return]
Join the given state_set.
join_gui_offsetmap_res [Gui_types]
join_list_predicate_status [Eval_terms]
join_predicate_status [Eval_terms]

K
kf_of_gui_loc [Gui_types]
ki_of_callstack [Value_messages]

L
length [Hashtbl.S]
length [State_imp]
length [State_builder.Hashtbl]
Length of the table.
length [State_set]
loc_bottom [Precise_locs]
loc_size [Precise_locs]
local [Per_stmt_slevel]
Slevel to use in this function
lv_has_exact_loc [Mem_lvalue]
lv_imprecise_loc [Mem_lvalue]
lv_is_precise [Mem_lvalue]
lv_name [Mem_lvalue]
lval_ev [Gui_eval]
lval_to_loc [Eval_exprs]
lval_to_loc_deps_state [Eval_exprs]
lval_to_loc_kinstr [Register]
lval_to_loc_state [Eval_exprs]
lval_to_loc_with_deps [Register]
lval_to_loc_with_deps_state [Register]
lval_to_offsetmap [Register]
lval_to_offsetmap_aux [Register]
lval_to_offsetmap_state [Register]
lval_to_precise_loc [Eval_exprs]
lval_to_precise_loc_deps_state [Eval_exprs]
lval_to_precise_loc_state [Eval_exprs]
lval_to_precise_loc_with_deps_state [Register]
lval_to_precise_loc_with_deps_state_alarm [Register]
lval_to_zone [Register]
lval_to_zone_state [Register]
lval_to_zone_with_deps_state [Register]
lval_zone_ev [Gui_eval]

M
machdep_macro [File]
machdep_macro machine returns the name of a macro __FC_MACHDEP_XXX so that the preprocessor can select std lib definition consistent with the selected machdep.
main [Register]
main_initial_state_with_formals [Function_args]
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_type [Datatype.Hashtbl]
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
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 [State_set]
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 [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 [Per_stmt_slevel]
Slevel merge strategy for this function
merge [State_set]
Merge the two sets together.
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]
For all formals of kf whose address is taken, merge their values in prev_state and new_state, and update new_state.
merge_results [Eval_slevel.Computer]
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.
mul [Cvalue.V]
must_recompute_cfg [File]
must_recompute_cfg f must be called by code transformation hooks when they modify statements in function f.

N
need_cast [Eval_typ]
new_alarm [Value_messages]
new_counter [Mem_exec]
Counter that must be used each time a new call is analyzed, in order to refer to it later
new_file_type [File]
new_file_type suffix func funcname registers a new type of files (with corresponding suffix) as recognized by Frama-C through func.
new_machdep [File]
new_machdep name module registers a new machdep name as recognized by Frama-C through The usual uses is Cmdline.run_after_loading_stage (fun () -> File.new_machdep "my_machdep" my_machdep_implem)
new_status [Value_messages]
no_memoization_enabled [Mark_noresults]
notify_status [Eval_annots]
null_ev [Gui_eval]

O
of_char [Cvalue.V]
of_int64 [Cvalue.V]
of_list [State_set]
of_list_forget_history [State_set]
of_string [Split_strategy]
off [Parameter_sig.Bool]
Set the boolean to false.
offset_bottom [Precise_locs]
offset_top [Precise_locs]
offset_zero [Precise_locs]
offsetmap_contains_imprecision [Warn]
Returns the first eventual imprecise part contained in an offsetmap
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.
on [Parameter_sig.Bool]
Set the boolean to true.
one [Cvalue.CardinalEstimate]
output [Parameter_sig.With_output]
To be used by the plugin to output the results of the option in a controlled way.
overridden_by_builtin [Builtins]
Should the given function be replaced by a call to a builtin

P
parameters_correctness [Value_parameters]
parameters_tuning [Value_parameters]
partition [FCMap.S]
partition p m returns a pair of maps (m1, m2), where m1 contains all the bindings of s that satisfy the predicate p, and m2 is the map with all the bindings of s that do not satisfy p.
partition_terminating_instr [Value_results]
Returns the list of terminating callstacks and the list of non-terminating callstacks.
paste_offsetmap [Eval_op]
Temporary.
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_pre_post_kind [Eval_annots]
pre_register [File]
Register some file as source file before command-line files
predicate_deps [Eval_terms]
predicate_ev [Gui_eval]
prepare_from_c_files [File]
Initialize the AST of the current project according to the current filename list.
pretty [Cvalue.CardinalEstimate]
pretty [Mem_lvalue.LatticeDirty]
pretty [State_imp]
pretty [State_set]
pretty_actuals [Value_util]
pretty_ast [File]
Print the project CIL file on the given Formatter.
pretty_call_stack [Value_util]
pretty_call_stack_short [Value_util]
Print a call stack.
pretty_callstack [Gui_types]
pretty_callstack_short [Gui_types]
pretty_current_cfunction_name [Value_util]
pretty_gui_offsetmap_res [Gui_types]
pretty_gui_res [Gui_types]
pretty_gui_selection [Gui_types]
pretty_loc [Precise_locs]
pretty_loc_bits [Precise_locs]
pretty_logic_evaluation_error [Eval_terms]
pretty_long_log10 [Cvalue.CardinalEstimate]
pretty_offset [Precise_locs]
pretty_predicate_status [Eval_terms]
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_lv [Mem_lvalue]
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
reads [Mem_lvalue.Compute]
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 [Eval_terms]
reduce_by_valid_loc [Eval_op]
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.
reduce_rel_from_type [Eval_op]
Reduction of a Cvalue.V.t by ==, !=, >=, >, <= and <.
reemit [Mem_lvalue]
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_code_transformation_category [File]
Adds a new category of code transformation
reinterpret [Eval_op]
reinterpret_float [Eval_op]
Read the given value value as a float int of the given fkind.
reinterpret_int [Eval_op]
Read the given value value as an int of the given ikind.
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 [Hashtbl.S]
remove [State_builder.Hashtbl]
remove_indeterminateness [Cvalue.V_Or_Uninitialized]
Remove 'unitialized' and 'escaping addresses' flags from the argument
remove_variables [Cvalue.Model]
For variables that are coming from the AST, this is equivalent to uninitializing them.
reorder [State_set]
Invert the order in which the states are iterated over
reorder_ast [File]
reorder globals so that all uses of an identifier are preceded by its declaration.
reorder_custom_ast [File]
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]
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.
returned_value [Library_functions]
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.

S
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_syntactic_context [Valarms]
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 [Eval_slevel]
singleton [FCMap.S]
singleton x y returns the one-element map that contains a binding y for x.
singleton [State_imp]
singleton [State_set]
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_disjunction_and_reduce [Eval_terms]
If reduce is true, reduce in all cases.
start_doing [Value_perf]
start_stmt [Valarms]
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]
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.
sub_untyped_pointwise [Cvalue.V]
Substracts two pointers (assumed to have type char*) and returns the difference of their offsets.

T
term_ev [Gui_eval]
tlval_ev [Gui_eval]
tlval_zone_ev [Gui_eval]
to_list [State_imp]
to_list [State_set]
to_set [State_imp]
to_string [Split_strategy]
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.
transfer_stmt [Mem_lvalue.Compute]
type_from_nb_elems [Builtins]
Helper function to create the best type for a new base.

U
uninitialize_blocks_locals [Cvalue.Model]
uninitialized [Cvalue.V_Or_Uninitialized]
Returns the canonical representant of a definitely uninitialized value.
unspecify_escaping_locals [Cvalue.V_Or_Uninitialized]
use_spec_instead_of_definition [Register]

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.
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_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_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]
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.
writes [Mem_lvalue.Compute]
written_formals [Value_util]
Over-approximation of its formals the given function may write into.