Functor Instantiator_builder.Make_instantiator

module Make_instantiator: functor (G : Generator_sig) -> Instantiator

Generates a Instantiator from a Generator_sig adding all necessary stuff for cache and function definition generation, as well as specification registration. This should only be used by Transform.

Parameters:

G : Generator_sig

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.