|
_add [Value_perf.Imperative_callstack_trie] |
|
_frama_c_va_arg [Builtins_nonfree] |
|
_frama_c_va_nothing [Builtins_nonfree] |
|
_self [Eval_funs] |
|
_update [Value_perf.Imperative_callstack_trie] |
|
A |
abstract_free [Builtins_nonfree_malloc] |
|
abstract_length [Builtins_nonfree_deterministic] |
|
abstract_strcmp [Builtins_nonfree] |
|
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_slevel.Arg] |
|
active_behaviors [Eval_annots.ActiveBehaviors] |
|
actualize_formals [Function_args] |
|
add [Dataflow2.StmtStartData] |
|
add [State_imp] |
|
add [State_set] |
Adding elements
|
add [State_builder.Hashtbl] |
Add a new binding.
|
add [Hashtbl.S] |
|
add_alias [Split_return.ReturnUsage] |
|
add_binding [Eval_op] |
Temporary.
|
add_binding_unspecified [Eval_op] |
Temporary.
|
add_call [Split_return.ReturnUsage] |
|
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_init [Eval_terms] |
|
add_initialized [Initial_state] |
Those functions intentionally ignore 'const' attributes.
|
add_kf_caller [Value_results] |
|
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] |
|
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 .
|
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] |
|
auto_strategy [Split_return] |
|
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_result [Builtins_nonfree_deterministic] |
|
C |
c_alarm [Eval_terms] |
|
c_labels [Register_gui] |
|
c_string_of_int [Builtins_nonfree_print_c] |
|
cacheable [Eval_slevel.Computer] |
|
call_stack [Value_util] |
|
caller_callee_callinfo [Value_perf] |
|
callers [Value_results] |
|
callstack_fold [Register_gui] |
|
cannot_find_lv [Eval_exprs] |
|
cast_lval_if_bitfield [Eval_op] |
if needed, cast the given abstract value to the given size.
|
check [Eval_funs] |
|
checkConvergence [Eval_slevel.Computer] |
|
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_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 [State_builder.Hashtbl] |
Clear the table.
|
clear [Hashtbl.S] |
|
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.
|
clob [Eval_slevel.Computer] |
Clobbered list for bases containing addresses of local variables.
|
cmp [Value_perf.Call_info] |
|
code_annotation_source [Eval_annots] |
|
code_annotation_text [Eval_annots] |
|
combinePredecessors [Eval_slevel.Computer.DataflowArg] |
|
compare [Mem_exec.Actuals] |
|
compatible_functions [Eval_exprs] |
|
compilation_unit_names [Config] |
List of names of all kernel compilation units.
|
compute [Dataflow2.Forwards] |
Fill in the T.stmtStartData, given a number of initial statements to
start from.
|
compute [Eval_slevel.Computer] |
|
compute [Split_return.ReturnUsage] |
|
computeFirstPredecessor [Eval_slevel.Computer.DataflowArg] |
|
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.DataflowArg] |
|
copy [Hashtbl.S] |
|
copy [Datatype.S] |
Deep copy: no possible sharing between x and copy x .
|
copy_char [Builtins_nonfree_deterministic] |
|
copy_float [Builtins_nonfree_deterministic] |
|
copy_int [Builtins_nonfree_deterministic] |
|
copy_offsetmap [Eval_op] |
Tempory.
|
copy_pointer [Builtins_nonfree_deterministic] |
|
copy_string [Builtins_nonfree_deterministic] |
|
count_disjunction [Eval_terms] |
|
create [Eval_annots.ActiveBehaviors] |
|
create [Hashtbl.S] |
|
create [Value_perf.Call_info] |
|
create_from_spec [Eval_annots.ActiveBehaviors] |
|
create_hidden_base [Initial_state] |
|
create_new_var [Value_util] |
Create and register a new variable inside Frama-C.
|
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_stmt [Valarms] |
|
current_stmt_tbl [Valarms] |
|
current_table [Eval_slevel.Computer] |
|
D |
datadir [Config] |
Directory where architecture independent files are.
|
date [Config] |
Compilation date.
|
debug [Eval_slevel.Computer.DataflowArg] |
|
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_results [Register] |
|
display_subtree [Value_perf] |
|
dkey [Eval_funs] |
|
dkey [Builtins_nonfree_malloc] |
|
dkey [Builtins_nonfree] |
|
dkey [Initial_state] |
|
dkey_callbacks [Eval_slevel] |
|
doEdge [Eval_slevel.Computer.DataflowArg] |
|
doGuard [Eval_slevel.Computer.DataflowArg] |
|
doInstr [Eval_slevel.Computer.DataflowArg] |
|
doStmt [Eval_slevel.Computer.DataflowArg] |
|
do_assign [Eval_stmt] |
|
do_assign_one_loc [Eval_stmt] |
|
do_promotion [Eval_op] |
|
do_promotion_c [Eval_exprs] |
|
do_warn [Valarms] |
|
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] |
|
duration [Value_perf] |
|
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 [Eval_slevel.Computer] |
|
end_stmt [Valarms] |
|
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] |
|
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] |
Set locv to true if you want to compute the value pointed to by
loc simultaneously.
|
eval_binop [Eval_terms] |
|
eval_binop [Eval_exprs] |
|
eval_binop_float [Eval_op] |
|
eval_binop_int [Eval_op] |
|
eval_by_callstack [Eval_annots] |
|
eval_const_initializer [Initial_state] |
|
eval_error_reason [Register] |
|
eval_exp_and_warn [Register_gui] |
|
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_minus_pp [Eval_op] |
|
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_location_with_deps [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_toffset [Eval_terms] |
|
eval_uneg [Eval_op] |
|
eval_unop [Eval_op] |
|
eval_user_term [Register_gui] |
|
exists [State_imp] |
|
exists [State_set] |
|
exp_ev [Register_gui] |
|
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 [Eval_op] |
Tempory.
|
find [State_builder.Hashtbl] |
Return the current binding of the given key.
|
find [Hashtbl.S] |
|
find [Value_perf.Imperative_callstack_trie] |
|
find_all [State_builder.Hashtbl] |
Return the list of all data associated with the given key.
|
find_all [Hashtbl.S] |
|
find_builtin [Builtins] |
Find a previously registered builtin.
|
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_match_in_previous [Mem_exec] |
Find a previous execution in map_inputs that matches st .
|
find_or_default [Split_return.ReturnUsage] |
|
find_subtree [Value_perf.Imperative_callstack_trie] |
|
flat [Value_perf] |
|
flat_perf_create [Value_perf] |
|
flat_print [Value_perf] |
|
float_kind [Value_util] |
Classify a Cil_types.fkind as either a 32 or 64 floating-point type.
|
float_or_double_fun_alarm [Builtins] |
|
floats_ok [Eval_funs] |
|
fold [State_imp] |
Iterators
|
fold [State_set] |
Iterators
|
fold [State_builder.Hashtbl] |
|
fold [Hashtbl.S] |
|
fold_left2_best_effort [Function_args] |
|
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_is_base_aligned [Builtins_nonfree] |
|
frama_C_sin [Builtins] |
|
frama_C_sin_precise [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_memset_imprecise [Builtins_nonfree] |
Implementation of memset that accepts imprecise arguments.
|
frama_c_memset_precise [Builtins_nonfree] |
Precise memset builtin, that requires its arguments to be sufficiently
precise abstract values.
|
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_strcmp [Builtins_nonfree] |
|
frama_c_strlen [Builtins_nonfree] |
|
frama_c_strncmp [Builtins_nonfree] |
|
frama_c_strnlen [Builtins_nonfree] |
|
frama_c_ungarble [Builtins_nonfree] |
|
frama_c_wcscmp [Builtins_nonfree] |
|
frama_c_wcsncmp [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] |
|
get_syntactic_context [Valarms] |
|
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 |
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).
|
initial_states [Eval_slevel.Arg] |
|
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] |
|
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_stmt] |
|
interpret_format [Builtins_nonfree_deterministic] |
|
interpret_format_char [Builtins_nonfree_deterministic] |
|
interpret_format_wchar [Builtins_nonfree_deterministic] |
|
interpreter [Value_parameters] |
|
inv_binop_rel [Eval_op] |
|
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_called [Value_results] |
|
is_const_write_invalid [Value_util] |
Detect that the type is const, and that option -global-const is set.
|
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_instr [Value_results] |
Returns true iff there exists executions of the statement that does
not always fail/loop (for function calls).
|
is_noop_cast [Eval_terms] |
|
is_same_term_coerce [Eval_terms] |
|
iter [Dataflow2.StmtStartData] |
|
iter [State_imp] |
|
iter [State_set] |
|
iter [State_builder.Hashtbl] |
|
iter [Hashtbl.S] |
|
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_offsetmap_result [Register_gui] |
|
join_predicate_status [Eval_terms] |
|
K |
kernel_parameters_correctness [Value_parameters] |
|
kf [Eval_slevel.Arg] |
|
kf_contains_slevel_directive [Per_stmt_slevel] |
|
kinstr_of_opt_stmt [Cil_datatype.Kinstr] |
|
L |
last_evaluate_acsl_request [Register_gui] |
|
last_time_displayed [Value_perf] |
|
lbl_here [Eval_terms] |
|
length [Dataflow2.StmtStartData] |
|
length [State_imp] |
|
length [State_set] |
|
length [State_builder.Hashtbl] |
Length of the table.
|
length [Hashtbl.S] |
|
libdir [Config] |
Directory where the Frama-C kernel library is.
|
loc [Cil_datatype.Stmt] |
|
loc [Cil_datatype.Kinstr] |
|
loc_of_typoffset [Initial_state] |
|
local_after_states [Eval_slevel.Computer] |
|
local_printer [Valarms] |
|
log_alarms [Register_gui] |
|
lop_to_cop [Eval_terms] |
|
lval_ev [Register_gui] |
|
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_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_state_for_writing [Eval_stmt] |
|
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] |
|
M |
main [Register_gui] |
|
main [Register] |
|
main [Value_perf.Call_info] |
|
main_initial_state_with_formals [Function_args] |
|
make_size [Builtins_nonfree_malloc] |
|
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
|
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_to_outputs [Mem_exec] |
|
mark_degeneration [Eval_slevel.Computer] |
|
mark_green_and_red [Eval_annots] |
|
mark_kf_as_called [Value_results] |
|
mark_rte [Eval_annots] |
|
mark_unreachable [Eval_annots] |
|
mask [Separate] |
|
may [State_builder.Option_ref] |
|
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 [Dataflow2.StmtStartData] |
|
mem [State_builder.Hashtbl] |
|
mem [Hashtbl.S] |
|
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.
|
memset_typ_offsm [Builtins_nonfree] |
Type-aware memset on an entire type.
|
memset_typ_offsm_int [Builtins_nonfree] |
memset_typ_offsm typ i returns an offsetmap of size sizeof(typ)
that maps each byte to the integer i .
|
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] |
|
N |
n [Stop_at_nth] |
|
name [Eval_slevel.Computer.DataflowArg] |
|
need_assigns [Eval_funs] |
|
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] |
|
offsetmap_contains_imprecision [Warn] |
Returns the first eventual imprecise part contained in an offsetmap
|
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_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] |
|
partition_terminating_instr [Value_results] |
Returns the list of terminating callstacks and the list of non-terminating callstacks.
|
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] |
|
paste_offsetmap [Eval_op] |
Temporary.
|
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] |
|
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_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_is_gnu_like [Config] |
whether the default preprocessor accepts the same options as gcc
(i.e.
|
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.DataflowArg] |
|
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_at_stmt [Register_gui] |
|
pretty_before_after [Register_gui] |
|
pretty_call_stack [Value_util] |
|
pretty_call_stack_short [Value_util] |
Print a call stack.
|
pretty_callstack_summary [Register_gui] |
|
pretty_current_cfunction_name [Value_util] |
|
pretty_exp_at_stmt [Register_gui] |
|
pretty_exp_result [Register_gui] |
|
pretty_float_assignment [Builtins_nonfree_print_c] |
|
pretty_float_range [Builtins_nonfree_print_c] |
|
pretty_formal_initial_state [Register_gui] |
Special case for formals
|
pretty_imprecise_memset_reason [Builtins_nonfree] |
|
pretty_int_assignment [Builtins_nonfree_print_c] |
|
pretty_int_range [Builtins_nonfree_print_c] |
|
pretty_logic_evaluation_error [Eval_terms] |
|
pretty_lva_at_stmt [Register_gui] |
|
pretty_lval_or_absolute [Register_gui] |
|
pretty_offsetmap_result [Register_gui] |
|
pretty_per_callstacks [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_strategies [Split_return] |
|
pretty_warn_mem_mode [Valarms] |
|
print [Value_perf.Call_info] |
|
print_declarations_for_malloc_bases [Builtins_nonfree_print_c] |
|
print_indentation [Value_perf] |
|
project_with_alarms [Eval_op] |
|
prologue [Separate] |
|
push_call_stack [Value_util] |
|
R |
real_mode [Eval_terms] |
|
realloc [Builtins_nonfree_malloc] |
|
reduce_actuals_by_formals [Eval_stmt] |
This function unbinds formals in state .
|
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_initialized_defined [Eval_op] |
|
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_modulo [Eval_exprs] |
state cond eqop exp1lv exp1mod exp2 reduces state by the property
exp1lv mod exp1mod =!= exp2 , =!= being the conjunct of eqop (which
must be either == or != ) and cond.positive .
|
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_op] |
|
reduce_previous_value [Eval_exprs] |
|
reduce_rel_float_double [Eval_op] |
|
reduce_rel_from_type [Eval_op] |
Reduction of a Cvalue.V.t by == , != , >= , > , <= and < .
|
reduce_rel_int [Eval_op] |
|
reduce_to_bottom [Eval_exprs] |
|
register [Builtins] |
|
register_alarm [Valarms] |
|
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 [Value_util] |
|
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 .
|
reject_empty_struct [Initial_state] |
|
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 [State_builder.Hashtbl] |
|
remove [Hashtbl.S] |
|
reorder [State_set] |
Invert the order in which the states are iterated over
|
replace [Dataflow2.StmtStartData] |
|
replace [State_builder.Hashtbl] |
Add a new binding.
|
replace [Hashtbl.S] |
|
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] |
|
results_kf_computed [Register_gui] |
|
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 .
|
S |
same_etype [Eval_terms] |
|
sc_kinstr_loc [Valarms] |
|
self [Cil_datatype.Stmt.Hptset] |
|
self [State_builder.Counter] |
|
sentinel [State_imp] |
|
set [State_builder.Ref] |
Change the referenced value.
|
set_loc [Value_util] |
|
set_syntactic_context [Valarms] |
|
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] |
|
split_disjunction_and_reduce [Eval_terms] |
If reduce is true, reduce in all cases.
|
split_eq_aux [Split_return] |
|
split_eq_multiple [Split_return] |
|
start_doing [Value_perf] |
|
start_stmt [Valarms] |
|
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_after [Eval_slevel.Computer] |
|
states_for_callbacks [Eval_slevel.Computer] |
|
states_unmerged [Eval_slevel.Computer] |
|
states_unmerged_for_callbacks [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] |
|
stmt_state [Eval_slevel.Computer] |
|
stmt_widening_info [Eval_slevel.Computer] |
|
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] |
|
supported_logic_var [Eval_terms] |
|
sync_filetree [Register_gui] |
|
syntactic_context [Valarms] |
|
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] |
|
two61 [Builtins_nonfree] |
|
type_from_nb_elems [Builtins] |
Helper function to create the best type for a new base.
|
types [Builtins_nonfree_print_c] |
|
U |
unbind_logic_vars [Eval_terms] |
|
under_from_over [Eval_terms] |
|
uninitialized [Builtins_nonfree_malloc] |
|
unsupported [Eval_terms] |
|
unsupported_lvar [Eval_terms] |
|
update_stmt_states [Eval_slevel.Computer] |
|
update_stmt_widening_info [Eval_slevel.Computer] |
|
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] |
|
verify_assigns_from [Eval_annots] |
|
version [Config] |
Frama-C Version identifier.
|
W |
warn_all_mode [Value_util] |
|
warn_all_quiet_mode [Value_util] |
|
warn_conjuctive_annots [Valarms] |
Auxiliary function that displays two simultaneous alarms as a conjunction
|
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 [Valarms] |
|
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_overlap [Warn] |
|
warn_overlap [Valarms] |
|
warn_pointer_comparison [Valarms] |
|
warn_pointer_subtraction [Valarms] |
|
warn_raise_mode [Eval_terms] |
|
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_reduce_index [Eval_exprs] |
We are accessing an array of size array_size at indexes index in state
state .
|
warn_reduce_shift_left [Eval_exprs] |
Reduce both arguments of a left shift, and the state if possible
|
warn_reduce_shift_rhs [Eval_exprs] |
Reduce the rhs argument of a shift so that it fits inside size bits.
|
warn_right_exp_imprecision [Warn] |
|
warn_separated [Valarms] |
|
warn_shift [Valarms] |
|
warn_shift_left_positive [Valarms] |
|
warn_top [Warn] |
Abort the analysis, signaling that Top has been found.
|
warn_uninitialized [Valarms] |
|
warn_unknown_size [Initial_state] |
|
warn_unknown_size_aux [Initial_state] |
|
warn_valid_string [Valarms] |
|
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_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 .
|
write_string_to_memory [Builtins_nonfree_deterministic] |
|
written_formals [Value_util] |
Over-approximation of its formals the given function may write into.
|