A | |
add [State_builder.Hashtbl] |
Add a new binding.
|
add [Interval.Env] | |
add [Env.Logic_binding] | |
add [Literal_strings] | |
add_assert [Env] | add_assert env s p associates the assertion p to the statement s in
the environment env .
|
add_e_acsl_library [Main] | |
add_loop_invariant [Env] | |
add_stmt [Env] | add_stmt env s extends env with the new statement s .
|
affect [Gmpz] | affect x_as_lv x_as_exp e builds stmt x = e or mpz_set*(e) with the
good function 'set' according to the type of e
|
annotation_kind [Env] | |
apply_after_transformation [Loops] | |
apply_on_e_acsl_ast [Main] | |
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 [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] | |
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] | extend_stmt_in_place env stmt ~pre b modifies stmt in place in order to
add the given block .
|
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_rte [Env] | |
generic_handle [Error] |
Run the closure with the given argument and handle potential errors.
|
get [Env.Logic_binding] | |
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
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_integer_ty [Typing] | |
get_op [Typing] |
Get the type which the operation on top of the given term must be generated
to.
|
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_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.
|
has_no_new_stmt [Env] |
Assume that a local context has been previously pushed.
|
I | |
ikind [Typing] | |
infer [Interval] | infer t infers the smallest possible integer interval which the values
of the term can fit in.
|
init [Gmpz] |
build stmt "mpz_init(v)"
|
init_set [Gmpz] | init_set x_as_lv x_as_exp e builds stmt x = e or mpz_init_set*(v, e)
with the good function 'set' according to the type of e
|
init_t [Gmpz] |
Must be called before any use of GMP
|
interv_of_typ [Interval] | |
is_empty [Literal_strings] | |
is_generated [Dup_functions] | |
is_generated_kf [Misc] |
Same as
is_generated_varinfo but for kernel functions
|
is_generated_literal_string_varinfo [Misc] |
Same as
is_generated_varinfo but indicates that varinfo is a local
variable which replaced a literal string.
|
is_generated_varinfo [Misc] | |
is_library_loc [Misc] | |
is_now_referenced [Gmpz] |
Should be called once one variable of type "mpz_t" exists
|
is_t [Gmpz] |
is the type equal to "mpz_t"?
|
iter [State_builder.Hashtbl] | |
iter_sorted [State_builder.Hashtbl] | |
J | |
join [Typing] | Typing.integer_ty is a join-semi-lattice if you do not consider Other .
|
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 [Misc] | |
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 [Misc] | |
mk_initialize [Misc] | |
mk_mark_readonly [Misc] | |
mk_store_stmt [Misc] | |
move [Label] |
Move all labels of the
old stmt onto the new stmt .
|
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_visit [Options] | |
mv_invariants [Loops] |
Transfer the loop invariants from the
old loop to the new one.
|
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 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 .
|
not_yet [Error] |
Not_yet_implemented error built from the given argument.
|
O | |
off [Parameter_sig.Bool] |
Set the boolean to
false .
|
old_must_model_vi [Mmodel_analysis] |
Same as
Mmodel_analysis.must_model_vi , but assume that the given varinfo is part of the
new project generated by the given copy behavior.
|
on [Parameter_sig.Bool] |
Set the boolean to
true .
|
other [Typing] | |
P | |
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 [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] | |
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_loop [Env] | |
Q | |
quantif_to_exp [Quantif] |
The given predicate must be a quantification.
|
R | |
register_library_function [Misc] | |
remove [State_builder.Hashtbl] | |
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_to_exp [Translate] | |
term_to_exp [E_ACSL.Translate] | |
term_to_exp_ref [Quantif] | |
transfer [Env] |
Pop the last local context of
from and push it into the other env.
|
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] |