Index of values

_debug [Labels]

Print internal state of labels translation.

A
actual_alloca [Functions.Libc]

The name of an actual alloca function used at link-time.

add [Global_observer]

Observe the given variable if necessary.

add [Env.Local_vars]
add [Env.Logic_binding]
add [Literal_strings]
add [Interval.Env]
add [Lscope]
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 [Typed_number]

add_cast ~loc ?name env kf ctx sty t_opt e convert number expression e in a way that it is compatible with the given typing context ctx.

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

Adds an optional additional guard condition that comes from the typing

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]
api_prefix [Functions.RTL]

Prefix used for the public API of E-ACSL runtime library.

app_to_exp [Logic_functions]

Translate a Tapp term or a Papp predicate to an expression.

assigns [Smart_stmt]

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

assigns_field [Smart_stmt]

assigns_field ~loc vi field value creates a statement to assign the value expression to the field of the structure in the variable vi.

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

bound_variables [Options.Dkey]
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]
case_globals [E_acsl_visitor]

Function to descend into the root of the ast according to the various cases relevant for E-ACSL.

cast_to_z [Rational]

Assumes that the given exp is of real type and casts it into Z

check [Functions]
clean [Assert]

clean ~loc env adata generates a call to the C cleanup function for the assertion context.

clear [Gmp]

build stmt mpz_clear(v) or mpq_clear(v) depending on typ of v

clear [Exit_points]

Clear all gathered data

clear [Typing]

Remove all the previously computed types.

clear [Interval.Env]
clear [Logic_normalizer]

clear the table of normalized predicates

clear_guards [Bound_variables]

Clear the table of guard conditions for quantified variables

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

comparison_to_exp ~data ~loc kf env ity ?e1 ?name bop t1 t2 topt generates the C code equivalent to t1 bop t2 in the given environment with the given assertion context.

comparison_to_exp [Logic_array]

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

conditional_to_exp [Translate_utils]

conditional_to_exp ?name ~loc kf t_opt e1 (e2, env2) (e3, env3) generates the C code equivalent to e1 ? e2 : e3 in the given environment.

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

create [Analyses_datatype.At_data]

create ?error kf kinstr lscope pot label creates an at_data from the given arguments.

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.

do_it [Translate_predicates]

Translate the given predicate to a runtime check in the given environment.

do_pending_register_data [Assert]

do_pending_register_data performs all the pending restrations

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

Empty assertion context.

empty [Env]
empty [Lscope]
enable [Temporal]

Enable/disable temporal transformations

env_of_li [Translate_utils]

env_of_li ~adata ~loc kf env li translates the logic info li in the given environment with the given assertion context.

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.

extended_interv_of_typ [Interval]
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 [Literal_strings]
find [Builtins]

Get the varinfo corresponding to the given E-ACSL built-in name.

find_all [Translate_ats.Free]
find_all [Translate_ats.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 [Literal_strings]
for_stmt [Translate_ats]

Translate all \at() predicates and terms for the given statement in the current environment.

found_concurrent_function [Memory_tracking]

found_concurrent_function ~loc fvi signals to the memory tracking sub-system that a concurrent function fvi has been found at loc while parsing the sources.

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

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

Returns the current value of RTE generation for the given environment

generic_handle [Error.S]

Run the closure with the given argument and handle potential errors.

get [Env.Local_vars]
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_assigns_from [Assigns]
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_first_inner_stmt [Labels]

If the given statement has a label, return the first statement of the block.

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_gmp_integer [Assigns]
get_guard_for_small_type [Bound_variables]
get_integer_op [Typing]
get_integer_op_of_predicate [Typing]
get_kinstr [Env]
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_pred [Logic_normalizer]

Retrieve the preprocessed form of a predicate

get_preprocessed_quantifier [Bound_variables]

Getters and setters

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

get_t ty returns Array if ty is an array type, StructOrUnion if ty is a struct or an union type and NotAggregate otherwise.

get_term [Logic_normalizer]

Retrieve the preprocessed form of a term

get_typ [Typing]

Get the type which the given term must be generated to.

gmp_to_sizet [Translate_utils]

Translate the given GMP integer to an expression of type size_t.

gmp_to_sizet_ref [Memory_translate]
gmpz [Typing]
H
handle [Error.S]

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_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_empty_quantif_ref [Labels]
has_fundef [Functions]
has_no_new_stmt [Env]

Assume that a local context has been previously pushed.

has_replacement [Functions.Concurrency]

Given the name of C library function return true if there is a drop-in replacement function for it in the RTL.

has_replacement [Functions.Libc]

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 creates 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]
interval [Options.Dkey]
is_bitfield_pointers [Misc]
is_empty [Global_observer]
is_empty [Literal_strings]
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_name [Functions.RTL]
is_generated_name [E_ACSL.Functions.RTL]
is_included [Interval]
is_libc_writing_memory_ref [Prepare_ast]
is_memcpy [Functions.Libc]

