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 [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_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]
assigns [Smart_stmt]

assigns ~loc ~result value create a statement to assign the value expression to the result lval.

B
binop [Rational]

Applies binop to the given expressions.

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_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 mpz_clear(v) or mpq_clear(v) depending on typ of v

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.

comparison_to_exp [Logic_array]

comparison_to_exp ~loc kf env ~name bop e1 e2 generate the C code equivalent to e1 bop e2.

compute_quantif_guards_ref [Typing]

Forward reference.

copy [Datatype.S]

Deep copy: no possible sharing between x and copy x.

create [Contract]

Create a contract from a spec object (either function spec or statement spec)

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

Same as store_stmt for __e_acsl_delete_block that observes the de-allocation of the given varinfo.

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 store, with a call to __e_acsl_duplicate_store_block.

duplicate_store_stmt [Smart_stmt]

Same as store_stmt for __e_acsl_duplicate_store_block that first checks for a previous allocation of the given varinfo.

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]

extend_stmt_in_place env stmt ~label b modifies stmt in place in order to add the given block.

extract_ival [Interval]

assume Ival _ as argument

extract_uncoerced_lval [Misc]

Unroll the CastE part of the expression until an Lval is found, and return it.

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]

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

Same as store_stmt for __e_acsl_full_init that observes the initialization of the given varinfo.

function_clean_name [Global_observer]

Name of the function in which mk_clean_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
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 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_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_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_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_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
if_stmt [Smart_stmt]

if ~loc ~cond ~then_blk ~else_blk create an if statement with cond as condition and then_blk and else_blk as respectively "then" block and "else" block.

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

initialize [Smart_stmt]

Same as store_stmt for __e_acsl_initialize that observes the initialization of the given left-value.

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_array [Logic_array]
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_fc_stdlib_generated [Misc]

Returns true if the varinfo is a generated stdlib function.

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_generated_name [E_ACSL.Functions.RTL]
is_included [Interval]
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_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 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.

lib_call [Smart_stmt]

Construct a call to a library function with the given name.

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]

link prj links the RTL's AST contained in prj to the AST of the current project.

lval [Smart_exp]

Construct an lval expression from an lval.

M
main [Main]
make_type [Datatype.Hashtbl]
mark_readonly [Smart_stmt]

Same as store_stmt for __e_acsl_markreadonly that observes the read-onlyness of the given varinfo.

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.

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_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_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_monitor_exp [Memory_tracking]

Same as must_model_vi, for expressions

must_monitor_lval [Memory_tracking]

Same as must_model_vi, for left-values

must_monitor_vi [Memory_tracking]

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

Return true if the given property must be translated (ie.

must_translate_opt [Translate_annots]

Same than must_translate but for Property.t option.

must_translate_ppt_opt_ref [Contract]
must_translate_ppt_ref [Contract]
must_visit [Options]
N
name_of_binop [Misc]
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 [Env]

Save the current context and raise Error.Not_yet exception.

not_yet [Error]

Not_yet_implemented error built from the given argument.

number_ty_of_typ [Typing]

Reverse of typ_of_number_ty number_ty_of_typ ~post ty return the Typing.number_ty corresponding to a C type.

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_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 [Logic_functions]
predicate_to_exp_ref [Memory_translate]
predicate_to_exp_ref [At_with_lscope]
predicate_to_exp_ref [Quantif]
predicate_to_exp_ref [Loops]
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.

process_error [Error]

Process the given error.

ptr_base [Misc]
ptr_index [Misc]

Split pointer-arithmetic expression of the type p + i into its pointer and integer parts.

ptr_sizeof [Smart_exp]

ptr_sizeof ~loc ptr_typ takes the pointer typ ptr_typ that points to a typ typ and returns sizeof(typ).

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 set_reset _ true has been called beforehand.

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]

Special version of lib_call for E-ACSL's RTL functions.

rtl_call_to_new_var [Env]

rtl_call_to_new_var env t ty name args Same as new_var but initialize the variable with a call to the RTL function name with the given args.

runtime_check [Smart_stmt]

runtime_check kind kf e p generates a runtime check for predicate p by building a call to __e_acsl_assert.

runtime_check_with_msg [Smart_stmt]

runtime_check_with_msg kind kf e msg generates a runtime check for e (or !e if reverse is true) by building a call to __e_acsl_assert.

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 [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 __e_acsl_store_block in the given environment.

store_stmt [Smart_stmt]

Construct a call to __e_acsl_store_block that observes the allocation of the given varinfo.

store_vars [Exit_points]

Compute variables that should be re-recorded before a labelled statement to which some goto jumps.

subscript [Smart_exp]

mk_subscript ~loc array idx Create an expression to access the idx'th element of the array.

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_ref [Logic_functions]
term_to_exp_ref [Memory_translate]
term_to_exp_ref [At_with_lscope]
term_to_exp_ref [Loops]
to_exp [At_with_lscope]
top_contract [Env]

Return the top contract of the environment's stack

top_ival [Interval]
transfer [Env]

Pop the last local context of from and push it into the other env.

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 Error.Typing_error exception.

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

Call the function Eva.Value_parameters.use_builtin if Eva is enabled, do nothing otherwise.

use_monitoring [Memory_tracking]

Is one variable monitored (at least)?

V
version [Local_config]