Frama-C API - Generator_sig
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 : Frama_c_kernel.Datatype.Hashtbl
Hashtbl
module used by the Make_instantiator
module to generate the function cache. The key
(override_key
) must identify a function override.
type override_key = Hashtbl.key
val well_typed_call : Frama_c_kernel.Cil_types.lval option -> Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.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 : Frama_c_kernel.Cil_types.lval option -> Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.exp list -> Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.exp list -> Frama_c_kernel.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 * Frama_c_kernel.Cil_types.typ
generate_prototype key
must generate the name and the type corresponding to key
.
val generate_spec : override_key -> Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.fundec -> Frama_c_kernel.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.