Index of values

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 [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]
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]

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_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_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 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_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_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]
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_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_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 [Literal_strings]
is_enabled [Temporal]

Return a boolean value indicating whether temporal analysis is enabled

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_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 [Gmpz]

Should be called once one variable of type "mpz_t" exists

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_rtl_name [Functions.RTL]
is_t [Gmpz]

is the type equal to "mpz_t"?

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]
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 [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 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]
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.

on [Parameter_sig.Bool]

Set the boolean to true.

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 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]
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 [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 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]