Index of values


_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.