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