_debug [Labels] | Print internal state of labels translation. |
A | |
actual_alloca [Functions.Libc] | The name of an actual |
add [Global_observer] | Observe the given variable if necessary. |
add [Env.Local_vars] | |
add [Env.Logic_binding] | |
add [Literal_strings] | |
add [Interval.Env] | |
add [Lscope] | |
add_assert [Env] |
|
add_binding [Env.Logic_binding] | |
add_cast [Typed_number] |
|
add_cast [Rational] | Assumes that the given exp is of real type and casts it into the given typ |
add_generated_functions [Logic_functions] | |
add_guard_for_small_type [Bound_variables] | Adds an optional additional guard condition that comes from the typing |
add_initializer [Global_observer] | Add the initializer for the given observed variable. |
add_loop_invariant [Env] | |
add_stmt [Env] |
|
affect [Gmp] |
|
annotation_kind [Env] | |
api_prefix [Functions.RTL] | Prefix used for the public API of E-ACSL runtime library. |
app_to_exp [Logic_functions] | Translate a Tapp term or a Papp predicate to an expression. |
assigns [Smart_stmt] |
|
assigns_field [Smart_stmt] |
|
at_for_stmt [Labels] | |
B | |
binop [Rational] | Applies |
bitcnt_t [Gmp_types] | |
block [Smart_stmt] | Create a block statement from a block to replace a given statement. |
block_from_stmts [Smart_stmt] | Create a block statement from a statement list. |
block_stmt [Smart_stmt] | Create a block statement from a block |
bound_variables [Options.Dkey] | |
break [Smart_stmt] | Create a break statement |
C | |
c_int [Typing] | |
call [Memory_translate] | |
call [Smart_stmt] | Construct a call to a function with the given name. |
call_valid [Memory_translate] | |
call_with_size [Memory_translate] | |
case_globals [E_acsl_visitor] | Function to descend into the root of the ast according to the various cases relevant for E-ACSL. |
cast_to_z [Rational] | Assumes that the given exp is of real type and casts it into Z |
check [Functions] | |
clean [Assert] |
|
clear [Gmp] | build stmt |
clear [Exit_points] | Clear all gathered data |
clear [Typing] | Remove all the previously computed types. |
clear [Interval.Env] | |
clear [Logic_normalizer] | clear the table of normalized predicates |
clear_guards [Bound_variables] | Clear the table of guard conditions for quantified variables |
clear_locals [Varname] | Reset the generator for variables that are local to a block or a function. |
cmp [Rational] | Compares two expressions according to the given |
comparison_to_exp [Translate_utils] |
|
comparison_to_exp [Logic_array] |
|
conditional_to_exp [Translate_utils] |
|
copy [Datatype.S] | Deep copy: no possible sharing between |
create [Contract] | Create a contract from a |
create [Rational] | Create a real |
create [Analyses_datatype.At_data] |
|
cty [Misc] | Assume that the logic type is indeed a C type. |
D | |
delete_from_list [Memory_observer] | Same as |
delete_from_set [Memory_observer] | Same as |
delete_stmt [Smart_stmt] | Same as |
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. |
deref [Smart_exp] | Construct a dereference of an expression. |
do_it [Translate_predicates] | Translate the given predicate to a runtime check in the given environment. |
do_pending_register_data [Assert] |
|
duplicate_store [Memory_observer] | Same as |
duplicate_store_stmt [Smart_stmt] | Same as |
E | |
emitter [Options] | |
empty [Assert] | Empty assertion context. |
empty [Env] | |
empty [Lscope] | |
enable [Temporal] | Enable/disable temporal transformations |
env_of_li [Translate_utils] |
|
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 [Env.Logic_scope] | Add a new logic variable with its associated information in the logic scope of the environment. |
extend_stmt_in_place [Env] |
|
extended_interv_of_typ [Interval] | |
extract_ival [Interval] | assume |
extract_uncoerced_lval [Misc] | Unroll the |
F | |
find [Literal_strings] | |
find [Builtins] | Get the varinfo corresponding to the given E-ACSL built-in name. |
find_all [Translate_ats.Free] | |
find_all [Translate_ats.Malloc] | |
find_vi [Rtl.Symbols] | |
finite_min_and_max [Misc] |
|
fkind [Typing] | |
fold [Literal_strings] | |
for_stmt [Translate_ats] | Translate all |
found_concurrent_function [Memory_tracking] |
|
full_init_stmt [Smart_stmt] | Same as |
function_clean_name [Global_observer] | Name of the function in which |
function_init_name [Global_observer] | Name of the function in which |
G | |
generalized_untyped_to_exp [Translate_predicates] | Convert an untyped ACSL predicate into a corresponding C expression. |
generate [Exit_points] | Visit a function and populate data structures used to compute exit points |
generate_global_init [Temporal] | Generate |
generate_rte [Env] | Returns the current value of RTE generation for the given environment |
generic_handle [Error.S] | Run the closure with the given argument and handle potential errors. |
get [Env.Local_vars] | |
get [Env.Logic_scope] | Return the logic scope associated to the environment. |
get [Env.Logic_binding] | |
get [Varname] | |
get_all [Lscope] | |
get_array_typ_opt [Logic_aggr] | |
get_assigns_from [Assigns] | |
get_cast [Typing] | Get the type which the given term must be converted to (if any). |
get_cast_of_predicate [Typing] | Like |
get_first_inner_stmt [Labels] | If the given statement has a label, return the first statement of the block. |
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_gmp_integer [Assigns] | |
get_guard_for_small_type [Bound_variables] | |
get_integer_op [Typing] | |
get_integer_op_of_predicate [Typing] | |
get_kinstr [Env] | |
get_number_ty [Typing] | |
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_pred [Logic_normalizer] | Retrieve the preprocessed form of a predicate |
get_preprocessed_quantifier [Bound_variables] | Getters and setters |
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_reset [Env.Logic_scope] | Getter of the information indicating whether the logic scope should be
reset at next call to |
get_t [Logic_aggr] |
|
get_term [Logic_normalizer] | Retrieve the preprocessed form of a term |
get_typ [Typing] | Get the type which the given term must be generated to. |
gmp_to_sizet [Translate_utils] | Translate the given GMP integer to an expression of type |
gmp_to_sizet_ref [Memory_translate] | |
gmpz [Typing] | |
H | |
handle [Error.S] | Run the closure with the given argument and handle potential errors. |
handle_annotations [Loops] | Modify the given stmt loop to insert the code which verifies the loop annotations, ie. |
handle_error [Env] | Run the closure with the given environment and handle potential errors. |
handle_error_with_args [Env] | Run the closure with the given environment and arguments and handle potential errors. |
handle_function_parameters [Temporal] |
|
handle_stmt [Temporal] | Update local environment ( |
has_empty_quantif_ref [Labels] | |
has_fundef [Functions] | |
has_no_new_stmt [Env] | Assume that a local context has been previously pushed. |
has_replacement [Functions.Concurrency] | Given the name of C library function return true if there is a drop-in replacement function for it in the RTL. |
has_replacement [Functions.Libc] | Given the name of C library function return true if there is a drop-in replacement function for it in the RTL. |
I | |
if_stmt [Smart_stmt] |
|
ikind [Typing] | |
ikind_of_ival [Interval] | |
infer [Interval] |
|
init [Gmp] | build stmt |
init [Gmp_types] | Must be called before any use of GMP |
init_set [Rational] |
|
init_set [Gmp] |
|
initialize [Smart_stmt] | Same as |
inject [Injector] | Inject all the necessary pieces of code for monitoring the program annotations. |
instrument [Functions] | |
interv_of_typ [Interval] | |
interval [Options.Dkey] | |
is_bitfield_pointers [Misc] | |
is_empty [Global_observer] | |
is_empty [Literal_strings] | |
is_fc_or_compiler_builtin [Misc] | |
is_fc_stdlib_generated [Misc] | Returns true if the |
is_generated_kf [Functions.RTL] | Same as |
is_generated_name [Functions.RTL] | |
is_generated_name [E_ACSL.Functions.RTL] | |
is_included [Interval] | |
is_libc_writing_memory_ref [Prepare_ast] | |
is_memcpy [Functions.Libc] | Return |
is_memset [Functions.Libc] | Return |
is_now_referenced [Gmp_types.S] | Call this function when using this type for the first time. |
is_printf_name [Functions.Libc] | Same as |
is_range_free [Misc] | |
is_set_of_ptr_or_array [Misc] | Checks whether the given logic type is a set of pointers. |
is_singleton_int [Interval] | |
is_t [Gmp_types.S] | |
is_t [Gmp_types] | |
is_used [Lscope] | |
is_vla_alloc_name [Functions.Libc] | Same as |
is_vla_free [Functions.Libc] | Return |
is_vla_free_name [Functions.Libc] | Return |
is_writing_memory [Libc] | |
J | |
join [Typing] |
|
join [Interval] | |
L | |
labels [Options.Dkey] | |
link [Rtl] |
|
lnot [Smart_exp] |
|
logic_normalizer [Options.Dkey] | |
lval [Smart_exp] | Construct an lval expression from an lval. |
M | |
make_not_memoized [Error.S] | Make a |
make_not_yet [Error.S] | Make a |
make_type [Datatype.Hashtbl] | |
make_untypable [Error.S] | Make a |
mark_readonly [Smart_stmt] | Same as |
meet [Interval] | |
mem [Builtins] | |
mem [Parameter_sig.Set] | Does the given element belong to the set? |
mem_global [Rtl.Symbols] | |
mem_kf [Rtl.Symbols] | |
mem_vi [Rtl.Symbols] | |
merge_right [Assert] |
|
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_clean_function [Global_observer] | Generate a new C function containing the observers for global variable de-allocations if there are global variables. |
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_init_function [Global_observer] | Generate a new C function containing the observers for global variable declarations and initializations. |
mk_nested_loops [Loops] |
|
mtracking [Options.Dkey] | |
must_monitor_exp [Memory_tracking] | Same as |
must_monitor_lval [Memory_tracking] | Same as |
must_monitor_vi [Memory_tracking] |
|
must_translate [Translate_utils] | |
must_translate_opt [Translate_utils] | Same than |
must_translate_ppt_opt_ref [E_acsl_visitor] | |
must_translate_ppt_ref [E_acsl_visitor] | |
must_visit [Options] | |
N | |
name_of_binop [Misc] | |
name_of_mpz_arith_bop [Gmp] |
|
nan [Typing] | |
nearest_elt_ge [Datatype.Set] | |
nearest_elt_le [Datatype.Set] | |
new_var [Env] |
|
new_var_and_mpz_init [Env] | Same as |
no_data [Assert] | No data assertion context. |
normalize_str [Rational] | Normalize the string so that it fits the representation used by the underlying real library. |
not_memoized [Error.S] | |
not_yet [Env] | Save the current context and raise |
not_yet [Error.S] | |
null [Smart_exp] |
|
number_ty_of_typ [Typing] | Reverse of |
O | |
off [Parameter_sig.Bool] | Set the boolean to |
on [Parameter_sig.Bool] | Set the boolean to |
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_and_get_contract [Env] | Pop and return the top contract of the environment's stack |
pop_loop [Env] | |
post_code_annotation [Translate_annots] | Translate the postconditions of the current code annotation in the environment. |
post_funspec [Translate_annots] | Translate the postconditions of the current function contract in the environment. |
pp_result [Error.S] |
|
pre_code_annotation [Translate_annots] | Translate the preconditions of the given code annotation in the environment. |
pre_funspec [Translate_annots] | Translate the preconditions of the given function contract in the environment. |
predicate_to_exp_ref [Translate_ats] | |
predicate_to_exp_ref [Translate_utils] | |
predicate_to_exp_ref [Memory_translate] | |
predicate_to_exp_ref [Quantif] | Forward reference for |
predicate_to_exp_ref [Loops] | |
predicate_to_exp_ref [Logic_functions] | |
prepare [Prepare_ast] | Prepare the AST |
prepare [Options.Dkey] | |
preprocess [Analyses] | Analyses to run before starting the translation |
preprocess [Labels] | Analyse sources to find the statements where a labeled predicate or term should be translated. |
preprocess [Bound_variables] | Preprocess all the quantified predicates in the ast and store the result in an hashtable |
preprocess [Logic_normalizer] | Preprocess all the predicates of the ast and store the results |
preprocess_annot [Bound_variables] | Preprocess the quantified predicate in a given code annotation |
preprocess_annot [Logic_normalizer] | Preprocess of the predicate of a single code annotation and store the results |
preprocess_predicate [Typing] | compute and store the types of all the terms in a given predicate |
preprocess_predicate [Bound_variables] | Preprocess the quantified predicate in a given predicate |
preprocess_predicate [Logic_normalizer] | Preprocess a predicate and its children and store the results |
preprocess_rte [Typing] | compute and store the type of all the terms in a code annotation |
pretty [Env] | |
print_not_yet [Error.S] | Print the "not yet supported" message without raising an exception. |
ptr_base [Misc] | Takes an expression |
ptr_base_and_base_addr [Misc] | |
ptr_sizeof [Smart_exp] |
|
push [Env] | Push a new local context in the environment |
push_contract [Env] | Push a contract to the environment's stack |
push_loop [Env] | |
push_new [Env.Local_vars] | |
push_pending_register_data [Assert] |
|
Q | |
quantif_to_exp [Quantif] | The given predicate must be a quantification. |
R | |
rational [Typing] | |
register [Assert] |
|
register_pred [Assert] |
|
register_pred_or_term [Assert] |
|
register_term [Assert] |
|
remove [Env.Logic_scope] | Remove a logic variable and its associated information from the logic scope of the environment. |
remove [Env.Logic_binding] | |
remove [Interval.Env] | |
remove [Lscope] | |
remove_all [Translate_ats.Free] | Remove all |
remove_all [Translate_ats.Malloc] | Remove all |
replace [Bound_variables] | Replace the computed guards. |
replacement [Rtl.Symbols] | Given the varinfo of a C function with an RTL replacement, return the varinfo of the RTL function that replaces it. |
replacement_name [Functions.Concurrency] | Given the name of C library function return the name of the RTL function that potentially replaces it. |
replacement_name [Functions.Libc] | Given the name of C library function return the name of the RTL function that potentially replaces it. |
reset [Global_observer] | |
reset [Translate_ats] | Clear the stored translations. |
reset [Logic_functions] | |
reset [Env.Logic_scope] | Return a new environment in which the logic scope is reset
iff |
reset [Analyses] | Clear the results of the analyses |
reset [Memory_tracking] | Must be called to redo the analysis |
reset [Literal_strings] | Must be called to redo the analysis |
reset [Labels] | Reset the results of the pre-anlaysis. |
result_lhost [Misc] | |
result_vi [Misc] | |
retrieve_preprocessing [Error.S] | Retrieve the result of a preprocessing phase, which possibly failed. |
rte_annots [Translate_rtes] | Translate the given RTE annotations into runtime checks in the given environment. |
rtl_call [Smart_stmt] | Construct a call to a library function with the given name. |
rtl_call_to_new_var [Env] |
|
runtime_check [Assert] |
|
runtime_check_with_msg [Assert] |
|
S | |
save [Env.Context] | |
set_annotation_kind [Env] | |
set_kinstr [Env] | |
set_loop_variant [Env] | |
set_possible_values [Parameter_sig.String] | Set what are the acceptable values for this parameter. |
set_reset [Env.Logic_scope] | Setter of the information indicating whether the logic scope should be
reset at next call to |
set_rte [Env] |
|
setup [Options] | Verify and initialize the options of the current project according to the options set by the user. |
sound_verdict [Prepare_ast] | |
stmt [Smart_stmt] | Create a statement from a statement kind. |
stmt [Rte] | RTEs of a given stmt, as a list of code annotations. |
store [Memory_observer] | For each variable of the given list, if necessary according to the mtracking
analysis, add a call to |
store_stmt [Smart_stmt] | Construct a call to |
store_vars [Exit_points] | Compute variables that should be re-recorded before a labelled statement to which some goto jumps. |
struct_local_init [Smart_stmt] |
|
subscript [Smart_exp] |
|
subst_all_literals_in_exp [Literal_observer] | Replace any sub-expression of the given exp that is a literal string by an observed variable. |
T | |
t [Gmp_types.S] | |
t_as_ptr [Gmp_types.S] | type equivalent to |
temporal_prefix [Functions.RTL] | Prefix used for the public API of E-ACSL runtime library dealing with temporal analysis. |
term_has_lv_from_vi [Misc] | |
term_of_li [Misc] |
|
term_to_exp_ref [Translate_ats] | |
term_to_exp_ref [Translate_utils] | |
term_to_exp_ref [Memory_translate] | |
term_to_exp_ref [Loops] | |
term_to_exp_ref [Logic_functions] | |
to_exp [Translate_terms] |
|
to_exp [Translate_ats] | |
top_loop_invariants [Env] | |
top_loop_variant [Env] | |
transfer [Env] | Pop the last local context of |
translate_postconditions [Contract] | Translate the postconditions of the given contract into the environment |
translate_preconditions [Contract] | Translate the preconditions of the given contract into the environement |
translate_predicate_ref [Loops] | |
translate_rte_annots_ref [Translate_predicates] | |
translate_rte_exp_ref [Translate_predicates] | |
translate_rte_exp_ref [Translate_terms] | |
translate_rte_ref [Logic_array] | |
translation [Options.Dkey] | |
typ_of_lty [Typing] | |
typ_of_number_ty [Typing] | |
type_named_predicate [Typing] | Compute the type of each term of the given predicate. |
type_program [Typing] | compute and store the type of all the terms that will be translated in a program |
type_term [Typing] | Compute the type of each subterm of the given term in the given context. |
typing [Options.Dkey] | |
U | |
unsafe_set [Typing] | Register that the given term has the given type in the given context (if any). |
untypable [Error.S] | |
untyped_to_exp [Translate_predicates] | Convert an untyped ACSL predicate into a corresponding C expression. |
untyped_to_exp [Translate_terms] | Convert an untyped ACSL term into a corresponding C expression. |
untyped_to_exp [E_ACSL.Translate_predicates] | |
untyped_to_exp [E_ACSL.Translate_terms] | |
update [Builtins] | If the given name is an E-ACSL built-in, change its old varinfo by the given new one. |
update_memory_model [Libc] |
|
use_monitoring [Memory_tracking] | Is one variable monitored (at least)? |
V | |
version [Local_config] | |
W | |
widen [Interval] | |
with_data_from [Assert] |
|
with_params [Env] |
|
with_params_and_result [Env] |
|