A | |
actual_alloca [Functions.Libc] | The name of an actual |
add [State_builder.Hashtbl] | Add a new binding. |
add [Interval.Env] | |
add [Env.Logic_binding] | |
add [Literal_strings] | |
add_assert [Env] |
|
add_e_acsl_library [Main] | |
add_loop_invariant [Env] | |
add_stmt [Env] |
|
affect [Gmpz] |
|
annotation_kind [Env] | |
apply_after_transformation [Loops] | |
apply_on_e_acsl_ast [Main] | |
B | |
before_translation [Keep_status] | to be called just before the main translation |
C | |
c_int [Typing] | |
change_printer [Main] | |
check [Main] | |
clear [State_builder.Hashtbl] | Clear the table. |
clear [Typing] | Remove all the previously computed types. |
clear [Interval.Env] | |
clear [Keep_status] | to be called before any program transformation |
clear [Exit_points] | Clear all gathered data |
clear [Gmpz] | build stmt "mpz_clear(v)" |
compute_quantif_guards_ref [Typing] | Forward reference. |
cty [Misc] | |
current_kf [Env] | Kernel function currently visited in the new project. |
D | |
delete_vars [Exit_points] | Given a statement which potentially leads to an early scope exit (such as goto, break or continue) return the list of local variables which need to be removed from tracking before that statement is executed. |
dkey_analysis [Options] | |
dkey_dup [Options] | |
dkey_translation [Options] | |
dkey_typing [Options] | |
do_visit [Visit] | |
dummy [Env] | |
dup [Dup_functions] | |
E | |
empty [Env] | |
enable [Temporal] | Enable/disable temporal transformations |
exists [Parameter_sig.Set] | Is there some element satisfying the given predicate? |
exp [Rte] | RTEs of a given exp, as a list of code annotations. |
extend_ast [Main] | |
extend_stmt_in_place [Env] |
|
extended_ast_project [Main] | |
F | |
find [State_builder.Hashtbl] | Return the current binding of the given key. |
find [Literal_strings] | |
find [Builtins] | Get the varinfo corresponding to the given E-ACSL built-in name. |
find_all [State_builder.Hashtbl] | Return the list of all data associated with the given key. |
fold [State_builder.Hashtbl] | |
fold [Literal_strings] | |
fold_sorted [State_builder.Hashtbl] | |
G | |
generate [Exit_points] | Visit a function and populate data structures used to compute exit points |
generate_code [Main] | |
generate_global_init [Temporal] | Generate |
generate_rte [Env] | |
generic_handle [Error] | Run the closure with the given argument and handle potential errors. |
get [Env.Logic_binding] | |
get [Env.Varname] | |
get_behavior [Env] | |
get_cast [Typing] | Get the type which the given term must be converted to (if any). |
get_cast_of_predicate [Typing] | Like |
get_function_name [Parameter_sig.String] | returns the given argument only if it is a valid function name
(see |
get_generated_variables [Env] | All the new variables local to the visited function. |
get_integer_op [Typing] | |
get_integer_op_of_predicate [Typing] | |
get_integer_ty [Typing] | |
get_lib_fun_vi [Misc] | Return varinfo corresponding to a name of a given library function |
get_op [Typing] | Get the type which the operation on top of the given term must be generated to. |
get_original_name [Functions.RTL] | Retrieve the name of the kernel function and strip prefix that indicates that it has been generated by the instrumentation. |
get_plain_string [Parameter_sig.String] | always return the argument, even if the argument is not a function name. |
get_possible_values [Parameter_sig.String] | What are the acceptable values for this parameter. |
get_printf_argument_str [Functions.Libc] | Given the name of a printf-like function and the list of its variadic arguments return a literal string expression where each character describes the type of an argument from a list. |
get_rtl_replacement_name [Functions.RTL] | Given the name of C library function return the name of the RTL function that potentially replaces it. |
get_stmt [Label] | |
get_typ [Typing] | Get the type which the given term must be generated to. |
get_visitor [Env] | |
gmp [Typing] | |
H | |
handle [Error] | Run the closure with the given argument and handle potential errors. |
handle_function_parameters [Temporal] |
|
handle_stmt [Temporal] | Update local environment ( |
has_fundef [Functions] | |
has_no_new_stmt [Env] | Assume that a local context has been previously pushed. |
has_rtl_replacement [Functions.RTL] | Given the name of C library function return true if there is a drop-in replacement function for it in the RTL. |
I | |
ikind [Typing] | |
infer [Interval] |
|
init [Gmpz] | build stmt "mpz_init(v)" |
init_set [Gmpz] |
|
init_t [Gmpz] | Must be called before any use of GMP |
interv_of_typ [Interval] | |
is_alloca [Functions.Libc] | Return |
is_alloca_name [Functions.Libc] | Same as |
is_dyn_alloc [Functions.Libc] | Return |
is_dyn_alloc_name [Functions.Libc] | Same as |
is_dyn_free [Functions.Libc] | Return |
is_dyn_free_name [Functions.Libc] | Same as |
is_empty [Literal_strings] | |
is_enabled [Temporal] | Return a boolean value indicating whether temporal analysis is enabled |
is_generated_kf [Functions.RTL] | Same as |
is_generated_literal_string_name [Functions.RTL] | Same as |
is_generated_name [Functions.RTL] | |
is_library_loc [Misc] | |
is_memcpy [Functions.Libc] | Return |
is_memcpy_name [Functions.Libc] | Same as |
is_memset [Functions.Libc] | Return |
is_memset_name [Functions.Libc] | Same as |
is_now_referenced [Gmpz] | Should be called once one variable of type "mpz_t" exists |
is_printf [Functions.Libc] | Return |
is_printf_name [Functions.Libc] | Same as |
is_rtl_name [Functions.RTL] | |
is_t [Gmpz] | is the type equal to "mpz_t"? |
is_vla_alloc [Functions.Libc] | Return |
is_vla_alloc_name [Functions.Libc] | Same as |
is_vla_free [Functions.Libc] | Return |
is_vla_free_name [Functions.Libc] | Return |
iter [State_builder.Hashtbl] | |
iter_sorted [State_builder.Hashtbl] | |
J | |
join [Typing] |
|
L | |
length [State_builder.Hashtbl] | Length of the table. |
library_files [Misc] | |
M | |
main [Main] | |
mem [State_builder.Hashtbl] | |
mem [Builtins] | |
mem [Parameter_sig.Set] | Does the given element belong to the set? |
memo [State_builder.Hashtbl] | Memoization. |
mk_api_name [Functions.RTL] | Prefix a name (of a variable or a function) with a string that identifies it as belonging to the public API of E-ACSL runtime library |
mk_block [Misc] | |
mk_call [Misc] | Call an E-ACSL library function or an E-ACSL built-in. |
mk_delete_stmt [Misc] | |
mk_deref [Misc] | Make a dereference of an expression |
mk_duplicate_store_stmt [Misc] | |
mk_e_acsl_guard [Misc] | |
mk_full_init_stmt [Misc] | |
mk_gen_name [Functions.RTL] | Prefix a name (of a variable or a function) with a string indicating that this name has been generated during instrumentation phase. |
mk_initialize [Misc] | |
mk_mark_readonly [Misc] | |
mk_store_stmt [Misc] | |
mk_temporal_name [Functions.RTL] | Prefix a name (of a variable or a function) with a string that identifies it as belonging to the public API of E-ACSL runtime library dealing with temporal analysis. |
move [Label] | Move all labels of the |
must_model_exp [Mmodel_analysis] | Same as |
must_model_lval [Mmodel_analysis] | Same as |
must_model_vi [Mmodel_analysis] |
|
must_translate [Keep_status] | To be called just before transforming a property of the given kind for the given function. |
must_visit [Options] | |
mv_invariants [Loops] | Transfer the loop invariants from the |
N | |
nb_not_yet [Error] | Number of not-yet-supported annotations. |
nb_untypable [Error] | Number of untypable annotations. |
new_labeled_stmt [Label] | |
new_var [Env] |
|
new_var_and_mpz_init [Env] | Same as |
not_yet [Error] | Not_yet_implemented error built from the given argument. |
O | |
off [Parameter_sig.Bool] | Set the boolean to |
on [Parameter_sig.Bool] | Set the boolean to |
other [Typing] | |
P | |
parameter_states [Options] | |
pop [Env] | Pop the last local context (ignore the corresponding new block if any |
pop_and_get [Env] | Pop the last local context and get back the corresponding new block
containing the given |
pop_loop [Env] | |
predicate_to_exp [Main] | |
predicate_to_exp [Translate] | |
predicate_to_exp_ref [Quantif] | |
prepare [Prepare_ast] | |
preserve_invariant [Loops] | modify the given stmt loop to insert the code which preserves its loop invarariants. |
pretty [Typing] | |
pretty [Env] | |
printf_fmt_position [Functions.Libc] | Given the name of a printf-like function (as determined by
|
ptr_index [Misc] | Split pointer-arithmetic expression of the type `p + i` into its pointer and integer parts. |
push [Keep_status] | store the given property of the given kind for the given function |
push [Env] | Push a new local context in the environment |
push_loop [Env] | |
Q | |
quantif_to_exp [Quantif] | The given predicate must be a quantification. |
R | |
register_library_function [Misc] | |
remove [State_builder.Hashtbl] | |
remove [Interval.Env] | |
remove [Env.Logic_binding] | |
reorder_ast [Misc] | |
replace [State_builder.Hashtbl] | Add a new binding. |
reset [Mmodel_analysis] | Must be called to redo the analysis |
reset [Literal_strings] | Must be called to redo the analysis |
reset [Misc] | |
restore [Env.Context] | |
result_lhost [Misc] | |
result_vi [Misc] | |
rte [Env] | |
S | |
save [Env.Context] | |
self [Label] | Internal state |
set_annotation_kind [Env] | |
set_original_project [Translate] | |
set_possible_values [Parameter_sig.String] | Set what are the acceptable values for this parameter. |
set_t [Gmpz] | |
stmt [Rte] | RTEs of a given stmt, as a list of code annotations. |
store_vars [Exit_points] | Compute variables that should be re-recorded before a labelled statement to which some goto jumps |
T | |
t [Gmpz] | type "mpz_t" |
term_addr_of [Misc] | |
term_of_li [Misc] | |
term_to_exp [Translate] | |
term_to_exp [E_ACSL.Translate] | |
term_to_exp_ref [Quantif] | |
transfer [Env] | Pop the last local context of |
translate_named_predicate [Translate] | |
translate_post_code_annotation [Translate] | |
translate_post_spec [Translate] | |
translate_pre_code_annotation [Translate] | |
translate_pre_spec [Translate] | |
translate_rte_annots [Translate] | |
typ_of_integer_ty [Typing] | |
type_named_predicate [Typing] | Compute the type of each term of the given predicate. |
type_term [Typing] | Compute the type of each subterm of the given term in the given context. |
U | |
unmemoized_extend_ast [Main] | |
unsafe_set [Typing] | Register that the given term has the given type in the given context (if any). |
untypable [Error] | Type error built from the given argument. |
update [Builtins] | If the given name is an E-ACSL built-in, change its old varinfo by the given new one. |
use_model [Mmodel_analysis] | Is one variable monitored (at least)? |
V | |
version [Local_config] |