Module type Instantiator_builder.Generator_sig

module type Generator_sig = sig .. end

Signature for a new instantiator generator.

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.

type override_key = Hashtbl.key

val function_name : string

Name of the implemented function

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.location -> Cil_types.fundec -> Cil_types.funspec

generate_spec key loc fundec 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.