Index of values


_add [Value_perf.Imperative_callstack_trie]
_cardinal_offset [Precise_locs]
_frama_c_va_arg [Builtins_nonfree]
_frama_c_va_nothing [Builtins_nonfree]
_scale_offset [Precise_locs]
_self [Eval_funs]
_update [Value_perf.Imperative_callstack_trie]

A
abstract_free [Builtins_nonfree_malloc]
abstract_length [Builtins_nonfree_deterministic]
abstract_strlen [Builtins_nonfree]
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 [Dataflow2.StmtStartData]
add [State_imp]
add [State_set]
Adding elements
add [Hashtbl.S]
add [State_builder.Hashtbl]
Add a new binding.
add_alias [Split_return.ReturnUsage]
add_call [Split_return.ReturnUsage]
add_caller [Kf_state]
add_compare [Split_return.ReturnUsage]
add_compare_ct [Split_return.ReturnUsage]
add_correctness_dep [Value_parameters]
add_dep [Value_parameters]
add_deps [Eval_terms]
add_direct_comparison [Split_return.ReturnUsage]
add_exn [State_imp]
add_exn [State_set]
add_here [Eval_terms]
add_initialized [Initial_state]
add_logic [Eval_terms]
add_old [Eval_terms]
add_post [Eval_terms]
add_pre [Eval_terms]
add_precision_dep [Value_parameters]
add_retres_to_state [Library_functions]
add_statement [State_set]
Update the trace of all the states in the stateset.
add_to_list [State_imp]
add_to_list [State_set]
add_unitialized [Initial_state]
add_watch [Builtins_nonfree_watchpoint]
after_call [Value_perf.Call_info]
alarm_behavior_raise_problem [Builtins_nonfree_deterministic]
alarms [Value_parameters]
alloc_abstract [Builtins_nonfree_malloc]
alloc_multiple_by_stack [Builtins_nonfree_malloc]
alloc_once_by_stack [Builtins_nonfree_malloc]
alloc_with_validity [Builtins_nonfree_malloc]
approximated_after_state [Register_gui]
assign_return_to_lv [Eval_stmt]
assign_return_to_lv_one_loc [Eval_stmt]
assigns_inputs_to_zone [Register]
assigns_outputs_aux [Register]
assigns_outputs_to_locations [Register]
assigns_outputs_to_zone [Register]
ast_error [Eval_terms]

B
bases [Mem_exec]
before_call [Value_perf.Call_info]
behavior_from_name [Eval_annots.ActiveBehaviors]
behavior_inactive [Eval_annots]
bind_logic_vars [Eval_terms]
block_top_addresses_of_locals [Locals_scoping]
Return a function that topifies all references to the variables local to the given blocks.
bottom [Locals_scoping]
bottom_location_bits [Precise_locs]
bottom_result [Builtins_nonfree_deterministic]

