Index of values

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 key args must transform the list of parameters of the override function such that the new list can be given to the original function.

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

clear () clears the internal table of the instantiator.

Clears internal tables

For a type T, returns T const

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

Builds a term from a varinfo

Is there some element satisfying the given predicate?

Name of the implemented function

Same as Generator_sig.override_key

Name of the implemented instantiator function

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

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

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

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

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

get_logic_function name f searches for an existing logic function name.

get_logic_function_in_axiomatic name f searches for an existing logic function name.

get_override key returns the function generated for key.

get_variable name f searches for an existing variable name.

get_variable name f searches for an existing variable name.

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

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

Same as Generator_sig.override_key

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

Builds a behavior from its components.

Builds a funspec from a list of behaviors.

Does the given element belong to the set?

Set the boolean to false.

Set the boolean to true.

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

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

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

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

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

For a type T, returns T*

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 ~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 ~loc struct bytes_len pred.

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

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

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

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

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

Finds and returns size_t

string_of_typ t returns a name generated from the given t.

tdivide ~loc t1 t2 builds t1/t2

tminus ~loc t1 t2 builds t1-t2

tplus ~loc t1 t2 builds t1+t2

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.

Returns the type of pointed for a give logic_type

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

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

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

Same as Generator_sig.override_key

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.