A | |
allocates_nothing [Basic_alloc] | |
allocates_result [Basic_alloc] | |
args_for_original [Instantiator_builder.Generator_sig] |
|
args_for_original [Instantiate.Instantiator_builder.Generator_sig] |
|
assigns_heap [Basic_alloc] | |
assigns_result [Basic_alloc] | |
C | |
call_function [Basic_blocks] |
|
clear [Instantiator_builder.Instantiator] |
|
clear [Global_context] | Clears internal tables |
const_of [Basic_blocks] | For a type |
copy [Datatype.S] | Deep copy: no possible sharing between |
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 |
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 [Instantiate.Instantiator_builder.Generator_sig] |
|
generate_spec [Instantiator_builder.Generator_sig] |
|
generate_spec [Instantiate.Instantiator_builder.Generator_sig] |
|
get_kfs [Instantiator_builder.Instantiator] |
|
get_logic_function [Global_context] |
|
get_logic_function_in_axiomatic [Global_context] |
|
get_override [Instantiator_builder.Instantiator] |
|
get_variable [Global_context] |
|
get_variable [Instantiate.Global_context] |
|
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 [Instantiator_builder.Instantiator] | Same as |
key_from_call [Instantiate.Instantiator_builder.Generator_sig] |
|
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 |
on [Parameter_sig.Bool] | Set the boolean to |
P | |
pbounds_incl_excl [Basic_blocks] |
|
pcorrect_len_bytes [Basic_blocks] |
|
plet_len_div_size [Basic_blocks] |
|
prepare_definition [Basic_blocks] | Create a function definition from a name and a type |
prototype [Mem_utils.Function] | |
pseparated_memories [Basic_blocks] |
|
ptr_of [Basic_blocks] | For a type |
punfold_all_elems_eq [Basic_blocks] |
|
punfold_all_elems_pred [Basic_blocks] |
|
punfold_flexible_struct_pred [Basic_blocks] |
|
pvalid_len_bytes [Basic_blocks] |
|
pvalid_read_len_bytes [Basic_blocks] |
|
R | |
register [Transform] | Registers a new |
register [Instantiate.Transform] | Registers a new |
retype_args [Mem_utils.Make] | |
retype_args [Instantiator_builder.Generator_sig] |
|
retype_args [Instantiator_builder.Instantiator] | |
retype_args [Instantiate.Instantiator_builder.Generator_sig] |
|
S | |
size_t [Basic_blocks] | Finds and returns |
string_of_typ [Basic_blocks] |
|
T | |
tdivide [Basic_blocks] |
|
tminus [Basic_blocks] |
|
tplus [Basic_blocks] |
|
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_bytes_len [Basic_blocks] |
|
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 |
well_typed_call [Mem_utils.Make] | |
well_typed_call [Instantiator_builder.Generator_sig] |
|
well_typed_call [Instantiator_builder.Instantiator] | Same as |
well_typed_call [Instantiate.Instantiator_builder.Generator_sig] |
|