C
c_alarm [Eval_terms]
c_string_of_int [Builtins_nonfree_print_c]
cacheable [Eval_slevel.Computer]
call_stack [Value_util]
caller_callee_callinfo [Value_perf]
callers [Kf_state]
cannot_find_lv [Eval_exprs]
cardinal_zero_or_one [Precise_locs]
cardinal_zero_or_one_location_bits [Precise_locs]
cardinal_zero_or_one_offset [Precise_locs]
cast_lval_bitfield [Eval_op]
check [Eval_funs]
checkConvergence [Eval_slevel.Computer]
check_arg_size [Function_args]
check_c_function_exists [Value_parameters]
check_fct_postconditions [Eval_annots]
check_fct_preconditions [Eval_annots]
Check the precondition of kf.
check_if_base_is_leaked [Builtins_nonfree_malloc]
check_leaked_malloced_bases [Builtins_nonfree_malloc]
check_no_recursive_call [Warn]
Check that kf is not already present in the call stack
check_non_overlapping [Eval_stmt]
check_not_comparable [Warn]
check_unspecified_sequence [Eval_stmt]
cleant_outputs [Register_gui]
cleanup_results [Mem_exec]
Clean all previously stored results
clear [Dataflow2.StmtStartData]
clear [Current_table]
clear [Hashtbl.S]
clear [Stop_at_nth]
clear [State_builder.Ref]
Reset the reference to its default value.
clear [State_builder.Hashtbl]
Clear the table.
clear_call_stack [Value_util]
Functions dealing with call stacks.
clob [Eval_slevel.Computer]
Clobbered list for bases containing addresses of local variables.
cmp [Value_perf.Call_info]
combinePredecessors [Eval_slevel.Computer]
combine_base_precise_offset [Precise_locs]
combine_loc_precise_offset [Precise_locs]
compare [Mem_exec.Actuals]
compatible_functions [Eval_exprs]
compilation_unit_names [Config]
List of names of all kernel compilation units.
compute [Split_return.ReturnUsage]
computeFirstPredecessor [Eval_slevel.Computer]
compute_actual [Function_args]
compute_assigns [Eval_funs]
Evaluate the assigns of kf active according to active_behaviors in the state with_formals.
compute_call [Eval_funs]
Compute a call to kf, called from call_kinstr, in the state state.
compute_call_ref [Eval_stmt]
compute_from_entry_point [Eval_funs]
Compute a call to the main function.
compute_maybe_builtin [Eval_funs]
Compute a call to a possible builtin kf in state state.
compute_non_linear_assignments [Non_linear]
compute_non_recursive_call [Eval_funs]
Compute a call to kf from call_kinstr, assuming kf is not yet present in the callstack.
compute_recursive_call [Eval_funs]
compute_using_body [Eval_funs]
Compute kf in state with_formals according to the body f of kf.
compute_using_spec_or_body [Eval_funs]
Compute a call to kf in the state with_formals.
compute_using_specification [Eval_funs]
Evaluate kf in state with_formals, first by reducing by the preconditions, then by evaluating the assigns, then by reducing by the post-conditions.
compute_widen_hints [Widen]
conditions_table [Eval_slevel.Computer]
conv_status [Eval_annots]
copy [Eval_slevel.Computer]
copy [Hashtbl.S]
copy [Datatype.S]
Deep copy: no possible sharing between x and copy x.
copy_float [Builtins_nonfree_deterministic]
copy_int [Builtins_nonfree_deterministic]
copy_pointer [Builtins_nonfree_deterministic]
copy_string [Builtins_nonfree_deterministic]
count_disjunction [Eval_terms]
counter_unroll_target [Eval_slevel.Computer]
create [Eval_annots.ActiveBehaviors]
create [Current_table]
create [Hashtbl.S]
create [Value_perf.Call_info]
create_from_spec [Eval_annots.ActiveBehaviors]
create_hidden_base [Initial_state]
create_node [Value_perf.Imperative_callstack_trie]
current_fundec [Eval_slevel.Computer]
current_kf [Eval_slevel.Computer]
current_kf [Value_util]
The current function is the one on top of the call stack.
current_table [Eval_slevel.Computer]

D
datadir [Config]
Directory where architecture independent files are.
date [Config]
Compilation date.
debug [Eval_slevel.Computer]
debug [Split_return.ReturnUsage]
debug_result [Value_util]
default [Split_return]
deps_at [Eval_terms]
display [Register]
display [Value_perf]
Display a complete summary of performance informations.
display_evaluation_error [Eval_terms]
display_interval [Value_perf]
display_node [Value_perf]
display_one [Eval_slevel.Computer]
display_results [Register]
display_subtree [Value_perf]
dkey [Eval_funs]
dkey [Builtins_nonfree_malloc]
dkey [Builtins_nonfree]
dkey_callbacks [Eval_slevel]
doEdge [Eval_slevel.Computer]
doGuard [Eval_slevel.Computer]
doGuardOneCond [Eval_slevel.Computer]
doInstr [Eval_slevel.Computer]
doStmt [Eval_slevel.Computer]
doStmtSpecific [Eval_slevel.Computer]
do_assign [Eval_stmt]
do_assign_abstract_value [Eval_stmt]
Precondition: the type of v and the type of loc_lv may be different only through a truncation or an extension.
do_assign_one_loc [Eval_stmt]
do_promotion [Eval_op]
do_promotion_c [Eval_exprs]
does_not_account_smaller_than [Value_perf]
dot [Config]
Dot command name.
double_double_fun [Builtins]
dump_args [Builtins]
dump_state [Builtins]
Builtins with multiple names; the lookup is done using a distinctive prefix
dump_state_file [Builtins]

