A | |
actual_alloca [Functions.Libc] | The name of an actual |
add [State_builder.Hashtbl] | Add a new binding. |
add [Global_observer] | Observe the given variable if necessary. |
add [Env.Logic_binding] | |
add [Interval.Env] | |
add [Lscope] | |
add [Literal_strings] | |
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_casts [Misc] |
|
add_generated_functions [Logic_functions] | |
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. |
assigns [Smart_stmt] |
|
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 |
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] | |
cast_to_z [Rational] | Assumes that the given exp is of real type and casts it into Z |
change_printer [Main] | |
check [Functions] | |
clear [State_builder.Hashtbl] | Clear the table. |
clear [Gmp] | build stmt |
clear [Typing] | Remove all the previously computed types. |
clear [Interval.Env] | |
clear [Exit_points] | Clear all gathered data |
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 [Logic_array] |
|
compute_quantif_guards_ref [Typing] | Forward reference. |
copy [Datatype.S] | Deep copy: no possible sharing between |
create [Contract] | Create a contract from a |
create [Rational] | Create a real |
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. |
dkey_analysis [Options] | |
dkey_prepare [Options] | |
dkey_translation [Options] | |
dkey_typing [Options] | |
duplicate_store [Memory_observer] | Same as |
duplicate_store_stmt [Smart_stmt] | Same as |
E | |
emitter [Options] | |
empty [Env] | |
empty [Lscope] | |
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 [Env.Logic_scope] | Add a new logic variable with its associated information in the logic scope of the environment. |
extend_stmt_in_place [Env] |
|
extract_ival [Interval] | assume |
extract_uncoerced_lval [Misc] | Unroll the |
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. |
find_all [At_with_lscope.Free] | |
find_all [At_with_lscope.Malloc] | |
find_vi [Rtl.Symbols] | |
finite_min_and_max [Misc] |
|
fkind [Typing] | |
fold [State_builder.Hashtbl] | |
fold [Literal_strings] | |
fold_sorted [State_builder.Hashtbl] | |
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_predicate_to_exp [Translate] | 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_code [Main] | |
generate_global_init [Temporal] | Generate |
generate_rte [Env] | Returns the current value of RTE generation for the given environment |
generic_handle [Error] | Run the closure with the given argument and handle potential errors. |
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_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_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_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_stmt [Label] | |
get_t [Logic_aggr] |
|
get_typ [Typing] | Get the type which the given term must be generated to. |
gmpz [Typing] | |
H | |
handle [Error] | 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_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 | |
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] | |
is_alloca [Functions.Libc] | Return |
is_alloca_name [Functions.Libc] | Same as |
is_bitfield_pointers [Misc] | |
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 [Global_observer] | |
is_empty [Lscope] | |
is_empty [Literal_strings] | |
is_enabled [Temporal] | Return a boolean value indicating whether temporal analysis is enabled |
is_fc_or_compiler_builtin [Misc] | |
is_fc_stdlib_generated [Misc] | Returns true if the |
is_generated_kf [Functions.RTL] | Same as |
is_generated_literal_string_name [Functions.RTL] | Same as |
is_generated_name [Functions.RTL] | |
is_generated_name [E_ACSL.Functions.RTL] | |
is_included [Interval] | |
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 [Gmp_types.S] | Call this function when using this type for the first time. |
is_printf [Functions.Libc] | Return |
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_t [Gmp_types.S] | |
is_t [Gmp_types] | |
is_used [Lscope] | |
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] | |
ival [Interval] | |
J | |
join [Typing] |
|
join [Interval] | |
L | |
length [State_builder.Hashtbl] | Length of the table. |
libc_replacement_name [Functions.RTL] | Given the name of C library function return the name of the RTL function that potentially replaces it. |
link [Rtl] |
|
lval [Smart_exp] | Construct an lval expression from an lval. |
M | |
main [Main] | |
make_type [Datatype.Hashtbl] | |
mark_readonly [Smart_stmt] | Same as |
mem [State_builder.Hashtbl] | |
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] | |
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_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] |
|
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_monitor_exp [Memory_tracking] | Same as |
must_monitor_lval [Memory_tracking] | Same as |
must_monitor_vi [Memory_tracking] |
|
must_translate [Translate_annots] | Return true if the given property must be translated (ie. |
must_translate_opt [Translate_annots] | Same than |
must_translate_ppt_opt_ref [Contract] | |
must_translate_ppt_ref [Contract] | |
must_visit [Options] | |
N | |
name_of_binop [Misc] | |
name_of_mpz_arith_bop [Gmp] |
|
nan [Typing] | |
nb_not_yet [Error] | Number of not-yet-supported annotations. |
nb_untypable [Error] | Number of untypable annotations. |
nearest_elt_ge [Datatype.Set] | |
nearest_elt_le [Datatype.Set] | |
new_var [Env] |
|
new_var_and_mpz_init [Env] | Same as |
normalize_str [Rational] | Normalize the string so that it fits the representation used by the underlying real library. |
not_yet [Env] | Save the current context and raise |
not_yet [Error] | Not_yet_implemented error built from the given argument. |
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_contract [Env] | Pop 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. |
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 [Translate] | Convert an ACSL predicate into a corresponding C expression. |
predicate_to_exp_ref [Memory_translate] | |
predicate_to_exp_ref [At_with_lscope] | |
predicate_to_exp_ref [Quantif] | Forward reference for |
predicate_to_exp_ref [Loops] | |
predicate_to_exp_ref [Logic_functions] | |
prepare [Prepare_ast] | |
pretty [Env] | |
print_not_yet [Error] | Print the "not yet" message without raising an exception. |
printf_fmt_position [Functions.Libc] | Given the name of a printf-like function (as determined by
|
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] | |
Q | |
quantif_to_exp [Quantif] | The given predicate must be a quantification. |
R | |
rational [Typing] | |
remove [State_builder.Hashtbl] | |
remove [Env.Logic_binding] | |
remove [Interval.Env] | |
remove_all [At_with_lscope.Free] | |
remove_all [At_with_lscope.Malloc] | |
replace [State_builder.Hashtbl] | Add a new binding. |
replace [Interval.Env] | |
reset [Global_observer] | |
reset [Logic_functions] | |
reset [Env.Logic_scope] | Return a new environment in which the logic scope is reset
iff |
reset [Memory_tracking] | Must be called to redo the analysis |
reset [Literal_strings] | Must be called to redo the analysis |
restore [Env.Context] | |
result_lhost [Misc] | |
result_vi [Misc] | |
rte [Env] |
|
rtl_call [Smart_stmt] | Construct a call to a library function with the given name. |
rtl_call_to_new_var [Env] |
|
runtime_check [Smart_stmt] |
|
runtime_check_with_msg [Smart_stmt] |
|
S | |
save [Env.Context] | |
self [Label] | Internal state |
set_annotation_kind [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 |
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. |
strip_casts [Misc] |
|
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 |
tapp_to_exp [Logic_functions] | Translate a Tapp term to an expression. |
temporal_prefix [Functions.RTL] | Prefix used for the public API of E-ACSL runtime library dealing with temporal analysis. |
term_addr_of [Misc] | |
term_has_lv_from_vi [Misc] | |
term_of_li [Misc] |
|
term_to_exp_ref [Memory_translate] | |
term_to_exp_ref [At_with_lscope] | |
term_to_exp_ref [Loops] | |
term_to_exp_ref [Logic_functions] | |
to_exp [At_with_lscope] | |
top_contract [Env] | Return the top contract of the environment's stack |
top_ival [Interval] | |
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 [Translate] | Translate the given predicate to a runtime check in the given environment. |
translate_predicate_ref [Loops] | |
translate_rte_annots [Translate] | Translate the given RTE annotations into runtime checks in the given environment. |
translate_rte_ref [Logic_array] | |
ty_of_interv [Typing] | Coercion rules |
typ_of_lty [Typing] | |
typ_of_number_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 | |
unsafe_set [Typing] | Register that the given term has the given type in the given context (if any). |
untypable [Env] | Save the current context and raise |
untypable [Error] | Type error built from the given argument. |
untyped_predicate_to_exp [Translate] | Convert an untyped ACSL predicate into a corresponding C expression. |
untyped_predicate_to_exp [E_ACSL.Translate] | |
untyped_term_to_exp [Translate] | Convert an untyped ACSL term into a corresponding C expression. |
untyped_term_to_exp [E_ACSL.Translate] | |
update [Builtins] | If the given name is an E-ACSL built-in, change its old varinfo by the given new one. |
use_monitoring [Memory_tracking] | Is one variable monitored (at least)? |
V | |
version [Local_config] | |
W | |
with_rte [Env] |
|
with_rte_and_result [Env] |
|