Module type Instantiator_builder.Instantiator

module type Instantiator = sig .. end

Signature of a instantiator.

Module built by the Transform module from a Generator_sig. Used to perform the different replacements in the AST. This should be only used by the Transform module.

module Enabled: Parameter_sig.Bool

Plugin option that allows to check whether the instantiator is enabled.

type override_key

Same as Generator_sig.override_key

val function_name : string

Same as Generator_sig.override_key

val well_typed_call : Cil_types.lval option -> Cil_types.varinfo -> Cil_types.exp list -> bool

Same as Generator_sig.override_key

val key_from_call : Cil_types.lval option ->
       Cil_types.varinfo ->
       Cil_types.exp list -> override_key

Same as Generator_sig.override_key

val retype_args : override_key ->
       Cil_types.exp list -> Cil_types.exp list

Same as Generator_sig.override_key

val get_override : override_key -> Cil_types.fundec

get_override key returns the function generated for key. This value is cached so that if it does not exist, it is created using the different Generator_sig generation functions, else the cached version is returned.

val get_kfs : unit -> Cil_types.kernel_function list

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

val clear : unit -> unit

clear () clears the internal table of the instantiator.