module type Generator_sig =sig
..end
In order to support a new function, this module must be implemented and
registered to the Transform
module.
module Hashtbl:Datatype.Hashtbl
Hashtbl
module used by the Make_instantiator
module to generate the
function cache.
typeoverride_key =
Hashtbl.key
val function_name : string
val well_typed_call : Cil_types.lval option -> Cil_types.varinfo -> Cil_types.exp list -> bool
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.val key_from_call : Cil_types.lval option ->
Cil_types.varinfo ->
Cil_types.exp list ->
override_key
key_from_call ret fct args
must return an identifier for the
corresponding call. key_from_call ret1 fct1 args1
and
key_from_call ret2 fct2 args2
must equal if and only if the same
override function can be used for both call. Any call for which
well_typed_call
returns true must be able to give a key.val retype_args : override_key ->
Cil_types.exp list -> Cil_types.exp list
retype_args key args
must returns a new argument list compatible with
the function identified by override_key
. args
is the list of arguments
that were given to the call for with Transform
is currently replacing.
Most of the time, it will consists in removing/changing some casts. But
note that arguments can be removed (for example if the override is built
because some constant have specialized).val args_for_original : override_key ->
Cil_types.exp list -> Cil_types.exp list
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. For example, if for a call:
foo(x, 0, z)
The Instantiator
module generates an override:
void foo_spec(int p1, int p3);
The received list of expression is p1 ; p3
and thus the returned list
should be p1 ; 0 ; p3
(so that the replaced call foo_spec(x, z)
has
the same behavior).
Note that there is no need to introduce casts to the original type, it is
introduced by Make_instantiator
.val generate_prototype : override_key ->
string * Cil_types.typ
generate_prototype key
must generate the name and the type corresponding
to key
.val generate_spec : override_key ->
Cil_types.fundec -> Cil_types.location -> Cil_types.funspec
generate_spec key fundec loc
must generate the specification of the
fundec
generated from key
. The location is the one generated by the
Transform
visitor. Note that it must return a funspec
but should
not register it in Annotations
tables.