A | |
actual_alloca [Functions.Libc] |
The name of an actual
alloca function used at link-time.
|
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_assert env s p associates the assertion p to the statement s in
the environment env .
|
add_binding [Env.Logic_binding] | |
add_cast [Rational] |
Assumes that the given exp is of real type and casts it into
the given typ
|
add_e_acsl_library [Main] | |
add_generated_functions [Logic_functions] | |
add_initializer [Global_observer] |
Add the initializer for the given observed variable.
|
add_loop_invariant [Env] | |
add_stmt [Env] | add_stmt env s extends env with the new statement s .
|
affect [Gmp] | affect x_as_lv x_as_exp e builds stmt x = e or mpz_set*(e)
or mpq_set*(e) with the good function 'set'
according to the type of e
|
annotation_kind [Env] | |
apply_on_e_acsl_ast [Main] | |
B | |
before_translation [Keep_status] |
to be called just before injecting the code
|
binop [Rational] |
Applies
binop to the given expressions.
|
C | |
c_int [Typing] | |
call [Mmodel_translate] | |
call_valid [Mmodel_translate] | |
call_with_size [Mmodel_translate] | |
cast_to_z [Rational] |
Assumes that the given exp is of real type and casts it into Z
|
change_printer [Main] | |
check [Main] | |
check [Functions] | |
clear [State_builder.Hashtbl] |
Clear the table.
|
clear [Gmp] |
build stmt
mpz_clear(v) or mpq_clear(v) depending on typ of v
|
clear [Keep_status] |
to be called before any program transformation
|
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
binop .
|
compute_quantif_guards_ref [Typing] |
Forward reference.
|
copy [Datatype.S] |
Deep copy: no possible sharing between
x and copy x .
|
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
store , with a call to __e_acsl_delete_block .
|
delete_from_set [Memory_observer] |
Same as
delete_from_list with a set of variables instead of a list.
|
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_prepare [Options] | |
dkey_translation [Options] | |
dkey_typing [Options] | |
duplicate_store [Memory_observer] |
Same as
store , with a call to __e_acsl_duplicate_store_block .
|
E | |
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_ast [Main] | |
extend_stmt_in_place [Env] | extend_stmt_in_place env stmt ~label b modifies stmt in place in
order to add the given block .
|
extended_ast_project [Main] | |
extract_ival [Interval] |
assume
Ival _ as argument
|
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] | |
finite_min_and_max [Misc] | finite_min_and_max i takes the finite ival i and returns its bounds.
|
fkind [Typing] | |
fold [State_builder.Hashtbl] | |
fold [Literal_strings] | |
fold_sorted [State_builder.Hashtbl] | |
function_delete_name [Global_observer] |
Name of the function in which
mk_delete_function (see below) generates the
code.
|
function_init_name [Global_observer] |
Name of the function in which
mk_init_function (see below) generates the
code.
|
G | |
generate [Exit_points] |
Visit a function and populate data structures used to compute exit points
|
generate_code [Main] | |
generate_global_init [Temporal] |
Generate
Some s , where s is a statement tracking global initializer
or None if there is no need to track it
|
generate_rte [Env] | |
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_cast [Typing] |
Get the type which the given term must be converted to (if any).
|
get_cast_of_predicate [Typing] |
Like
Typing.get_cast , but for predicates.
|
get_function_name [Parameter_sig.String] |
returns the given argument only if it is a valid function name
(see
Parameter_customize.get_c_ified_functions for more information),
and abort otherwise.
|
get_generated_variables [Env] |
All the new variables local to the visited function.
|
get_integer_op [Typing] | |
get_integer_op_of_predicate [Typing] | |
get_lib_fun_vi [Misc] | |
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
reset .
|
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.
|
gmpz [Typing] | |
H | |
handle [Error] |
Run the closure with the given argument and handle potential errors.
|
handle_function_parameters [Temporal] | handle_function_parameters kf env updates the local environment env ,
according to the parameters of kf , with statements allowing to track
referent numbers across function calls.
|
handle_stmt [Temporal] |
Update local environment (
Env.t ) with statements tracking temporal
properties of memory blocks
|
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] | |
ikind_of_ival [Interval] | |
infer [Interval] | infer t infers the smallest possible integer interval which the values
of the term can fit in.
|
init [Gmp] |
build stmt
mpz_init(v) or mpq_init(v) depending on typ of v
|
init [Gmp_types] |
Must be called before any use of GMP
|
init_set [Rational] | init_set lval lval_as_exp exp sets lval to exp while guranteeing that
lval is properly initialized wrt the underlying real library.
|
init_set [Gmp] | init_set x_as_lv x_as_exp e builds stmt x = e or mpz_init_set*(v, e)
or mpq_init_set*(v, e) with the good function 'set'
according to the type of e
|
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
true if exp captures a function name that matches
a function that allocates memory on stack.
|
is_alloca_name [Functions.Libc] |
Same as
is_alloca but for strings
|
is_bitfield_pointers [Misc] | |
is_dyn_alloc [Functions.Libc] |
Return
true if exp captures a function name that matches a function
that dynamically allocates memory such as malloc or calloc
|
is_dyn_alloc_name [Functions.Libc] |
Same as
is_dyn_alloc but for strings
|
is_dyn_free [Functions.Libc] |
Return
true if exp captures a function name that matches
a function that dynamically deallocates memory (e.g., free )
|
is_dyn_free_name [Functions.Libc] |
Same as
is_dyn_free but for strings
|
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_generated_kf [Functions.RTL] |
Same as
is_generated_name but for kernel functions
|
is_generated_literal_string_name [Functions.RTL] |
Same as
is_generated_name but indicates that the name represents a local
variable that replaced a literal string.
|
is_generated_name [Functions.RTL] | |
is_included [Interval] | |
is_library_loc [Misc] | |
is_memcpy [Functions.Libc] |
Return
true if exp captures a function name that matches memcpy or
an equivalent function
|
is_memcpy_name [Functions.Libc] |
Same as
is_memcpy but for strings
|
is_memset [Functions.Libc] |
Return
true if exp captures a function name that matches memset or
an equivalent function
|
is_memset_name [Functions.Libc] |
Same as
is_memset but for strings
|
is_now_referenced [Gmp_types.S] |
Call this function when using this type for the first time.
|
is_printf [Functions.Libc] |
Return
true if exp captures a function name that matches
a printf-like function such as printf , fprintf , dprintf etc.
|
is_printf_name [Functions.Libc] |
Same as
is_printf but for strings
|
is_range_free [Misc] | |
is_rtl_name [Functions.RTL] | |
is_set_of_ptr_or_array [Misc] |
Checks whether the given logic type is a set of pointers.
|
is_t [Gmp_types.S] | |
is_used [Lscope] | |
is_vla_alloc [Functions.Libc] |
Return
true if exp captures a function name that matches
a function that deallocates memory for a variable-size array.
|
is_vla_alloc_name [Functions.Libc] |
Same as
is_dyn_alloc but for strings
|
is_vla_free [Functions.Libc] |
Return
true if exp captures a function name that matches
a function that allocates memory for a variable-size array.
|
is_vla_free_name [Functions.Libc] |
Return
true if string captures a function name that matches
a function that deallocates memory for a variable-size array.
|
iter [State_builder.Hashtbl] | |
iter_sorted [State_builder.Hashtbl] | |
ival [Interval] | |
J | |
join [Typing] | Typing.number_ty is a join-semi-lattice if you do not consider Other .
|
join [Interval] | |
L | |
length [State_builder.Hashtbl] |
Length of the table.
|
library_files [Misc] | |
M | |
main [Main] | |
make_type [Datatype.Hashtbl] | |
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 [Constructor] |
Create a block statement from a block to replace a given statement.
|
mk_delete_function [Global_observer] |
Generate a new C function containing the observers for global variable
de-allocations.
|
mk_delete_stmt [Constructor] |
Same as
mk_store_stmt for __e_acsl_delete_block that observes the
de-allocation of the given varinfo.
|
mk_deref [Constructor] |
Construct a dereference of an expression.
|
mk_duplicate_store_stmt [Constructor] |
Same as
mk_store_stmt for __e_acsl_duplicate_store_block that first
checks for a previous allocation of the given varinfo.
|
mk_full_init_stmt [Constructor] |
Same as
mk_store_stmt for __e_acsl_full_init that observes the
initialization of the given varinfo.
|
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_initialize [Constructor] |
Same as
mk_store_stmt for __e_acsl_initialize that observes the
initialization of the given left-value.
|
mk_lib_call [Constructor] |
Construct a call to a library function with the given name.
|
mk_mark_readonly [Constructor] |
Same as
mk_store_stmt for __e_acsl_markreadonly that observes the
read-onlyness of the given varinfo.
|
mk_nested_loops [Loops] | mk_nested_loops ~loc mk_innermost_block kf env lvars creates nested
loops (with the proper statements for initializing the loop counters)
from the list of logic variables lvars .
|
mk_ptr_sizeof [Misc] | mk_ptr_sizeof ptr_typ loc takes the pointer typ ptr_typ that points
to a typ typ and returns sizeof(typ) .
|
mk_rtl_call [Constructor] |
Special version of
mk_lib_call for E-ACSL's RTL functions.
|
mk_runtime_check [Constructor] | mk_runtime_check kind kf e p generates a runtime check for predicate p
by building a call to __e_acsl_assert .
|
mk_store_stmt [Constructor] |
Construct a call to
__e_acsl_store_block that observes the allocation of
the given varinfo.
|
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
old stmt onto the new stmt .
|
must_model_exp [Mmodel_analysis] |
Same as
Mmodel_analysis.must_model_vi , for expressions
|
must_model_lval [Mmodel_analysis] |
Same as
Mmodel_analysis.must_model_vi , for left-values
|
must_model_vi [Mmodel_analysis] | must_model_vi ?kf ?stmt vi returns true if the varinfo vi at the given
stmt in the given function kf must be tracked by the memory model
library.
|
must_translate [Keep_status] |
To be called just before transforming a property of the given kind for the
given function.
|
must_visit [Options] | |
N | |
name_of_binop [Misc] | |
named_predicate_ref [Loops] | |
named_predicate_to_exp_ref [Logic_functions] | |
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 env t ty mk_stmts extends env with a fresh variable of type
ty corresponding to t .
|
new_var_and_mpz_init [Env] |
Same as
new_var , but dedicated to mpz_t variables initialized by
Mpz.init .
|
normalize_str [Rational] |
Normalize the string so that it fits the representation used by the
underlying real library.
|
not_yet [Error] |
Not_yet_implemented error built from the given argument.
|
number_ty_of_typ [Typing] |
Reverse of
typ_of_number_ty
|
O | |
off [Parameter_sig.Bool] |
Set the boolean to
false .
|
on [Parameter_sig.Bool] |
Set the boolean to
true .
|
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
stmt at the given place (Before is before the code
corresponding to annotations, After is after this code and Middle is
between the stmt corresponding to annotations and the ones for freeing the
memory.
|
pop_loop [Env] | |
predicate_to_exp [Main] | |
predicate_to_exp [Translate] | |
predicate_to_exp_ref [Mmodel_translate] | |
predicate_to_exp_ref [At_with_lscope] | |
predicate_to_exp_ref [Quantif] | |
prepare [Prepare_ast] | |
preserve_invariant [Loops] |
Modify the given stmt loop to insert the code which preserves its loop
invariants.
|
pretty [Env] | |
printf_fmt_position [Functions.Libc] |
Given the name of a printf-like function (as determined by
is_printf_name ) return the number of arguments preceding its variadic
arguments.
|
ptr_index [Misc] |
Split pointer-arithmetic expression of the type `p + i` into its
pointer and integer parts.
|
push [Env] |
Push a new local context in the environment
|
push [Keep_status] |
store the given property of the given kind for the given function
|
push_loop [Env] | |
Q | |
quantif_to_exp [Quantif] |
The given predicate must be a quantification.
|
R | |
rational [Typing] | |
register_library_function [Misc] | |
remove [State_builder.Hashtbl] | |
remove [Env.Logic_binding] | |
remove [Interval.Env] | |
remove_all [At_with_lscope.Free] | |
remove_all [At_with_lscope.Malloc] | |
reorder_ast [Misc] | |
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
set_reset _ true has been called beforehand.
|
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_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
reset .
|
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 mmodel
analysis, add a call to
__e_acsl_store_block in the given environment.
|
store_vars [Exit_points] |
Compute variables that should be re-recorded before a labelled statement to
which some goto jumps.
|
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
t but seen as a pointer
|
tapp_to_exp [Logic_functions] | |
term_addr_of [Misc] | |
term_has_lv_from_vi [Misc] | |
term_of_li [Misc] | term_of_li li assumes that li.l_body matches LBterm t
and returns t .
|
term_to_exp [Translate] | |
term_to_exp [E_ACSL.Translate] | |
term_to_exp_ref [Logic_functions] | |
term_to_exp_ref [Mmodel_translate] | |
term_to_exp_ref [At_with_lscope] | |
term_to_exp_ref [Loops] | |
to_exp [At_with_lscope] | |
top_ival [Interval] | |
transfer [Env] |
Pop the last local context of
from and push it into the other env.
|
translate_named_predicate [Translate] | |
translate_named_predicate_ref [Loops] | |
translate_post_code_annotation [Translate] | |
translate_post_spec [Translate] | |
translate_pre_code_annotation [Translate] | |
translate_pre_spec [Translate] | |
translate_rte_annots [Translate] | |
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 | |
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] |