sig
module type Generator_sig =
sig
module Hashtbl : Datatype.Hashtbl
type override_key = Hashtbl.key
val function_name : string
val well_typed_call :
Cil_types.lval option ->
Cil_types.varinfo -> Cil_types.exp list -> bool
val key_from_call :
Cil_types.lval option ->
Cil_types.varinfo ->
Cil_types.exp list -> Instantiator_builder.Generator_sig.override_key
val retype_args :
Instantiator_builder.Generator_sig.override_key ->
Cil_types.exp list -> Cil_types.exp list
val args_for_original :
Instantiator_builder.Generator_sig.override_key ->
Cil_types.exp list -> Cil_types.exp list
val generate_prototype :
Instantiator_builder.Generator_sig.override_key ->
string * Cil_types.typ
val generate_spec :
Instantiator_builder.Generator_sig.override_key ->
Cil_types.location -> Cil_types.fundec -> Cil_types.funspec
end
module type Instantiator =
sig
module Enabled : Parameter_sig.Bool
type override_key
val function_name : string
val well_typed_call :
Cil_types.lval option ->
Cil_types.varinfo -> Cil_types.exp list -> bool
val key_from_call :
Cil_types.lval option ->
Cil_types.varinfo ->
Cil_types.exp list -> Instantiator_builder.Instantiator.override_key
val retype_args :
Instantiator_builder.Instantiator.override_key ->
Cil_types.exp list -> Cil_types.exp list
val get_override :
Instantiator_builder.Instantiator.override_key -> Cil_types.fundec
val get_kfs : unit -> Cil_types.kernel_function list
val clear : unit -> unit
end
module Make_instantiator : functor (G : Generator_sig) -> Instantiator
end