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 fundec loc must generate the specification of the fundec generated from key.
generate_spec [Instantiate.Instantiator_builder.Generator_sig]
generate_spec key fundec loc 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.