[RENAME PLUGIN] Builtin -> Instantiate

headers/header_spec.txt

@@ -938,34 +938,34 @@ src/plugins/occurrence/options.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/occurrence/register.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/Builtin.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/builtin_builder.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/builtin_builder.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/basic_alloc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/basic_alloc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/calloc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/calloc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/free.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/free.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memcmp.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memcpy.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memcpy.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memmove.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memmove.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memset.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/string/memset.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/transform.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/transform.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/Instantiate.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/instantiator_builder.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/instantiator_builder.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/configure.ac: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/Makefile.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/basic_alloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/basic_alloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/calloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/calloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/free.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/free.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memcmp.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memcpy.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memcpy.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memmove.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memmove.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memset.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/string/memset.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/options.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/options.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/transform.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/transform.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/pdg/Pdg.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/pdg/annot.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/pdg/annot.mli: CEA_LGPL_OR_PROPRIETARY

src/plugins/builtin/tests/options/test_config

-OPT: @PTEST_FILE@ -builtin -print
\ No newline at end of file

src/plugins/builtin/tests/stdlib/test_config

-OPT: @PTEST_FILE@ -builtin -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-builtin @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file

src/plugins/builtin/tests/string/test_config

-OPT: @PTEST_FILE@ -builtin -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-builtin @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file

src/plugins/builtin/Builtin.mli → src/plugins/instantiate/Instantiate.mli

@@ -22,23 +22,23 @@
 
 open Cil_types
 
-module Builtin_builder: sig
-  (** Builds a [Builtin] module (used by [Transform]) from a [Generator_sig] *)
+module Instantiator_builder: sig
+  (** Builds a [Instantiator] module (used by [Transform]) from a [Generator_sig] *)
 