Return true if exp captures a function name that matches memcpy or an equivalent function

is_memset [Functions.Libc]

Return true if exp captures a function name that matches memset or an equivalent function

is_now_referenced [Gmp_types.S]

Call this function when using this type for the first time.

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_singleton_int [Interval]
is_t [Gmp_types.S]
is_t [Gmp_types]
is_used [Lscope]
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.

is_writing_memory [Libc]
J
join [Typing]

Typing.number_ty is a join-semi-lattice if you do not consider Other.

join [Interval]
L
labels [Options.Dkey]
link [Rtl]

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

lnot [Smart_exp]

lnot ~loc e creates a logical not on the given expression e.

logic_normalizer [Options.Dkey]
lval [Smart_exp]

Construct an lval expression from an lval.

M
make_not_memoized [Error.S]

Make a Not_memoized exception with the given message.

make_not_yet [Error.S]

Make a Not_yet exception with the given message.

make_type [Datatype.Hashtbl]
make_untypable [Error.S]

Make a Typing_error exception with the given message.

mark_readonly [Smart_stmt]

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

meet [Interval]
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]
merge_right [Assert]

merge_right ~loc env adata1 adata2 merges the assertion data of adata1 into adata2 if adata2 is not a "no data" assertion context.

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_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.

mtracking [Options.Dkey]
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_utils]
must_translate_opt [Translate_utils]

Same than must_translate but for Property.t option.

must_translate_ppt_opt_ref [E_acsl_visitor]
must_translate_ppt_ref [E_acsl_visitor]
must_visit [Options]
N
name_of_binop [Misc]
name_of_mpz_arith_bop [Gmp]

name_of_mpz_arith_bop bop returns the name of the GMP function on integer corresponding to the bop arithmetic operation.

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

no_data [Assert]

No data assertion context.

normalize_str [Rational]

Normalize the string so that it fits the representation used by the underlying real library.

not_memoized [Error.S]
not_yet [Env]

Save the current context and raise Error.Not_yet exception.

not_yet [Error.S]
null [Smart_exp]

null ~loc creates an expression to represent the NULL pointer.

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_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.

pp_result [Error.S]

pp_result pp where pp is a formatter for 'a returns a formatter for 'a result.

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_ref [Translate_ats]
predicate_to_exp_ref [Translate_utils]
predicate_to_exp_ref [Memory_translate]
predicate_to_exp_ref [Quantif]

Forward reference for Translate_predicates.to_exp.

predicate_to_exp_ref [Loops]
predicate_to_exp_ref [Logic_functions]
prepare [Prepare_ast]

Prepare the AST

prepare [Options.Dkey]
preprocess [Analyses]

Analyses to run before starting the translation

preprocess [Labels]

Analyse sources to find the statements where a labeled predicate or term should be translated.

preprocess [Bound_variables]

Preprocess all the quantified predicates in the ast and store the result in an hashtable

preprocess [Logic_normalizer]

Preprocess all the predicates of the ast and store the results

preprocess_annot [Bound_variables]

Preprocess the quantified predicate in a given code annotation

preprocess_annot [Logic_normalizer]

Preprocess of the predicate of a single code annotation and store the results

preprocess_predicate [Typing]

compute and store the types of all the terms in a given predicate

preprocess_predicate [Bound_variables]

Preprocess the quantified predicate in a given predicate

preprocess_predicate [Logic_normalizer]

Preprocess a predicate and its children and store the results

preprocess_rte [Typing]

compute and store the type of all the terms in a code annotation

pretty [Env]
print_not_yet [Error.S]

Print the "not yet supported" message without raising an exception.

ptr_base [Misc]

Takes an expression e and return base where base is the address p if e is of the form p + i and e otherwise.

ptr_base_and_base_addr [Misc]
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]
push_new [Env.Local_vars]
push_pending_register_data [Assert]

push_pending_register_data adds a data registration to a stack of pending data registration to be generated later

Q
quantif_to_exp [Quantif]

The given predicate must be a quantification.

R
rational [Typing]
register [Assert]

register ~loc env ?force name e adata registers the data e corresponding to the name name to the assertion context adata.

register_pred [Assert]

register_pred ~loc env ?force p e adata registers the data e corresponding to the predicate p to the assertion context adata.

