diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 422e78690a6874f7d42f357cecbb1c25134dca93..1a83a710a5bb981d01a93e2f5cac9cb58c353743 100644
--- a/headers/header_spec.txt
+++ b/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
diff --git a/src/plugins/builtin/tests/options/test_config b/src/plugins/builtin/tests/options/test_config
deleted file mode 100644
index 23385de533568c5088ea4b945e39aa4c5c35e504..0000000000000000000000000000000000000000
--- a/src/plugins/builtin/tests/options/test_config
+++ /dev/null
@@ -1 +0,0 @@
-OPT: @PTEST_FILE@ -builtin -print
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/test_config b/src/plugins/builtin/tests/stdlib/test_config
deleted file mode 100644
index 467fffb4bcbf47fdf3f1e630026de31df38a78aa..0000000000000000000000000000000000000000
--- a/src/plugins/builtin/tests/stdlib/test_config
+++ /dev/null
@@ -1 +0,0 @@
-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
diff --git a/src/plugins/builtin/tests/string/test_config b/src/plugins/builtin/tests/string/test_config
deleted file mode 100644
index 467fffb4bcbf47fdf3f1e630026de31df38a78aa..0000000000000000000000000000000000000000
--- a/src/plugins/builtin/tests/string/test_config
+++ /dev/null
@@ -1 +0,0 @@
-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
diff --git a/src/plugins/builtin/.gitignore b/src/plugins/instantiate/.gitignore
similarity index 100%
rename from src/plugins/builtin/.gitignore
rename to src/plugins/instantiate/.gitignore
diff --git a/src/plugins/builtin/Builtin.mli b/src/plugins/instantiate/Instantiate.mli
similarity index 87%
rename from src/plugins/builtin/Builtin.mli
rename to src/plugins/instantiate/Instantiate.mli
index a41f4c5c3d8c8ef9ef30a29e48be9031aa39ebdf..603ab3e76501c6e84a137eecfc0b6088b7408bbd 100644
--- a/src/plugins/builtin/Builtin.mli
+++ b/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
diff --git a/src/plugins/builtin/Makefile.in b/src/plugins/instantiate/Makefile.in
similarity index 93%
rename from src/plugins/builtin/Makefile.in
rename to src/plugins/instantiate/Makefile.in
index 79b968e99a98bb80c4370a04b7f772fe6f713bfb..1ab35d905cf1e786c67bd1b6770e9bf2b52c037b 100644
--- a/src/plugins/builtin/Makefile.in
+++ b/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 $@
diff --git a/src/plugins/builtin/README.md b/src/plugins/instantiate/README.md
similarity index 72%
rename from src/plugins/builtin/README.md
rename to src/plugins/instantiate/README.md
index ffdc7099383029e9fca6f2a60e3e07b3bb9fa16c..bf55ae2cf31a74fe80eb1d587adaa83803c8a03e 100644
--- a/src/plugins/builtin/README.md
+++ b/src/plugins/instantiate/README.md
@@ -1,10 +1,10 @@
-# 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`.
\ No newline at end of file
+The role and types of each function is documented in `Instantiator_builder.mli`.
\ No newline at end of file
diff --git a/src/plugins/builtin/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
similarity index 100%
rename from src/plugins/builtin/basic_blocks.ml
rename to src/plugins/instantiate/basic_blocks.ml
diff --git a/src/plugins/builtin/basic_blocks.mli b/src/plugins/instantiate/basic_blocks.mli
similarity index 100%
rename from src/plugins/builtin/basic_blocks.mli
rename to src/plugins/instantiate/basic_blocks.mli
diff --git a/src/plugins/builtin/configure.ac b/src/plugins/instantiate/configure.ac
similarity index 93%
rename from src/plugins/builtin/configure.ac
rename to src/plugins/instantiate/configure.ac
index 706c8832b25842dcae29c37604b0c9b0d1313459..718ec18eaf45758eab14e307223324870b2454a8 100644
--- a/src/plugins/builtin/configure.ac
+++ b/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 #
diff --git a/src/plugins/builtin/builtin_builder.ml b/src/plugins/instantiate/instantiator_builder.ml
similarity index 96%
rename from src/plugins/builtin/builtin_builder.ml
rename to src/plugins/instantiate/instantiator_builder.ml
index 15952538624d65bfd2d03ac646363ff12bfac868..7471c8a8351bdcaa322519b24fb54aae44940883 100644
--- a/src/plugins/builtin/builtin_builder.ml
+++ b/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 =
diff --git a/src/plugins/builtin/builtin_builder.mli b/src/plugins/instantiate/instantiator_builder.mli
similarity index 90%
rename from src/plugins/builtin/builtin_builder.mli
rename to src/plugins/instantiate/instantiator_builder.mli
index 82924b9e8ed8a516d63fda22e1b225f6d19e82fc..fd5f42e26baf0fd65c0aa7641218cc91f9540419 100644
--- a/src/plugins/builtin/builtin_builder.mli
+++ b/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
diff --git a/src/plugins/builtin/options.ml b/src/plugins/instantiate/options.ml
similarity index 89%
rename from src/plugins/builtin/options.ml
rename to src/plugins/instantiate/options.ml
index f4e7e8b813bf69bd8c326f487e4ce3366d1db98f..a094dde9d23ee469f0f7d8f26bc7f91967a5bc1b 100644
--- a/src/plugins/builtin/options.ml
+++ b/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:[]
diff --git a/src/plugins/builtin/options.mli b/src/plugins/instantiate/options.mli
similarity index 89%
rename from src/plugins/builtin/options.mli
rename to src/plugins/instantiate/options.mli
index 8086aca2afeb094291b3d7b66a3f32d283e5875c..320e1bbc1c2b0b2b01b4d96b5d7fcb0f8df0e89f 100644
--- a/src/plugins/builtin/options.mli
+++ b/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
diff --git a/src/plugins/builtin/register.ml b/src/plugins/instantiate/register.ml
similarity index 96%
rename from src/plugins/builtin/register.ml
rename to src/plugins/instantiate/register.ml
index 67719835d820cbfd1879f3f2119a1674ef9bb0f0..4bd18168ac5024287047b8b6eb0fe717feed1cd3 100644
--- a/src/plugins/builtin/register.ml
+++ b/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 =
diff --git a/src/plugins/builtin/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
similarity index 100%
rename from src/plugins/builtin/stdlib/basic_alloc.ml
rename to src/plugins/instantiate/stdlib/basic_alloc.ml
diff --git a/src/plugins/builtin/stdlib/basic_alloc.mli b/src/plugins/instantiate/stdlib/basic_alloc.mli
similarity index 100%
rename from src/plugins/builtin/stdlib/basic_alloc.mli
rename to src/plugins/instantiate/stdlib/basic_alloc.mli
diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
similarity index 100%
rename from src/plugins/builtin/stdlib/calloc.ml
rename to src/plugins/instantiate/stdlib/calloc.ml
diff --git a/src/plugins/builtin/stdlib/calloc.mli b/src/plugins/instantiate/stdlib/calloc.mli
similarity index 100%
rename from src/plugins/builtin/stdlib/calloc.mli
rename to src/plugins/instantiate/stdlib/calloc.mli
diff --git a/src/plugins/builtin/stdlib/free.ml b/src/plugins/instantiate/stdlib/free.ml
similarity index 100%
rename from src/plugins/builtin/stdlib/free.ml
rename to src/plugins/instantiate/stdlib/free.ml
diff --git a/src/plugins/builtin/stdlib/free.mli b/src/plugins/instantiate/stdlib/free.mli
similarity index 100%
rename from src/plugins/builtin/stdlib/free.mli
rename to src/plugins/instantiate/stdlib/free.mli
diff --git a/src/plugins/builtin/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml
similarity index 100%
rename from src/plugins/builtin/stdlib/malloc.ml
rename to src/plugins/instantiate/stdlib/malloc.ml
diff --git a/src/plugins/builtin/stdlib/malloc.mli b/src/plugins/instantiate/stdlib/malloc.mli
similarity index 100%
rename from src/plugins/builtin/stdlib/malloc.mli
rename to src/plugins/instantiate/stdlib/malloc.mli
diff --git a/src/plugins/builtin/string/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
similarity index 98%
rename from src/plugins/builtin/string/memcmp.ml
rename to src/plugins/instantiate/string/memcmp.ml
index a8edb6e540b98c42ac1772f51171d81ca5465b8e..c08fab9d5c3adf96d31ad296d63461c49746b095 100644
--- a/src/plugins/builtin/string/memcmp.ml
+++ b/src/plugins/instantiate/string/memcmp.ml
@@ -102,7 +102,7 @@ let well_typed_call _ret = function
let key_from_call _ret = function
| [ s1 ; _ ; _ ] -> type_from_arg s1
- | _ -> failwith "Call to Memmove.key_from_call on an ill-typed builtin call"
+ | _ -> failwith "Call to Memmove.key_from_call on an ill-typed call"
let retype_args override_key = function
| [ s1 ; s2 ; len ] ->
@@ -113,7 +113,7 @@ let retype_args override_key = function
Cil_datatype.Typ.equal (type_from_arg s2) override_key
) ;
[ s1 ; s2 ; len ]
- | _ -> failwith "Call to Memmove.retype_args on an ill-typed builtin call"
+ | _ -> failwith "Call to Memmove.retype_args on an ill-typed call"
let args_for_original _t args = args
diff --git a/src/plugins/builtin/string/memcmp.mli b/src/plugins/instantiate/string/memcmp.mli
similarity index 100%
rename from src/plugins/builtin/string/memcmp.mli
rename to src/plugins/instantiate/string/memcmp.mli
diff --git a/src/plugins/builtin/string/memcpy.ml b/src/plugins/instantiate/string/memcpy.ml
similarity index 98%
rename from src/plugins/builtin/string/memcpy.ml
rename to src/plugins/instantiate/string/memcpy.ml
index 31eee35d2b49ca384ad02b3275196aee5c1c2653..6a88daa2bb80afec46be151e52bd4fca2cc56d43 100644
--- a/src/plugins/builtin/string/memcpy.ml
+++ b/src/plugins/instantiate/string/memcpy.ml
@@ -108,7 +108,7 @@ let well_typed_call _ret = function
let key_from_call _ret = function
| [ dest ; _ ; _ ] -> type_from_arg dest
- | _ -> failwith "Call to Memcpy.key_from_call on an ill-typed builtin call"
+ | _ -> failwith "Call to Memcpy.key_from_call on an ill-typed call"
let retype_args override_key = function
| [ dest ; src ; len ] ->
@@ -119,7 +119,7 @@ let retype_args override_key = function
Cil_datatype.Typ.equal (type_from_arg src) override_key
) ;
[ dest ; src ; len ]
- | _ -> failwith "Call to Memcpy.retype_args on an ill-typed builtin call"
+ | _ -> failwith "Call to Memcpy.retype_args on an ill-typed call"
let args_for_original _t args = args
diff --git a/src/plugins/builtin/string/memcpy.mli b/src/plugins/instantiate/string/memcpy.mli
similarity index 100%
rename from src/plugins/builtin/string/memcpy.mli
rename to src/plugins/instantiate/string/memcpy.mli
diff --git a/src/plugins/builtin/string/memmove.ml b/src/plugins/instantiate/string/memmove.ml
similarity index 98%
rename from src/plugins/builtin/string/memmove.ml
rename to src/plugins/instantiate/string/memmove.ml
index dd3104d45c5a1aab876d0a7b2369989caee3b720..a987e8cf5e286ea50e5f7c64c6877de410e16d60 100644
--- a/src/plugins/builtin/string/memmove.ml
+++ b/src/plugins/instantiate/string/memmove.ml
@@ -102,7 +102,7 @@ let well_typed_call _ret = function
let key_from_call _ret = function
| [ dest ; _ ; _ ] -> type_from_arg dest
- | _ -> failwith "Call to Memmove.key_from_call on an ill-typed builtin call"
+ | _ -> failwith "Call to Memmove.key_from_call on an ill-typed call"
let retype_args override_key = function
| [ dest ; src ; len ] ->
@@ -113,7 +113,7 @@ let retype_args override_key = function
Cil_datatype.Typ.equal (type_from_arg src) override_key
) ;
[ dest ; src ; len ]
- | _ -> failwith "Call to Memmove.retype_args on an ill-typed builtin call"
+ | _ -> failwith "Call to Memmove.retype_args on an ill-typed call"
let args_for_original _t args = args
diff --git a/src/plugins/builtin/string/memmove.mli b/src/plugins/instantiate/string/memmove.mli
similarity index 100%
rename from src/plugins/builtin/string/memmove.mli
rename to src/plugins/instantiate/string/memmove.mli
diff --git a/src/plugins/builtin/string/memset.ml b/src/plugins/instantiate/string/memset.ml
similarity index 97%
rename from src/plugins/builtin/string/memset.ml
rename to src/plugins/instantiate/string/memset.ml
index 6da6545f3b0f881b9502bcc5127b451f1ce0c394..afee4f55a21ba5a25b71483dba8bccdb25f33495 100644
--- a/src/plugins/builtin/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -29,11 +29,11 @@ type key = (typ * int option)
module With_collection = struct
module OptIntInfo = struct
- let module_name = String.capitalize_ascii "Builtin.Memset.OptInt.Datatype"
+ let module_name = String.capitalize_ascii "Instantiate.Memset.OptInt.Datatype"
end
module OptInt = Datatype.Option_with_collections (Datatype.Int)(OptIntInfo)
module MemsetKeyInfo = struct
- let module_name = String.capitalize_ascii "Builtin.Memset.Key.Datatype"
+ let module_name = String.capitalize_ascii "Instantiate.Memset.Key.Datatype"
end
include Datatype.Pair_with_collections
(Cil_datatype.Typ) (OptInt) (MemsetKeyInfo)
@@ -203,7 +203,7 @@ let key_from_call _ret = function
(type_from_arg ptr), None
| [ ptr ; value ; _ ] when not (is_union_type (type_from_arg ptr)) ->
(type_from_arg ptr), (memset_value value)
- | _ -> failwith "Call to Memset.key_from_call on an ill-typed builtin call"
+ | _ -> failwith "Call to Memset.key_from_call on an ill-typed call"
let char_prototype t =
assert (any_char_composed_type t) ;
@@ -232,7 +232,7 @@ let generate_prototype = function
let fun_type = non_char_prototype t in
name, fun_type
| _, _ ->
- failwith "Call to Memset.generate_prototype on an ill-typed builtin call"
+ failwith "Call to Memset.generate_prototype on an ill-typed call"
let retype_args (t, e) args =
match e, args with
@@ -248,7 +248,7 @@ let retype_args (t, e) args =
assert (match memset_value v with Some x when x = fv -> true | _ -> false) ;
[ ptr ; n ]
| _ ->
- failwith "Call to Memset.retype_args on an ill-typed builtin call"
+ failwith "Call to Memset.retype_args on an ill-typed call"
let args_for_original (_t , e) args =
match e with
diff --git a/src/plugins/builtin/string/memset.mli b/src/plugins/instantiate/string/memset.mli
similarity index 100%
rename from src/plugins/builtin/string/memset.mli
rename to src/plugins/instantiate/string/memset.mli
diff --git a/src/plugins/builtin/tests/api/external_builtin_registration.c b/src/plugins/instantiate/tests/api/external_instantiator_registration.c
similarity index 53%
rename from src/plugins/builtin/tests/api/external_builtin_registration.c
rename to src/plugins/instantiate/tests/api/external_instantiator_registration.c
index d74dd0fcee37333608e5fccc3df5a696b3f312ed..e7366b9816960b0eb6d3c2230c8ff45fc8827e79 100644
--- a/src/plugins/builtin/tests/api/external_builtin_registration.c
+++ b/src/plugins/instantiate/tests/api/external_instantiator_registration.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -load-script tests/api/external_builtin_registration.ml -builtin -check -print
+ OPT: -load-script tests/api/external_instantiator_registration.ml -instantiate -check -print
*/
void mine(void* parameter) ;
@@ -10,4 +10,4 @@ void foo(void){
mine(i);
mine(f);
-}
\ No newline at end of file
+}
diff --git a/src/plugins/builtin/tests/api/external_builtin_registration.ml b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
similarity index 95%
rename from src/plugins/builtin/tests/api/external_builtin_registration.ml
rename to src/plugins/instantiate/tests/api/external_instantiator_registration.ml
index b69388b5e9551b8b62055e21cc58425b88c86fdd..b800bd1efbdd4bd92fe985fab4771f1f001c95cd 100644
--- a/src/plugins/builtin/tests/api/external_builtin_registration.ml
+++ b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
@@ -35,7 +35,7 @@ let generate_spec _ _ _ = Cil.empty_funspec ()
let args_for_original _ x = x
-let () = Builtin.Transform.register (module struct
+let () = Instantiate.Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = Hashtbl.key
@@ -46,4 +46,4 @@ let () = Builtin.Transform.register (module struct
let generate_prototype = generate_prototype
let generate_spec = generate_spec
let args_for_original = args_for_original
- end)
\ No newline at end of file
+ end)
diff --git a/src/plugins/builtin/tests/api/oracle/external_builtin_registration.res.oracle b/src/plugins/instantiate/tests/api/oracle/external_instantiator_registration.res.oracle
similarity index 75%
rename from src/plugins/builtin/tests/api/oracle/external_builtin_registration.res.oracle
rename to src/plugins/instantiate/tests/api/oracle/external_instantiator_registration.res.oracle
index aca41b9d5746d6b9bdaddbd80fd4acf8478f73bc..c4fceec9316f10d163c7ad214d392e45623effcf 100644
--- a/src/plugins/builtin/tests/api/oracle/external_builtin_registration.res.oracle
+++ b/src/plugins/instantiate/tests/api/oracle/external_instantiator_registration.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/api/external_builtin_registration.c (with preprocessing)
+[kernel] Parsing tests/api/external_instantiator_registration.c (with preprocessing)
/* Generated by Frama-C */
void mine(void *parameter);
diff --git a/src/plugins/builtin/tests/options/ignore-functions.c b/src/plugins/instantiate/tests/options/ignore-functions.c
similarity index 87%
rename from src/plugins/builtin/tests/options/ignore-functions.c
rename to src/plugins/instantiate/tests/options/ignore-functions.c
index 5cec9a3a2ee31294dd14f1546a8fa76bca3cea95..3edee39dd0877135a7a9a3f61a749f1234e5a46f 100644
--- a/src/plugins/builtin/tests/options/ignore-functions.c
+++ b/src/plugins/instantiate/tests/options/ignore-functions.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-builtin-fct=@all,-foo"
+ STDOPT: +"-instantiate-fct=@all,-foo"
*/
#include <string.h>
@@ -20,4 +20,4 @@ void baz(){
int src[10] = {0} ;
int dest[10] ;
memcpy(dest, src, sizeof(src)) ;
-}
\ No newline at end of file
+}
diff --git a/src/plugins/builtin/tests/options/ignore-builtin.c b/src/plugins/instantiate/tests/options/ignore-instantiator.c
similarity index 80%
rename from src/plugins/builtin/tests/options/ignore-builtin.c
rename to src/plugins/instantiate/tests/options/ignore-instantiator.c
index e9312d8ec9865418337ac99d6c5d9dc09f1460cc..7c883eb2911efc84bdd49ff19ce8317e3942ff92 100644
--- a/src/plugins/builtin/tests/options/ignore-builtin.c
+++ b/src/plugins/instantiate/tests/options/ignore-instantiator.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT:+"-builtin-no-memcpy"
+ STDOPT:+"-instantiate-no-memcpy"
*/
#include <string.h>
@@ -9,4 +9,4 @@ void foo(){
int dest[10] ;
memset(src, 0, sizeof(src)) ;
memcpy(dest, src, sizeof(src)) ;
-}
\ No newline at end of file
+}
diff --git a/src/plugins/builtin/tests/options/only-functions.c b/src/plugins/instantiate/tests/options/only-functions.c
similarity index 89%
rename from src/plugins/builtin/tests/options/only-functions.c
rename to src/plugins/instantiate/tests/options/only-functions.c
index 9ad8836a67a6f38cca18a24f1387d1d936c3ec03..c92cc19b766889eaab534711e7a80807efa7263d 100644
--- a/src/plugins/builtin/tests/options/only-functions.c
+++ b/src/plugins/instantiate/tests/options/only-functions.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-builtin-fct=foo"
+ STDOPT: +"-instantiate-fct=foo"
*/
#include <string.h>
@@ -20,4 +20,4 @@ void baz(){
int src[10] = {0} ;
int dest[10] ;
memcpy(dest, src, sizeof(src)) ;
-}
\ No newline at end of file
+}
diff --git a/src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle b/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
similarity index 100%
rename from src/plugins/builtin/tests/options/oracle/ignore-functions.res.oracle
rename to src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
diff --git a/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle b/src/plugins/instantiate/tests/options/oracle/ignore-instantiator.res.oracle
similarity index 91%
rename from src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle
rename to src/plugins/instantiate/tests/options/oracle/ignore-instantiator.res.oracle
index 69cf5e09ef7a6f65c519a8866701c11e7087ae50..3c17c3dc05f66a98cf9dbb0111eae666781bd348 100644
--- a/src/plugins/builtin/tests/options/oracle/ignore-builtin.res.oracle
+++ b/src/plugins/instantiate/tests/options/oracle/ignore-instantiator.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/options/ignore-builtin.c (with preprocessing)
+[kernel] Parsing tests/options/ignore-instantiator.c (with preprocessing)
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/builtin/tests/options/oracle/only-functions.res.oracle b/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
similarity index 100%
rename from src/plugins/builtin/tests/options/oracle/only-functions.res.oracle
rename to src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
diff --git a/src/plugins/instantiate/tests/options/test_config b/src/plugins/instantiate/tests/options/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..01d3ae76752389c86266658217efba589a7e71e0
--- /dev/null
+++ b/src/plugins/instantiate/tests/options/test_config
@@ -0,0 +1 @@
+OPT: @PTEST_FILE@ -instantiate -print
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/calloc.c b/src/plugins/instantiate/tests/stdlib/calloc.c
similarity index 100%
rename from src/plugins/builtin/tests/stdlib/calloc.c
rename to src/plugins/instantiate/tests/stdlib/calloc.c
diff --git a/src/plugins/builtin/tests/stdlib/free.c b/src/plugins/instantiate/tests/stdlib/free.c
similarity index 100%
rename from src/plugins/builtin/tests/stdlib/free.c
rename to src/plugins/instantiate/tests/stdlib/free.c
diff --git a/src/plugins/builtin/tests/stdlib/malloc.c b/src/plugins/instantiate/tests/stdlib/malloc.c
similarity index 100%
rename from src/plugins/builtin/tests/stdlib/malloc.c
rename to src/plugins/instantiate/tests/stdlib/malloc.c
diff --git a/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
similarity index 99%
rename from src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
rename to src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index aad87a80a2173a2e4916b089f6102ed4951d59b1..5fb370ab29a192623a74034cbf0923e31191b163 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
-[builtin] tests/stdlib/calloc.c:21: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/calloc.c:21: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
diff --git a/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
similarity index 98%
rename from src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
rename to src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
index 830b23cefbf2e40ca1717eef885baa42ed5255f0..1e764fcd7c62f75f1a4160cd430d760db327f29a 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/stdlib/free.c (with preprocessing)
-[builtin] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
diff --git a/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
similarity index 99%
rename from src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
rename to src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index a43a99fddf6ecfc3a86809a43ebb1751b811ced7..feb0c41909dd4a6cb6b7de4c4ec3dac49cd07869 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[builtin] tests/stdlib/malloc.c:21: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:21: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
diff --git a/src/plugins/instantiate/tests/stdlib/test_config b/src/plugins/instantiate/tests/stdlib/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..dba5b7b5f4a3904ab10ba039dce5bee0734e2101
--- /dev/null
+++ b/src/plugins/instantiate/tests/stdlib/test_config
@@ -0,0 +1 @@
+OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/string/memcmp.c b/src/plugins/instantiate/tests/string/memcmp.c
similarity index 100%
rename from src/plugins/builtin/tests/string/memcmp.c
rename to src/plugins/instantiate/tests/string/memcmp.c
diff --git a/src/plugins/builtin/tests/string/memcpy.c b/src/plugins/instantiate/tests/string/memcpy.c
similarity index 100%
rename from src/plugins/builtin/tests/string/memcpy.c
rename to src/plugins/instantiate/tests/string/memcpy.c
diff --git a/src/plugins/builtin/tests/string/memmove.c b/src/plugins/instantiate/tests/string/memmove.c
similarity index 100%
rename from src/plugins/builtin/tests/string/memmove.c
rename to src/plugins/instantiate/tests/string/memmove.c
diff --git a/src/plugins/builtin/tests/string/memset_0.c b/src/plugins/instantiate/tests/string/memset_0.c
similarity index 100%
rename from src/plugins/builtin/tests/string/memset_0.c
rename to src/plugins/instantiate/tests/string/memset_0.c
diff --git a/src/plugins/builtin/tests/string/memset_FF.c b/src/plugins/instantiate/tests/string/memset_FF.c
similarity index 100%
rename from src/plugins/builtin/tests/string/memset_FF.c
rename to src/plugins/instantiate/tests/string/memset_FF.c
diff --git a/src/plugins/builtin/tests/string/memset_value.c b/src/plugins/instantiate/tests/string/memset_value.c
similarity index 100%
rename from src/plugins/builtin/tests/string/memset_value.c
rename to src/plugins/instantiate/tests/string/memset_value.c
diff --git a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
similarity index 99%
rename from src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
rename to src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 83f1e8a4fbaa365a2479191d5e6c641866981561..9a3d0e6381121a41265d270e492b2b5ffca83dc7 100644
--- a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/string/memcmp.c (with preprocessing)
-[builtin] tests/string/memcmp.c:31: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcmp.c:31: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
similarity index 98%
rename from src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
rename to src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 5a9013b038d5a676888485d9970d4d743f36f69a..63bd23cf23c207e89a094717492cd87246acb3c0 100644
--- a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
-[builtin] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
-[builtin] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
similarity index 98%
rename from src/plugins/builtin/tests/string/oracle/memmove.res.oracle
rename to src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index 193a3f96dbc8823e9775f142f472cc63a98a40b6..6023a30c6bf1db32b311e1cc205aa6780273e26c 100644
--- a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/string/memmove.c (with preprocessing)
-[builtin] tests/string/memmove.c:36: Warning: Ignore call: not well typed
-[builtin] tests/string/memmove.c:37: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:36: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:37: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
similarity index 98%
rename from src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
rename to src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
index 84e0ba0e23d2e5c1fc935d7dcabecdbab3cb66bb..8936d80df52ddcdaf70d3aa9dcf6f9a2c97edf53 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/string/memset_0.c (with preprocessing)
-[builtin] tests/string/memset_0.c:56: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_0.c:57: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:56: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:57: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
similarity index 99%
rename from src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
rename to src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index e45698fc0a39aec442985387420c593b29868ba1..c64a99baf967de3fff4386486b4b06d1687f0959 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/string/memset_FF.c (with preprocessing)
-[builtin] tests/string/memset_FF.c:82: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_FF.c:83: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:82: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:83: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
similarity index 89%
rename from src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
rename to src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
index 50858d41d3ca2de42803b473b42a946d98b78c47..26ed27864cc376fc2578df1e457c44cec81850ec 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -1,16 +1,28 @@
[kernel] Parsing tests/string/memset_value.c (with preprocessing)
-[builtin] tests/string/memset_value.c:26: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:27: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:31: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:32: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:36: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:37: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:41: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:42: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:46: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:47: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:51: Warning: Ignore call: not well typed
-[builtin] tests/string/memset_value.c:52: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:26: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:27: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:31: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:32: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:36: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:37: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:41: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:42: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:46: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:47: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:51: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:52: Warning:
+ Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
diff --git a/src/plugins/instantiate/tests/string/test_config b/src/plugins/instantiate/tests/string/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..dba5b7b5f4a3904ab10ba039dce5bee0734e2101
--- /dev/null
+++ b/src/plugins/instantiate/tests/string/test_config
@@ -0,0 +1 @@
+OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
diff --git a/src/plugins/builtin/transform.ml b/src/plugins/instantiate/transform.ml
similarity index 79%
rename from src/plugins/builtin/transform.ml
rename to src/plugins/instantiate/transform.ml
index acb0ac63b605ad1a07191de5daf62d7614a2b853..797f1ac1bae71dd19612ae1e6692ad5318253005 100644
--- a/src/plugins/builtin/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -21,24 +21,24 @@
(**************************************************************************)
open Cil_types
-open Builtin_builder
+open Instantiator_builder
-let base : (string, (module Builtin)) Hashtbl.t = Hashtbl.create 17
+let base : (string, (module Instantiator)) Hashtbl.t = Hashtbl.create 17
let register (module G: Generator_sig) =
- let module Builtin = Make_builtin(G) in
- Hashtbl.add base G.function_name (module Builtin)
+ let module Instantiator = Make_instantiator(G) in
+ Hashtbl.add base G.function_name (module Instantiator)
let mark_as_computed () =
- let mark_as_computed _ builtin =
- let module B = (val builtin: Builtin) in B.mark_as_computed ()
+ let mark_as_computed _ instantiator =
+ let module I = (val instantiator: Instantiator) in I.mark_as_computed ()
in
Hashtbl.iter mark_as_computed base
let get_kfs () =
- let get_kfs _ builtin =
- let module B = (val builtin: Builtin) in
- let res = B.get_kfs () in
+ let get_kfs _ instantiator =
+ let module I = (val instantiator: Instantiator) in
+ let res = I.get_kfs () in
res
in
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
@@ -48,8 +48,8 @@ module VISet = Cil_datatype.Varinfo.Hptset
class transformer = object(self)
inherit Visitor.frama_c_inplace
- val introduced_builtins = ref VISet.empty
- val used_builtin_last_kf = Queue.create ()
+ val introduced_instantiators = ref VISet.empty
+ val used_instantiator_last_kf = Queue.create ()
method! vfile _ =
let post f =
@@ -64,13 +64,13 @@ class transformer = object(self)
let post g =
let loc = Cil.CurrentLoc.get() in
let folding l fd =
- if VISet.mem fd.svar !introduced_builtins then l
+ if VISet.mem fd.svar !introduced_instantiators then l
else begin
- introduced_builtins := VISet.add fd.svar !introduced_builtins ;
+ introduced_instantiators := VISet.add fd.svar !introduced_instantiators ;
GFun (fd, loc) :: l
end
in
- Queue.fold folding g used_builtin_last_kf
+ Queue.fold folding g used_instantiator_last_kf
in
Cil.DoChildrenPost post
@@ -81,20 +81,20 @@ class transformer = object(self)
else
Cil.SkipChildren
- method private find_enabled_builtin fct =
- let builtin = Hashtbl.find base fct.vname in
- let module B = (val builtin: Builtin) in
- if not (B.Enabled.get ()) then raise Not_found ;
- builtin
+ method private find_enabled_instantiator fct =
+ let instantiator = Hashtbl.find base fct.vname in
+ let module I = (val instantiator: Instantiator) in
+ if not (I.Enabled.get ()) then raise Not_found ;
+ instantiator
method private replace_call (lval, fct, args) =
try
- let module B = (val (self#find_enabled_builtin fct): Builtin) in
- if B.well_typed_call lval args then
- let key = B.key_from_call lval args in
- let fundec = B.get_override key in
- let new_args = B.retype_args key args in
- Queue.add fundec used_builtin_last_kf ;
+ let module I = (val (self#find_enabled_instantiator fct): Instantiator) in
+ if I.well_typed_call lval args then
+ let key = I.key_from_call lval args in
+ let fundec = I.get_override key in
+ let new_args = I.retype_args key args in
+ Queue.add fundec used_instantiator_last_kf ;
(fundec.svar), new_args
else begin
Options.warning ~current:true "Ignore call: not well typed" ;
diff --git a/src/plugins/builtin/transform.mli b/src/plugins/instantiate/transform.mli
similarity index 86%
rename from src/plugins/builtin/transform.mli
rename to src/plugins/instantiate/transform.mli
index 72800ee3426ee6d57c800d63ff501a042d1e182b..bd924473c5d7a3068180cec0c9be5f346bdedfba 100644
--- a/src/plugins/builtin/transform.mli
+++ b/src/plugins/instantiate/transform.mli
@@ -22,14 +22,13 @@
(** Module for AST transformation *)
-(** Registers a new [Builtin] to the visitor from the [Generator_sig] module
- of this builtin. Each new builtin function generator should call this
- globally.
+(** Registers a new [Instantiator] to the visitor from the [Generator_sig]
+ module. Each new instantiator generator should call this globally.
*)
-val register: (module Builtin_builder.Generator_sig) -> unit
+val register: (module Instantiator_builder.Generator_sig) -> unit
(** In all selected functions of the given file, for all function call, if there
- exists a builtin module for this function, and the call is well-typed,
+ exists a instantiator module for this function, and the call is well-typed,
replaces it with a call to the generated override function and inserted the
generated function in the AST.
*)