E
einteger [Eval_terms]
emit_status [Eval_annots]
emitter [Value_util]
empty [State_imp]
Creation
empty [State_set]
Creation
empty [Value_perf.Imperative_callstack_trie]
empty_logic_deps [Eval_terms]
empty_record [Current_table]
enumerate_valid_bits [Precise_locs]
env_annot [Eval_terms]
env_assigns [Eval_terms]
env_current_state [Eval_terms]
env_here [Eval_terms]
env_post_f [Eval_terms]
env_pre_f [Eval_terms]
env_state [Eval_terms]
epilogue [Separate]
equal_offsetmap_result [Register_gui]
equal_watch [Builtins_nonfree_watchpoint]
ereal [Eval_terms]
eval_and_reduce_pre_post [Eval_annots]
eval_as_exact_loc [Eval_exprs]
eval_binop [Eval_terms]
eval_binop [Eval_exprs]
eval_binop_float [Eval_op]
eval_binop_int [Eval_op]
eval_const_initializer [Initial_state]
eval_error_reason [Register]
eval_expr [Eval_exprs]
eval_expr_with_deps_state [Eval_exprs]
eval_expr_with_deps_state_subdiv [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_host [Eval_exprs]
eval_initializer [Initial_state]
eval_lval [Eval_exprs]
eval_lval_and_convert [Eval_exprs]
eval_lval_one_loc [Eval_exprs]
eval_offset [Eval_exprs]
eval_predicate [Register]
eval_predicate [Eval_terms]
eval_single_initializer [Initial_state]
eval_term [Eval_terms]
eval_term_as_exact_loc [Eval_terms]
eval_thost_toffset [Eval_terms]
eval_tlhost [Eval_terms]
eval_tlval [Eval_terms]
eval_tlval_as_location [Eval_terms]
eval_tlval_as_locations [Eval_terms]
eval_tlval_as_zone [Eval_terms]
eval_toffset [Eval_terms]
eval_uneg [Eval_op]
eval_unop [Eval_op]
eval_user_term [Register_gui]
exists [State_imp]
exists [State_set]
expr_to_kernel_function [Register]
expr_to_kernel_function_state [Register]
externalize [Eval_slevel.Computer]
externalize [Eval_stmt]
extract_slevel_directive [Per_stmt_slevel]

F
filter_and_sort [Value_perf.Call_info]
filter_callstack [Builtins_nonfree_malloc]
filter_if [Separate]
filter_state [Mem_exec]
final_states [Eval_slevel.Computer]
find [Dataflow2.StmtStartData]
find [Non_linear]
find [Hashtbl.S]
find [Value_perf.Imperative_callstack_trie]
find [State_builder.Hashtbl]
Return the current binding of the given key.
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_current [Current_table]
find_deps_term_no_transitivity_state [Register]
find_lv [Eval_exprs]
find_lv_plus_offset [Eval_exprs]
If possible, decomposes e into lval+offset; where lval is a Cil expression, and offset is an Ival.t, in bytes.
find_or_default [Split_return.ReturnUsage]
find_subtree [Value_perf.Imperative_callstack_trie]
find_superposition [Current_table]
find_widening_info [Current_table]
Extraction
flat [Value_perf]
flat_perf_create [Value_perf]
flat_print [Value_perf]
floats_ok [Eval_funs]
fold [Precise_locs]
fold [State_imp]
Iterators
fold [State_set]
Iterators
fold [Hashtbl.S]
fold [State_builder.Hashtbl]
fold_left2_best_effort [Function_args]
fold_offset [Precise_locs]
fold_on_disjunction [Eval_terms]
fold_sorted [State_builder.Hashtbl]
fold_succ [Per_stmt_slevel.G]
fold_vertex [Per_stmt_slevel.G]
for_kf [Per_stmt_slevel]
force_compute [Eval_funs]
frama_C_assert [Builtins]
frama_C_compare_cos [Builtins]
frama_C_cos [Builtins]
frama_C_cos_precise [Builtins]
frama_C_exp [Builtins]
frama_C_is_base_aligned [Builtins_nonfree]
frama_C_sin [Builtins]
frama_C_sin_precise [Builtins]
frama_C_sqrt [Builtins]
frama_c_alloc_infinite [Builtins_nonfree_malloc]
frama_c_bzero [Builtins]
frama_c_copy_block [Builtins_nonfree]
frama_c_dump_assert [Builtins_nonfree_print_c]
frama_c_dump_assignments [Builtins_nonfree_print_c]
frama_c_free [Builtins_nonfree_malloc]
Builtin for free function
frama_c_fscanf [Builtins_nonfree]
frama_c_interval_split [Builtins_nonfree]
frama_c_memcmp [Builtins_nonfree]
frama_c_memcpy [Builtins_nonfree]
frama_c_memset [Builtins_nonfree]
frama_c_offset [Builtins_nonfree]
frama_c_printf [Builtins_nonfree_deterministic]
frama_c_snprintf [Builtins_nonfree_deterministic]
frama_c_sprintf [Builtins_nonfree_deterministic]
frama_c_strlen [Builtins_nonfree]
frama_c_strnlen [Builtins_nonfree]
frama_c_ungarble [Builtins_nonfree]
frama_c_wprintf [Builtins_nonfree_deterministic]
free [Builtins_nonfree_malloc]
fresh_base [Builtins_nonfree_malloc]

G
generate_specs [Eval_funs]
get [State_builder.Counter]
get [Library_functions]
get [State_builder.Ref]
Get the referenced value.
getWidenHints [Widen]
get_influential_vars [Eval_exprs]
get_option [State_builder.Option_ref]
get_rounding_mode [Value_util]
get_slevel [Value_util]
guess_intended_malloc_type [Builtins_nonfree_malloc]
gui_compute_values [Register_gui]

H
handle_overflow [Eval_op]
has_requires [Eval_annots]
header [Eval_annots.ActiveBehaviors]
hide_unused [Register_gui]
hide_unused_function_or_var [Register_gui]

I
imprecise_location [Precise_locs]
imprecise_location_bits [Precise_locs]
imprecise_offset [Precise_locs]
incr [Stop_at_nth]
infer_binop_res_type [Eval_terms]
infer_type [Eval_terms]
init_trailing_padding [Initial_state]
init_var_zero [Initial_state]
initial_context [Value_parameters]
initial_state_contextfree_only_globals [Initial_state]
Initial state in -lib-entry mode
initial_state_only_globals [Initial_state]
Initial value for globals and NULL in no-lib-entry mode (everything initialized to 0).
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_padding [Initial_state]
inject_location_bits [Precise_locs]
int_hrange [Builtins_nonfree]
int_neg_ival [Builtins_nonfree]
int_nonneg_ival [Builtins_nonfree]
int_nonpos_ival [Builtins_nonfree]
int_pos_ival [Builtins_nonfree]
interp_annot [Eval_annots]
interp_call [Eval_slevel.Computer]
interp_call [Eval_stmt]
interpret_format [Builtins_nonfree_deterministic]
interpret_format_char [Builtins_nonfree_deterministic]
interpret_format_wchar [Builtins_nonfree_deterministic]
interpreter [Value_parameters]
isLogicNonCompositeType [Eval_terms]
is_active [Eval_annots.ActiveBehaviors]
is_active_aux [Eval_annots.ActiveBehaviors]
is_basic_loop [Eval_slevel.Computer]
is_bitfield [Eval_op]
Bitfields
is_bottom_loc [Precise_locs]
is_bottom_offset [Precise_locs]
is_called [Kf_state]
is_directed [Per_stmt_slevel.G]
is_empty [State_imp]
Information
is_empty [State_set]
Information
is_gui [Config]
Is the Frama-C GUI running?
is_init [Builtins_nonfree]
is_loop [Eval_slevel.Computer]
is_natural_loop [Eval_slevel.Computer]
is_non_terminating_call [Value_results]
is_return [Eval_slevel.Computer]
is_same_term_coerce [Eval_terms]
iter [Dataflow2.StmtStartData]
iter [State_imp]
iter [State_set]
iter [Hashtbl.S]
iter [State_builder.Hashtbl]
iter_sorted [State_builder.Hashtbl]
iter_succ [Per_stmt_slevel.G]
iter_vertex [Per_stmt_slevel.G]

J
join [State_imp]
Export
join [State_set]
Export
join_env [Eval_terms]
join_final_states [Split_return]
Join the given state_set.
join_label_states [Eval_terms]
join_list_predicate_status [Eval_terms]
join_logic_deps [Eval_terms]
join_predicate_status [Eval_terms]

K
kernel_parameters_correctness [Value_parameters]
kf_contains_slevel_directive [Per_stmt_slevel]
kinstr_of_opt_stmt [Cil_datatype.Kinstr]

L
last_time_displayed [Value_perf]
lbl_here [Eval_terms]
length [Dataflow2.StmtStartData]
length [State_imp]
length [State_set]
length [Hashtbl.S]
length [State_builder.Hashtbl]
Length of the table.
libdir [Config]
Directory where the Frama-C kernel library is.
light_topify [Eval_op]
Change all offsets to top_int.
loc [Cil_datatype.Stmt]
loc [Cil_datatype.Kinstr]
loc_bottom [Precise_locs]
loc_size [Precise_locs]
local_after_states [Eval_slevel.Computer]
log_alarms [Register_gui]
lop_to_cop [Eval_terms]
lval_or_absolute_to_offsetmap [Register_gui]
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_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_zone [Register]
lval_to_zone_state [Register]
lval_to_zone_with_deps_state [Register]

M
main [Register_gui]
main [Register]
main [Value_perf.Call_info]
main_initial_state_with_formals [Function_args]
make_precise_loc [Precise_locs]
make_size [Builtins_nonfree_malloc]
make_type [Datatype.Hashtbl]
make_watch_cardinal [Builtins_nonfree_watchpoint]
make_watch_value [Builtins_nonfree_watchpoint]
make_well [Initial_state]
malloc_var [Builtins_nonfree_malloc]
map [State_builder.Option_ref]
map [State_set]
map_outputs [Value_util]
mark_as_called [Kf_state]
mark_call_terminating [Value_results]
mark_degeneration [Eval_slevel.Computer]
mark_rte [Eval_annots]
mark_unreachable [Eval_annots]
mask [Separate]
mask_both [Eval_slevel.Computer]
mask_else [Eval_slevel.Computer]
mask_then [Eval_slevel.Computer]
may [State_builder.Option_ref]
mem [Dataflow2.StmtStartData]
mem [Hashtbl.S]
mem [State_builder.Hashtbl]
mem_builtin [Builtins]
Does the builtin table contain an entry for name?
memcmp_ivals [Builtins_nonfree]
memo [Datatype.Hashtbl]
memo tbl k f returns the binding of k in tbl.
memo [State_builder.Option_ref]
Memoization.
memo [State_builder.Hashtbl]
Memoization.
merge [State_set]
Merge the two sets together.
merge_after [Eval_slevel.Computer]
merge_db_table [Current_table]
Merge the results of the current analysis with the global results.
merge_if_loop [Eval_slevel.Computer]
merge_into [State_set]
Raise Unchanged if the first set was already included in into
merge_results [Eval_slevel.Computer]
merge_set_return_new [State_imp]

N
n [Stop_at_nth]
name [Eval_slevel.Computer]
need_cast [Eval_stmt]
new_watchpoint [Builtins_nonfree_watchpoint]
next [State_builder.Counter]
Increments the counter and returns a fresh value
no_env [Eval_terms]
no_memoization_enabled [Mark_noresults]
no_result [Eval_terms]
not_an_exact_loc [Eval_exprs]
notify_status [Eval_annots]

O
obviously_terminates [Eval_slevel.Computer]
obviously_terminates [State_set]
ocamlc [Config]
Name of the bytecode compiler.
ocamlopt [Config]
Name of the native compiler.
of_list [State_set]
of_list_forget_history [State_set]
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_of_lv [Eval_exprs]
offsetmap_of_v [Eval_op]
Transformation a value into an offsetmap of size sizeof(typ) bytes.
offsetmap_pretty [Builtins_nonfree_print_c]
offsetmap_top_addresses_of_locals [Locals_scoping]
offsetmap_top_addresses_of_locals is_local returns a function that topifies all the parts of an offsetmap that contains a pointer verifying is_local.
offsm_from_validity [Builtins_nonfree_malloc]
options_ok [Eval_funs]
overridden_by_builtin [Builtins]
Should the given function be replaced by a call to a builtin
overwrite_current_state [Eval_terms]
overwrite_state [Eval_terms]

P
parameters_correctness [Value_parameters]
parameters_tuning [Value_parameters]
pass_cast [Eval_exprs]
Detects if an expression can be considered as a lvalue even though it is hidden by a cast that does not change the lvalue.
pass_logic_cast [Eval_terms]
perf [Value_perf]
performance [Value_parameters]
plugin_dir [Config]
Directory where the Frama-C dynamic plug-ins are.
pop_call_stack [Value_util]
post_cleanup [Eval_funs]
post_kind [Eval_annots]
pp_bhv [Eval_annots.ActiveBehaviors]
pp_callstack [Value_util]
Prints the current callstack.
pp_eval_ok [Register_gui]
pp_header [Eval_annots]
pp_pre_post_kind [Eval_annots]
pp_v [Eval_op]
pre [Eval_funs]
precision_tuning [Value_parameters]
predicate_deps [Eval_terms]
preprocessor [Config]
Name of the default command to call the preprocessor.
preprocessor_keep_comments [Config]
true if the default preprocessor selected during compilation is able to keep comments (hence ACSL annotations) in its output.
pretty [Eval_slevel.Computer]
pretty [State_imp]
pretty [State_set]
pretty_actuals [Value_util]
pretty_assignment_expression [Builtins_nonfree_print_c]
pretty_assignment_expression_ival [Builtins_nonfree_print_c]
pretty_call_stack [Value_util]
pretty_call_stack_short [Value_util]
Print a call stack.
pretty_current_cfunction_name [Value_util]
pretty_float_assignment [Builtins_nonfree_print_c]
pretty_float_range [Builtins_nonfree_print_c]
pretty_formal_initial_state [Register_gui]
pretty_int_assignment [Builtins_nonfree_print_c]
pretty_int_range [Builtins_nonfree_print_c]
pretty_loc [Precise_locs]
pretty_logic_evaluation_error [Eval_terms]
pretty_lva_at_stmt [Register_gui]
pretty_lva_before_after [Register_gui]
pretty_lva_callstacks [Register_gui]
pretty_lval_or_absolute [Register_gui]
pretty_offset [Precise_locs]
pretty_offsetmap_result [Register_gui]
pretty_pointer_assignment [Builtins_nonfree_print_c]
pretty_predicate_status [Eval_terms]
pretty_sid [Cil_datatype.Stmt]
Pretty print the sid of the statement
pretty_state_as_c_assert [Builtins_nonfree_print_c]
pretty_state_as_c_assignments [Builtins_nonfree_print_c]
pretty_stitched_offsetmap [Register_gui]
pretty_usage [Split_return.ReturnUsage]
previous_matches [Mem_exec]
print [Value_perf.Call_info]
print_declarations_for_malloc_bases [Builtins_nonfree_print_c]
print_indentation [Value_perf]
prologue [Separate]
push_call_stack [Value_util]

R
real_mode [Eval_terms]
realloc [Builtins_nonfree_malloc]
reduce_by_accessed_loc [Eval_exprs]
reduce_by_comparison [Eval_exprs]
Reduce the state for comparisons of the form 'v Rel k', 'k Rel v' or 'v = w'
reduce_by_cond [Eval_exprs]
raises Reduce_to_bottom and never returns Cvalue.Model.bottom
reduce_by_cond_enumerate [Eval_exprs]
reduce_by_left_comparison [Eval_exprs]
reduce_by_left_comparison_abstract [Eval_exprs]
Reduce the state for comparisons of the form 'v Rel k', where v evaluates to a location, and k to some value
reduce_by_left_relation [Eval_terms]
reduce_by_predicate [Eval_terms]
reduce_by_predicate_content [Eval_terms]
reduce_by_relation [Eval_terms]
reduce_by_valid [Eval_terms]
reduce_by_valid_loc [Eval_exprs]
reduce_index [Eval_exprs]
We are accessing an array of size array_size at indexes index in state state.
reduce_rel_antisymmetric_float [Eval_op]
reduce_rel_antisymmetric_int [Eval_op]
reduce_rel_float [Eval_op]
reduce_rel_from_type [Eval_exprs]
reduce_rel_int [Eval_op]
reduce_rel_symmetric_float [Eval_op]
reduce_rel_symmetric_int [Eval_op]
reduce_to_bottom [Eval_exprs]
register_builtin [Builtins_nonfree]
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_callback [Mem_exec]
register_malloced_base [Builtins_nonfree_malloc]
register_new_var [Library_functions]
Auxiliary function that registers a new variable declared by Value within the kernel internal tables
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 [Hashtbl.S]
remove [State_builder.Hashtbl]
remove_formals_from_state [Value_util]
reorder [State_set]
Invert the order in which the states are iterated over
replace [Dataflow2.StmtStartData]
replace [Hashtbl.S]
replace [State_builder.Hashtbl]
Add a new binding.
reset [Hashtbl.S]
reset [Value_perf.Imperative_callstack_trie]
reset [Value_perf]
Reset the internal state of the module; to call at the very beginning of the analysis.
resolv_func_vinfo [Eval_exprs]
resolve_bases_to_free [Builtins_nonfree_malloc]
results [Eval_slevel.Computer]
retrieve_annot [Per_stmt_slevel]
return [Eval_slevel.Computer]
return_lv [Eval_slevel.Computer]
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.
run [Mark_noresults]

S
same_etype [Eval_terms]
self [Cil_datatype.Stmt.Hptset]
self [State_builder.Counter]
sentinel [State_imp]
set [State_builder.Ref]
Change the referenced value.
set_loc [Value_util]
shift_offset [Precise_locs]
shift_offset_by_singleton [Precise_locs]
should_memorize_function [Mark_noresults]
singleton [State_imp]
singleton [State_set]
singleton_eight [Builtins_nonfree]
size_non_constant_malloc [Builtins_nonfree_malloc]
sizeof_lval_typ [Eval_op]
Size of the type of a lval, taking into account that the lval might have been a bitfield.
slevel [Eval_slevel.Computer]
slevel_merge_after_loop [Eval_slevel.Computer]
small_cardinal [Precise_locs]
split_disjunction_and_reduce [Eval_terms]
If reduce is true, reduce in all cases.
split_eq_aux [Split_return]
split_eq_multiple [Split_return]
split_option [Value_parameters]
split_option_multiple [Value_parameters]
start_doing [Value_perf]
state_pretty [Builtins_nonfree_print_c]
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.
states [Current_table]
states_after [Eval_slevel.Computer]
static_gui_plugins [Config]
GUI of plug-ins statically linked within Frama-C.
static_plugins [Config]
Plug-ins statically linked within Frama-C.
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.
store_state_after_during_dataflow [Eval_slevel.Computer]
strategy [Split_return]
string_of_predicate_status [Eval_terms]
substitute_space_by_underscore [Builtins_nonfree_print_c]
succs [Per_stmt_slevel.G]
summarize [Split_return.ReturnUsage]
superpositions [Current_table]
Export
supported_logic_var [Eval_terms]
sync_filetree [Register_gui]

T
table [Builtins]
to_do_on_select [Register_gui]
to_list [State_imp]
to_list [State_set]
to_set [State_imp]
too_linear [Eval_exprs]
top [Locals_scoping]
top_addresses_of_locals [Locals_scoping]
Return two functions that topifies all references to the locals and formals of the given function.
top_gather_locals [Locals_scoping]
topify_offset [Eval_exprs]
topify_pointed_arguments [Builtins_nonfree]
total_duration [Value_perf.Call_info]
typeHasAttribute [Initial_state]
type_from_nb_elems [Builtins_nonfree_malloc]
types [Builtins_nonfree_print_c]

U
unbind_logic_vars [Eval_terms]
uninitialized [Builtins_nonfree_malloc]
unsupported [Eval_terms]
unsupported_lvar [Eval_terms]
update_and_tell_if_changed [Current_table]
Updating
update_widening_info [Current_table]
use_spec_instead_of_definition [Register]
used_var [Register_gui]

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.
value_panel [Register_gui]
value_pretty [Builtins_nonfree_print_c]
value_uninit_pretty [Builtins_nonfree_print_c]
version [Config]
Frama-C Version identifier.

W
warn_all_mode [Value_util]
warn_all_quiet_mode [Value_util]
warn_float [Warn]
warn_float_addr [Warn]
warn_imprecise_lval_read [Warn]
warn_indeterminate [Value_util]
warn_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.
warn_locals_escape [Warn]
warn_locals_escape_result [Warn]
warn_modified_result_loc [Warn]
This function should be used to treat a call lv = kf(...).
warn_overlap [Warn]
warn_raise_mode [Eval_terms]
warn_reduce_by_accessed_loc [Eval_exprs]
warn_right_exp_imprecision [Warn]
warn_unknown_size [Initial_state]
warn_unknown_size_aux [Initial_state]
warning_once_current [Value_util]
watch_hook [Builtins_nonfree_watchpoint]
watch_table [Builtins_nonfree_watchpoint]
with_alarm_stop_at_first [Value_util]
with_alarms [Builtins_nonfree_deterministic]
with_alarms_raise_exn [Value_util]
wrap_double [Eval_op]
wrap_int [Eval_op]
Specialization of the function above for standard types
wrap_ptr [Eval_op]
write_string_to_memory [Builtins_nonfree_deterministic]