Index of values

A
allocates_nothing [Basic_alloc]
allocates_result [Basic_alloc]
args_for_original [Instantiator_builder.Generator_sig]

args_for_original key args must transform the list of parameters of the override function such that the new list can be given to the original function.

args_for_original [Instantiate.Instantiator_builder.Generator_sig]

args_for_original key args must transform the list of parameters of the override function such that the new list can be given to the original function.

assigns_heap [Basic_alloc]
assigns_result [Basic_alloc]
C
call_function [Basic_blocks]

call_function ret_lval vi args creates an instruction (ret_lval = ) vi.vname(args).

category [Register]
clear [Instantiator_builder.Instantiator]

clear () clears the internal table of the instantiator.

clear [Global_context]

Clears internal tables

const_of [Basic_blocks]

For a type T, returns T const

copy [Datatype.S]

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

cvar_to_tvar [Basic_blocks]

Builds a term from a varinfo

E
emitter [Options]
exists [Parameter_sig.Set]

Is there some element satisfying the given predicate?

exp_type_of_pointed [Mem_utils]
F
fresh_result [Basic_alloc]
function_name [Instantiator_builder.Generator_sig]

Name of the implemented function

function_name [Instantiator_builder.Instantiator]

Same as Generator_sig.override_key

function_name [Instantiate.Instantiator_builder.Generator_sig]

Name of the implemented instantiator function

G
generate_function_type [Mem_utils.Make]
generate_prototype [Mem_utils.Make]
generate_prototype [Instantiator_builder.Generator_sig]

generate_prototype key must generate the name and the type corresponding to key.

generate_prototype [Instantiate.Instantiator_builder.Generator_sig]

generate_prototype key must generate the name and the type corresponding to key.

generate_spec [Instantiator_builder.Generator_sig]

generate_spec key loc fundec must generate the specification of the fundec generated from key.

generate_spec [Instantiate.Instantiator_builder.Generator_sig]

generate_spec key loc fundec must generate the specification of the fundec generated from key.

get_kfs [Instantiator_builder.Instantiator]

get_kfs () returns all generated kernel functions for the current project.

get_logic_function [Global_context]

get_logic_function name f searches for an existing logic function name.

get_logic_function_in_axiomatic [Global_context]

get_logic_function_in_axiomatic name f searches for an existing logic function name.

get_override [Instantiator_builder.Instantiator]

get_override key returns the function generated for key.

get_variable [Global_context]

get_variable name f searches for an existing variable name.

get_variable [Instantiate.Global_context]

get_variable name f searches for an existing variable name.

globals [Global_context]

Creates a list of global for the elements that have been created

I
is_allocable [Basic_alloc]
isnt_allocable [Basic_alloc]
K
key_from_call [Mem_utils.Make]
key_from_call [Instantiator_builder.Generator_sig]

key_from_call ret fct args must return an identifier for the corresponding call.

key_from_call [Instantiator_builder.Instantiator]

Same as Generator_sig.override_key

key_from_call [Instantiate.Instantiator_builder.Generator_sig]

key_from_call ret fct args must return an identifier for the corresponding call.

M
make_behavior [Basic_blocks]

Builds a behavior from its components.

make_funspec [Basic_blocks]

Builds a funspec from a list of behaviors.

make_type [Datatype.Hashtbl]
mem [Parameter_sig.Set]

Does the given element belong to the set?

mem2s_spec [Mem_utils]
mem2s_typing [Mem_utils]
memcpy_memmove_common_assigns [Mem_utils]
memcpy_memmove_common_ensures [Mem_utils]
memcpy_memmove_common_requires [Mem_utils]
N
name [Mem_utils.Function]
null_result [Basic_alloc]
O
off [Parameter_sig.Bool]

Set the boolean to false.

on [Parameter_sig.Bool]

Set the boolean to true.

P
pbounds_incl_excl [Basic_blocks]

pbounds_incl_excl ~loc low v up builds low <= v < up.

pcorrect_len_bytes [Basic_blocks]

pcorrect_len_bytes ~loc ltyp bytes_len returns a predicate bytes_len % sizeof(ltyp) == 0.

plet_len_div_size [Basic_blocks]