register_pred_or_term [Assert]

register_pred_or_term ~loc kf env ?force pot e adata registers the data e corresponding to the predicate or term pot to the assertion context adata.

register_term [Assert]

register_term ~loc env ?force t e adata registers the data e corresponding to the term t to the assertion context adata.

remove [Env.Logic_scope]

Remove a logic variable and its associated information from the logic scope of the environment.

remove [Env.Logic_binding]
remove [Interval.Env]
remove [Lscope]
remove_all [Translate_ats.Free]

Remove all free stmts for kf from the internal table.

remove_all [Translate_ats.Malloc]

Remove all malloc stmts for kf from the internal table.

replace [Bound_variables]

Replace the computed guards.

replacement [Rtl.Symbols]

Given the varinfo of a C function with an RTL replacement, return the varinfo of the RTL function that replaces it.

replacement_name [Functions.Concurrency]

Given the name of C library function return the name of the RTL function that potentially replaces it.

replacement_name [Functions.Libc]

Given the name of C library function return the name of the RTL function that potentially replaces it.

reset [Global_observer]
reset [Translate_ats]

Clear the stored translations.

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

Clear the results of the analyses

reset [Memory_tracking]

Must be called to redo the analysis

reset [Literal_strings]

Must be called to redo the analysis

reset [Labels]

Reset the results of the pre-anlaysis.

result_lhost [Misc]
result_vi [Misc]
retrieve_preprocessing [Error.S]

Retrieve the result of a preprocessing phase, which possibly failed.

rte_annots [Translate_rtes]

Translate the given RTE annotations into runtime checks in the given environment.

rtl_call [Smart_stmt]

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

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

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

runtime_check_with_msg [Assert]

runtime_check_with_msg ~adata ~loc ?name msg ~pred_kind kind kf env e generates a runtime check for e (or !e if reverse is true) by building a call to __e_acsl_assert.

S
save [Env.Context]
set_annotation_kind [Env]
set_kinstr [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 reset.

set_rte [Env]

set_rte env x sets RTE generation to x for the given environment

setup [Options]

Verify and initialize the options of the current project according to the options set by the user.

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

struct_local_init [Smart_stmt]

struct_local_init ~loc vi fields creates a local initialization for the structure variable vi.

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

temporal_prefix [Functions.RTL]

Prefix used for the public API of E-ACSL runtime library dealing with temporal analysis.

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 [Translate_ats]
term_to_exp_ref [Translate_utils]
term_to_exp_ref [Memory_translate]
term_to_exp_ref [Loops]
term_to_exp_ref [Logic_functions]
to_exp [Translate_terms]

to_exp ~adata ?inplace kf env t converts an ACSL term into a corresponding C expression.

to_exp [Translate_ats]
top_loop_invariants [Env]
top_loop_variant [Env]
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_ref [Loops]
translate_rte_annots_ref [Translate_predicates]
translate_rte_exp_ref [Translate_predicates]
translate_rte_exp_ref [Translate_terms]
translate_rte_ref [Logic_array]
translation [Options.Dkey]
typ_of_lty [Typing]
typ_of_number_ty [Typing]
type_named_predicate [Typing]

Compute the type of each term of the given predicate.

type_program [Typing]

compute and store the type of all the terms that will be translated in a program

type_term [Typing]

Compute the type of each subterm of the given term in the given context.

typing [Options.Dkey]
U
unsafe_set [Typing]

Register that the given term has the given type in the given context (if any).

untypable [Error.S]
untyped_to_exp [Translate_predicates]

Convert an untyped ACSL predicate into a corresponding C expression.

untyped_to_exp [Translate_terms]

Convert an untyped ACSL term into a corresponding C expression.

untyped_to_exp [E_ACSL.Translate_predicates]
untyped_to_exp [E_ACSL.Translate_terms]
update [Builtins]

If the given name is an E-ACSL built-in, change its old varinfo by the given new one.

update_memory_model [Libc]

update_memory_model ~loc env kf ?result caller args generates code in env to update the memory model after executing the libc function caller with the given args.

use_monitoring [Memory_tracking]

Is one variable monitored (at least)?

V
version [Local_config]
W
widen [Interval]
with_data_from [Assert]

with_data_from ~loc kf env from creates a new assertion context with the same data than the from assertion context.

with_params [Env]

with_params ~rte ~kinstr ~f env executes the given closure with the given environment after having set RTE generation to rte and current kinstr to kinstr.

with_params_and_result [Env]

with_params_and_result ~rte ~kinstr ~f env executes the given closure with the given environment after having set RTE generation to rte and current kinstr to kinstr.