-  (** Signature for a new builtin generator.
+  (** 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 type Generator_sig = sig
-    (** [Hashtbl] module used by the [Make_builtin] module to generate the
+    (** [Hashtbl] module used by the [Make_instantiator] module to generate the
         function cache. The [key] ([override_key]) must identify a function
         override.
     *)
     module Hashtbl: Datatype.Hashtbl
     type override_key = Hashtbl.key
 
-    (** Name of the implemented builtin function *)
+    (** Name of the implemented instantiator function *)
     val function_name: string
 
     (** [well_typed_call ret args] must return true if and only if the
@@ -68,13 +68,13 @@ module Builtin_builder: sig
         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 [Builtin] module generates an override:
+        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_builtin].
+        introduced by [Make_instantiator].
     *)
     val args_for_original: override_key -> exp list -> exp list
 
@@ -93,9 +93,9 @@ module Builtin_builder: sig
 end
 
 module Transform: sig
-  (** Registers a new [Builtin] to the visitor from the [Generator_sig] module
-      of this builtin. Each new builtin function generator should call this
+  (** Registers a new [Instantiator] to the visitor from the [Generator_sig] module
+      of this instantiator. Each new instantiator function generator should call this
       globally.
   *)
-  val register: (module Builtin_builder.Generator_sig) -> unit
+  val register: (module Instantiator_builder.Generator_sig) -> unit
 end

src/plugins/builtin/Makefile.in → src/plugins/instantiate/Makefile.in

@@ -48,14 +48,14 @@ SRC_STDLIB:=$(addprefix stdlib/, $(SRC_STDLIB))
 ###################
 
 PLUGIN_DIR ?= .
-PLUGIN_ENABLE := @ENABLE_BUILTIN@
-PLUGIN_NAME := Builtin
+PLUGIN_ENABLE := @ENABLE_INSTANTIATE@
+PLUGIN_NAME := Instantiate
 PLUGIN_EXTRA_DIRS:=\
 	string\
 	stdlib
 PLUGIN_CMI :=
 PLUGIN_CMO := \
-	basic_blocks options builtin_builder transform register \
+	basic_blocks options instantiator_builder transform register \
 	$(SRC_STRING) \
 	$(SRC_STDLIB)
 
@@ -80,6 +80,6 @@ else
 CONFIG_STATUS_DIR=.
 endif
 
-$(Builtin_DIR)/Makefile: $(Builtin_DIR)/Makefile.in \
+$(Instantiate_DIR)/Makefile: $(Instantiate_DIR)/Makefile.in \
 				$(CONFIG_STATUS_DIR)/config.status
 	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/builtin/README.md → src/plugins/instantiate/README.md

-# Builtin plugin
+# Instantiate plugin
 
 ## Description
 
-The builtin plugin is meant to build function specialization to C functions in
-a project when the original specification (or prototype of the function) cannot
-be efficiently used by some plugins.
+The instantiate plugin is meant to build function specialization to C functions
+in a project when the original specification (or prototype of the function)
+cannot be efficiently used by some plugins.
 
 For example, the specification of a function like `memcpy` cannot be efficiently
 used by a plugin like `WP` because it involves `void*` pointers and requires to
@@ -26,20 +26,20 @@ int *memcpy_int(int *dest, int const *src, size_t len);
 
 That can be easily used by WP.
 
-The role of the Builtin plugin is to find each call for which a builtin
-generator is available and if the call is well-typed according to the generator
-(for example for `memcpy` if `dest` and `src` are both pointers to integers), to
-replace this call with a call to an automatically generated specialization
-corresponding to the call.
+The role of the Instantiate plugin is to find each call for which an
+instantiation generator is available and if the call is well-typed according to
+the generator (for example for `memcpy` if `dest` and `src` are both pointers to
+integers), to replace this call with a call to an automatically generated
+specialization corresponding to the call.
 
 ## Options
 
-- `-builtin` activate builtin replacement
-- `-builtin-fct=f,...` only replace calls in specified functions (default to all)
-- `-builtin-(no-)<function_name>` activate or deactivate a particular builtin
+- `-instantiate` activate function replacement
+- `-instantiate-fct=f,...` only replace calls in specified functions (default to all)
+- `-instantiate-(no-)<function_name>` activate or deactivate a particular
   function, defaults to true.
 
-## Available builtin functions
+## Available functions
 
 ### `string.h`
 
@@ -106,10 +106,10 @@ void* malloc(size_t num, size_t size);
 `malloc` is typed according to the variable that receives its result. It must be
 a pointer type different from `void*`.
 
-## Adding a new builtin
+## Adding a new instantiator
 
-To add a new builtin, one has to register a new module implementing the
-`Builtin_builder.Generator_sig` module type to the `Transform` module. The
+To add a new instantiator, one has to register a new module implementing the
+`Instantiator_builder.Generator_sig` module type to the `Transform` module. The
 lasts steps of the code should look like:
 
 ```ocaml
@@ -117,7 +117,7 @@ let () = Transform.register (module struct
     module Hashtbl = ...
     type override_key = ...
 
-    let function_name = "my_builtin_function"
+    let function_name = "my_function"
     let well_typed_call = ...
     let key_from_call = ...
     let retype_args = ...
@@ -127,4 +127,4 @@ let () = Transform.register (module struct
   end)
 ```
 
-The role and types of each function is documented in `Builtin_builder.mli`.
+The role and types of each function is documented in `Instantiator_builder.mli`.
\ No newline at end of file

src/plugins/builtin/configure.ac → src/plugins/instantiate/configure.ac

@@ -21,7 +21,7 @@
 ##########################################################################
 
 ##########################################
-# Builtin stdlib C plugin                #
+# Instantiate plugin                     #
 ##########################################
 
 m4_define([plugin_file],Makefile.in)
@@ -35,8 +35,8 @@ m4_define([FRAMAC_SHARE],
 
 m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
 
-check_plugin(builtin,PLUGIN_RELATIVE_PATH(plugin_file),
-	     [support for builtin plug-in],yes)
+check_plugin(instantiate,PLUGIN_RELATIVE_PATH(plugin_file),
+	     [support for instantiate plug-in],yes)
 
 #######################
 # Generating Makefile #

src/plugins/builtin/builtin_builder.ml → src/plugins/instantiate/instantiator_builder.ml

@@ -36,7 +36,7 @@ module type Generator_sig = sig
   val generate_spec: override_key -> fundec -> location -> funspec
 end
 
-module type Builtin = sig
+module type Instantiator = sig
   module Enabled: Parameter_sig.Bool
   type override_key
 
@@ -65,14 +65,14 @@ let build_body caller callee args_generator =
   let ret = Cil.mkStmt (Return ( (opt_map Cil.evar ret_var), loc)) in
   { (Cil.mkBlock [call ; ret]) with blocals = list_of_opt ret_var }
 
-module Make_builtin (G: Generator_sig) = struct
+module Make_instantiator (G: Generator_sig) = struct
   include G
-  module Enabled = Options.NewBuiltin (G)
+  module Enabled = Options.NewInstantiator (G)
   module Cache = State_builder.Hashtbl (G.Hashtbl) (Cil_datatype.Fundec)
       (struct
         let size = 5
         let dependencies = []
-        let name = "Builtins." ^ G.function_name
+        let name = "Instantiator." ^ G.function_name
       end)
 
   let make_fundec key =

src/plugins/builtin/builtin_builder.mli → src/plugins/instantiate/instantiator_builder.mli

@@ -22,22 +22,22 @@
 
 open Cil_types
 
-(** Builds a [Builtin] module (used by [Transform]) from a [Generator_sig] *)
+(** Builds a [Instantiator] module (used by [Transform]) from a [Generator_sig] *)
 
-(** Signature for a new builtin generator.
+(** 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 type Generator_sig = sig
-  (** [Hashtbl] module used by the [Make_builtin] module to generate the
+  (** [Hashtbl] module used by the [Make_instantiator] module to generate the
       function cache. The [key] ([override_key]) must identify a function
       override.
   *)
   module Hashtbl: Datatype.Hashtbl
   type override_key = Hashtbl.key
 
-  (** Name of the implemented builtin function *)
+  (** Name of the implemented function *)
   val function_name: string
 
   (** [well_typed_call ret args] must return true if and only if the
@@ -67,13 +67,13 @@ module type Generator_sig = sig
       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 [Builtin] module generates an override:
+      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_builtin].
+      introduced by [Make_instantiator].
   *)
   val args_for_original: override_key -> exp list -> exp list
 
@@ -90,14 +90,14 @@ module type Generator_sig = sig
   val generate_spec: override_key -> fundec -> location -> funspec
 end
 
-(** Signature of a builtin.
+(** 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 type Builtin = sig
-  (** Plugin option that allows to check whether the builtin is enabled. *)
+module type Instantiator = sig
+  (** Plugin option that allows to check whether the instantiator is enabled. *)
   module Enabled: Parameter_sig.Bool
   (** Same as [Generator_sig.override_key] *)
   type override_key
@@ -129,8 +129,8 @@ module type Builtin = sig
   val mark_as_computed:  ?project:Project.t -> unit -> unit
 end
 
-(** Generates a [Builtin] from a [Generator_sig] adding all necessary stuff for
+(** 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].
 *)
-module Make_builtin (G: Generator_sig) : Builtin
+module Make_instantiator (G: Generator_sig) : Instantiator

src/plugins/builtin/options.ml → src/plugins/instantiate/options.ml

@@ -20,8 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-let name = "Builtin"
-let shortname = "builtin"
+let name = "Instantiate"
+let shortname = "instantiate"
 
 include Plugin.Register
     (struct
@@ -44,10 +44,10 @@ module Kfs =
       let help = "Override stdlib functions only into the specified functions (defaults to all)."
     end)
 
-module NewBuiltin (B: sig val function_name: string end) = True
+module NewInstantiator (I: sig val function_name: string end) = True
     (struct
-      let option_name = "-" ^ shortname ^ "-" ^ B.function_name
-      let help = "Activate replacement for function '" ^ B.function_name ^ "'"
+      let option_name = "-" ^ shortname ^ "-" ^ I.function_name
+      let help = "Activate replacement for function '" ^ I.function_name ^ "'"
     end)
 
 let emitter = Emitter.create shortname [Emitter.Funspec] ~correctness:[] ~tuning:[]

src/plugins/builtin/options.mli → src/plugins/instantiate/options.mli

@@ -22,17 +22,17 @@
 
 include Plugin.General_services
 
-(** Builtin transformtion enabled *)
+(** Instantiate transformation enabled *)
 module Enabled : Parameter_sig.Bool
 
 (** Set of kernel function provided for transformation *)
 module Kfs : Parameter_sig.Kernel_function_set
 
-(** Used by [Builtin_builder] to generate builtin options. For a given builtin,
-    the module generate an option "-builtin-(no-)<function_name>" that defaults
+(** Used by [Instantiator_builder] to generate options. For a given instantiator
+    the module generates an option "-instantiate-(no-)<function_name>" that defaults
     to true.
 *)
-module NewBuiltin
+module NewInstantiator
     (B : sig val function_name: string end) : Parameter_sig.Bool
 
 val emitter: Emitter.t

src/plugins/builtin/register.ml → src/plugins/instantiate/register.ml

@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-let category = File.register_code_transformation_category "builtin"
+let category = File.register_code_transformation_category "instantiate"
 
 let () =
   let perform file =