plet_len_div_size ~loc ~name_ext ltyp bytes_len pred buils a predicate: \let name = bytes_len / sizeof(ltyp) ; < pred name > with name = "__fc_<name_ext>len".

prepare_definition [Basic_blocks]

Create a function definition from a name and a type vdefined is positionned to true, formals are registered to FormalsDecl

prototype [Mem_utils.Function]
pseparated_memories [Basic_blocks]

pseparated_memories ~loc p1 len1 p2 len2 returns a predicate: \separated(p1 + (0 .. len1), p2 + (0 .. len2)) Parameters: p1 and p2 must be of pointer type

ptr_of [Basic_blocks]

For a type T, returns T*

punfold_all_elems_eq [Basic_blocks]

punfold_all_elems_eq ~loc p1 p2 len builds a predicate: \forall integer j1 ; 0 <= j1 < len ==> p1[j1] == p2[j1]. If p1[j1] is itself an array, it recursively builds a predicate: \forall integer j2 ; 0 <= j2 < len_of_array ==> .... Parameters: p1 and p2 must be pointers to the same type

punfold_all_elems_pred [Basic_blocks]

punfold_all_elems_pred ~loc ptr len pred builds a predicate: \forall integer j ; 0 <= j1 < len ==> < pred (\*(ptr + j1)) >. If ptr[j1] is a compound type (array or structure), it recursively builds a predicate on each element (either by introducing a new \forall for arrays or a conjunction for structure fields).

punfold_flexible_struct_pred [Basic_blocks]

punfold_flexible_struct_pred ~loc struct bytes_len pred.

pvalid_len_bytes [Basic_blocks]

pvalid_len_bytes ~loc label ptr bytes_len generates a predicate \valid{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr)))). Parameters: ptr must be a term of pointer type.

pvalid_read_len_bytes [Basic_blocks]

pvalid_read_len_bytes ~loc label ptr bytes_len generates a predicate \valid_read{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr)))). Parameters: ptr must be a term of pointer type.

R
register [Transform]

Registers a new Instantiator to the visitor from the Generator_sig module.

register [Instantiate.Transform]

Registers a new Instantiator to the visitor from the Generator_sig module of this instantiator.

retype_args [Mem_utils.Make]
retype_args [Instantiator_builder.Generator_sig]

retype_args key args must returns a new argument list compatible with the function identified by override_key.

retype_args [Instantiator_builder.Instantiator]
retype_args [Instantiate.Instantiator_builder.Generator_sig]

retype_args key args must returns a new argument list compatible with the function identified by override_key.

S
size_t [Basic_blocks]

Finds and returns size_t

string_of_typ [Basic_blocks]

string_of_typ t returns a name generated from the given t.

T
tdivide [Basic_blocks]

tdivide ~loc t1 t2 builds t1/t2

tminus [Basic_blocks]

tminus ~loc t1 t2 builds t1-t2

tplus [Basic_blocks]

tplus ~loc t1 t2 builds t1+t2

transform [Transform]

In all selected functions of the given file, for all function call, if there exists a instantiator module for this function, and the call is well-typed, replaces it with a call to the generated override function and inserted the generated function in the AST.

ttype_of_pointed [Basic_blocks]

Returns the type of pointed for a give logic_type

tunref_range [Basic_blocks]

tunref_range ~loc ptr len builds *(ptr + (0 .. len-1))

tunref_range_bytes_len [Basic_blocks]

tunref_range ~loc ptr bytes_len same as tunref_range except that length is provided in bytes.

V
valid_size [Basic_alloc]
W
well_typed [Mem_utils.Function]

receives the type of the lvalue and the types of the arguments received for a call to the function and returns true iff they are correct.

well_typed_call [Mem_utils.Make]
well_typed_call [Instantiator_builder.Generator_sig]

well_typed_call ret fct args must return true if and only if the corresponding call is well typed in the sens that the generator can produce a function override for the corresponding return value and parameters, according to their types and/or values.

well_typed_call [Instantiator_builder.Instantiator]

Same as Generator_sig.override_key

well_typed_call [Instantiate.Instantiator_builder.Generator_sig]

well_typed_call ret fct args must return true if and only if the corresponding call is well typed in the sens that the generator can produce a function override for the corresponding return value and parameters, according to their types and/or values.