From bec92f6ad181659ec0cc85e68371b029f356d8dd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Feb 2020 14:19:36 +0100
Subject: [PATCH] [RENAME PLUGIN] Builtin -> Instantiate
---
headers/header_spec.txt | 56 +++++++++----------
src/plugins/builtin/tests/options/test_config | 1 -
src/plugins/builtin/tests/stdlib/test_config | 1 -
src/plugins/builtin/tests/string/test_config | 1 -
.../{builtin => instantiate}/.gitignore | 0
.../Instantiate.mli} | 20 +++----
.../{builtin => instantiate}/Makefile.in | 8 +--
.../{builtin => instantiate}/README.md | 36 ++++++------
.../{builtin => instantiate}/basic_blocks.ml | 0
.../{builtin => instantiate}/basic_blocks.mli | 0
.../{builtin => instantiate}/configure.ac | 6 +-
.../instantiator_builder.ml} | 8 +--
.../instantiator_builder.mli} | 22 ++++----
.../{builtin => instantiate}/options.ml | 10 ++--
.../{builtin => instantiate}/options.mli | 8 +--
.../{builtin => instantiate}/register.ml | 2 +-
.../stdlib/basic_alloc.ml | 0
.../stdlib/basic_alloc.mli | 0
.../{builtin => instantiate}/stdlib/calloc.ml | 0
.../stdlib/calloc.mli | 0
.../{builtin => instantiate}/stdlib/free.ml | 0
.../{builtin => instantiate}/stdlib/free.mli | 0
.../{builtin => instantiate}/stdlib/malloc.ml | 0
.../stdlib/malloc.mli | 0
.../{builtin => instantiate}/string/memcmp.ml | 4 +-
.../string/memcmp.mli | 0
.../{builtin => instantiate}/string/memcpy.ml | 4 +-
.../string/memcpy.mli | 0
.../string/memmove.ml | 4 +-
.../string/memmove.mli | 0
.../{builtin => instantiate}/string/memset.ml | 10 ++--
.../string/memset.mli | 0
.../api/external_instantiator_registration.c} | 4 +-
.../external_instantiator_registration.ml} | 4 +-
...rnal_instantiator_registration.res.oracle} | 2 +-
.../tests/options/ignore-functions.c | 4 +-
.../tests/options/ignore-instantiator.c} | 4 +-
.../tests/options/only-functions.c | 4 +-
.../oracle/ignore-functions.res.oracle | 0
.../oracle/ignore-instantiator.res.oracle} | 2 +-
.../options/oracle/only-functions.res.oracle | 0
.../instantiate/tests/options/test_config | 1 +
.../tests/stdlib/calloc.c | 0
.../tests/stdlib/free.c | 0
.../tests/stdlib/malloc.c | 0
.../tests/stdlib/oracle/calloc.res.oracle | 2 +-
.../tests/stdlib/oracle/free.res.oracle | 2 +-
.../tests/stdlib/oracle/malloc.res.oracle | 2 +-
.../instantiate/tests/stdlib/test_config | 1 +
.../tests/string/memcmp.c | 0
.../tests/string/memcpy.c | 0
.../tests/string/memmove.c | 0
.../tests/string/memset_0.c | 0
.../tests/string/memset_FF.c | 0
.../tests/string/memset_value.c | 0
.../tests/string/oracle/memcmp.res.oracle | 2 +-
.../tests/string/oracle/memcpy.res.oracle | 4 +-
.../tests/string/oracle/memmove.res.oracle | 4 +-
.../tests/string/oracle/memset_0.res.oracle | 4 +-
.../tests/string/oracle/memset_FF.res.oracle | 4 +-
.../string/oracle/memset_value.res.oracle | 36 ++++++++----
.../instantiate/tests/string/test_config | 1 +
.../{builtin => instantiate}/transform.ml | 50 ++++++++---------
.../{builtin => instantiate}/transform.mli | 9 ++-
64 files changed, 179 insertions(+), 168 deletions(-)
delete mode 100644 src/plugins/builtin/tests/options/test_config
delete mode 100644 src/plugins/builtin/tests/stdlib/test_config
delete mode 100644 src/plugins/builtin/tests/string/test_config
rename src/plugins/{builtin => instantiate}/.gitignore (100%)
rename src/plugins/{builtin/Builtin.mli => instantiate/Instantiate.mli} (87%)
rename src/plugins/{builtin => instantiate}/Makefile.in (93%)
rename src/plugins/{builtin => instantiate}/README.md (72%)
rename src/plugins/{builtin => instantiate}/basic_blocks.ml (100%)
rename src/plugins/{builtin => instantiate}/basic_blocks.mli (100%)
rename src/plugins/{builtin => instantiate}/configure.ac (93%)
rename src/plugins/{builtin/builtin_builder.ml => instantiate/instantiator_builder.ml} (96%)
rename src/plugins/{builtin/builtin_builder.mli => instantiate/instantiator_builder.mli} (90%)
rename src/plugins/{builtin => instantiate}/options.ml (89%)
rename src/plugins/{builtin => instantiate}/options.mli (89%)
rename src/plugins/{builtin => instantiate}/register.ml (96%)
rename src/plugins/{builtin => instantiate}/stdlib/basic_alloc.ml (100%)
rename src/plugins/{builtin => instantiate}/stdlib/basic_alloc.mli (100%)
rename src/plugins/{builtin => instantiate}/stdlib/calloc.ml (100%)
rename src/plugins/{builtin => instantiate}/stdlib/calloc.mli (100%)
rename src/plugins/{builtin => instantiate}/stdlib/free.ml (100%)
rename src/plugins/{builtin => instantiate}/stdlib/free.mli (100%)
rename src/plugins/{builtin => instantiate}/stdlib/malloc.ml (100%)
rename src/plugins/{builtin => instantiate}/stdlib/malloc.mli (100%)
rename src/plugins/{builtin => instantiate}/string/memcmp.ml (98%)
rename src/plugins/{builtin => instantiate}/string/memcmp.mli (100%)
rename src/plugins/{builtin => instantiate}/string/memcpy.ml (98%)
rename src/plugins/{builtin => instantiate}/string/memcpy.mli (100%)
rename src/plugins/{builtin => instantiate}/string/memmove.ml (98%)
rename src/plugins/{builtin => instantiate}/string/memmove.mli (100%)
rename src/plugins/{builtin => instantiate}/string/memset.ml (97%)
rename src/plugins/{builtin => instantiate}/string/memset.mli (100%)
rename src/plugins/{builtin/tests/api/external_builtin_registration.c => instantiate/tests/api/external_instantiator_registration.c} (53%)
rename src/plugins/{builtin/tests/api/external_builtin_registration.ml => instantiate/tests/api/external_instantiator_registration.ml} (95%)
rename src/plugins/{builtin/tests/api/oracle/external_builtin_registration.res.oracle => instantiate/tests/api/oracle/external_instantiator_registration.res.oracle} (75%)
rename src/plugins/{builtin => instantiate}/tests/options/ignore-functions.c (87%)
rename src/plugins/{builtin/tests/options/ignore-builtin.c => instantiate/tests/options/ignore-instantiator.c} (80%)
rename src/plugins/{builtin => instantiate}/tests/options/only-functions.c (89%)
rename src/plugins/{builtin => instantiate}/tests/options/oracle/ignore-functions.res.oracle (100%)
rename src/plugins/{builtin/tests/options/oracle/ignore-builtin.res.oracle => instantiate/tests/options/oracle/ignore-instantiator.res.oracle} (91%)
rename src/plugins/{builtin => instantiate}/tests/options/oracle/only-functions.res.oracle (100%)
create mode 100644 src/plugins/instantiate/tests/options/test_config
rename src/plugins/{builtin => instantiate}/tests/stdlib/calloc.c (100%)
rename src/plugins/{builtin => instantiate}/tests/stdlib/free.c (100%)
rename src/plugins/{builtin => instantiate}/tests/stdlib/malloc.c (100%)
rename src/plugins/{builtin => instantiate}/tests/stdlib/oracle/calloc.res.oracle (99%)
rename src/plugins/{builtin => instantiate}/tests/stdlib/oracle/free.res.oracle (98%)
rename src/plugins/{builtin => instantiate}/tests/stdlib/oracle/malloc.res.oracle (99%)
create mode 100644 src/plugins/instantiate/tests/stdlib/test_config
rename src/plugins/{builtin => instantiate}/tests/string/memcmp.c (100%)
rename src/plugins/{builtin => instantiate}/tests/string/memcpy.c (100%)
rename src/plugins/{builtin => instantiate}/tests/string/memmove.c (100%)
rename src/plugins/{builtin => instantiate}/tests/string/memset_0.c (100%)
rename src/plugins/{builtin => instantiate}/tests/string/memset_FF.c (100%)
rename src/plugins/{builtin => instantiate}/tests/string/memset_value.c (100%)
rename src/plugins/{builtin => instantiate}/tests/string/oracle/memcmp.res.oracle (99%)
rename src/plugins/{builtin => instantiate}/tests/string/oracle/memcpy.res.oracle (98%)
rename src/plugins/{builtin => instantiate}/tests/string/oracle/memmove.res.oracle (98%)
rename src/plugins/{builtin => instantiate}/tests/string/oracle/memset_0.res.oracle (98%)
rename src/plugins/{builtin => instantiate}/tests/string/oracle/memset_FF.res.oracle (99%)
rename src/plugins/{builtin => instantiate}/tests/string/oracle/memset_value.res.oracle (89%)
create mode 100644 src/plugins/instantiate/tests/string/test_config
rename src/plugins/{builtin => instantiate}/transform.ml (79%)
rename src/plugins/{builtin => instantiate}/transform.mli (86%)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 422e78690a6..1a83a710a5b 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 23385de5335..00000000000
--- 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 467fffb4bcb..00000000000
--- 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 467fffb4bcb..00000000000
--- 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 a41f4c5c3d8..603ab3e7650 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 79b968e99a9..1ab35d905cf 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 ffdc7099383..bf55ae2cf31 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 706c8832b25..718ec18eaf4 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 15952538624..7471c8a8351 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 82924b9e8ed..fd5f42e26ba 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 f4e7e8b813b..a094dde9d23 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 8086aca2afe..320e1bbc1c2 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 67719835d82..4bd18168ac5 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 a8edb6e540b..c08fab9d5c3 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 31eee35d2b4..6a88daa2bb8 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 dd3104d45c5..a987e8cf5e2 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 6da6545f3b0..afee4f55a21 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 d74dd0fcee3..e7366b98169 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 b69388b5e95..b800bd1efbd 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 aca41b9d574..c4fceec9316 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 5cec9a3a2ee..3edee39dd08 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 e9312d8ec98..7c883eb2911 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 9ad8836a67a..c92cc19b766 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 69cf5e09ef7..3c17c3dc05f 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 00000000000..01d3ae76752
--- /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 aad87a80a21..5fb370ab29a 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 830b23cefbf..1e764fcd7c6 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 a43a99fddf6..feb0c41909d 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 00000000000..dba5b7b5f4a
--- /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 83f1e8a4fba..9a3d0e63811 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 5a9013b038d..63bd23cf23c 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 193a3f96dbc..6023a30c6bf 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 84e0ba0e23d..8936d80df52 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 e45698fc0a3..c64a99baf96 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 50858d41d3c..26ed27864cc 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 00000000000..dba5b7b5f4a
--- /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 acb0ac63b60..797f1ac1bae 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 72800ee3426..bd924473c5d 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.
*)
--
GitLab