diff --git a/tests/spec/Extend_conflict.i b/tests/spec/Extend_conflict.i
deleted file mode 100644
index cb82bc29c44e7481555acc3057669ccc3e4bd606..0000000000000000000000000000000000000000
--- a/tests/spec/Extend_conflict.i
+++ /dev/null
@@ -1,10 +0,0 @@
-/* run.config
-  MODULE: Extend_plugin
-  EXIT: 1
-  STDOPT:
-*/
-
-//@ \eva::foo x == 0;
-int g(int x) {
-  return x;
-}
diff --git a/tests/spec/Extend_errors.c b/tests/spec/Extend_errors.c
new file mode 100644
index 0000000000000000000000000000000000000000..775c3bff98e97d9e58e6a6a8d2ea453d5b85f13a
--- /dev/null
+++ b/tests/spec/Extend_errors.c
@@ -0,0 +1,40 @@
+/* run.config
+  MODULE: @PTEST_NAME@
+  COMMENT: Debug is set to distinguish this particular test in the module
+  STDOPT: +"-debug 1 -kernel-msg-key acsl-extension"
+  STDOPT: +"-cpp-extra-args=-DWARN_EXT_KERNEL"
+  STDOPT: +"-cpp-extra-args=-DWARN_EXT_TOKEN"
+  EXIT: 1
+  STDOPT: +"-cpp-extra-args=-DWARN_EXT_UNKNOWN"
+  STDOPT: +"-cpp-extra-args=-DERR_EXT_AMBIGUITY"
+*/
+
+/*@ \myplugin1::foo x == 0;
+    \myplugin2::foo x == 0;
+*/
+int ok(int x) {
+  return x;
+}
+
+// Using a token as extension name
+#ifdef WARN_EXT_TOKEN
+//@ \myplugin1::__FC_FILENAME__ x == 0;
+#endif
+
+#ifdef ERR_EXT_KERNEL
+int kernel(int x) {
+  //@ \kernel::calls ok;
+  return ok(x);
+}
+#endif
+
+#ifdef WARN_EXT_UNKNOWN
+/*@ \myplugin1::bar x == 0;
+    \unknown_plugin::bar x == 0;
+ */
+#endif
+
+// Using an extension registered 2 times or more with different plugins
+#ifdef ERR_EXT_AMBIGUITY
+//@ foo x == 0;
+#endif
diff --git a/tests/spec/Extend_errors.ml b/tests/spec/Extend_errors.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9a4d583747e0ffd27e52780734f7c15b9b2fb1ad
--- /dev/null
+++ b/tests/spec/Extend_errors.ml
@@ -0,0 +1,51 @@
+open Logic_typing
+
+module Plugin1 =
+  Plugin.Register
+    (struct
+      let name = "MyPlugin1"
+      let shortname = "myplugin1"
+      let help = ""
+    end)
+
+module Plugin2 =
+  Plugin.Register
+    (struct
+      let name = "MyPlugin2"
+      let shortname = "myplugin2"
+      let help = ""
+    end)
+
+let type_foo typing_context _loc l =
+  let preds =
+    List.map
+      (typing_context.type_predicate
+         typing_context typing_context.pre_state)
+      l
+  in
+  Cil_types.Ext_preds preds
+
+let catch msg f x =
+  try
+    Kernel.feedback "Triggering %s :" msg;
+    ignore(f x)
+  with _ -> ()
+
+let cover_errors () =
+  catch "User Error" (Logic_env.is_extension ~plugin:None) "foo";
+  catch "Unsupported" (Logic_env.preprocess_extension ~plugin:(Some "myplugin1")) "bar"
+
+let cover_warnings () =
+  Acsl_extension.register_behavior ~plugin:"myplugin1" "foo" type_foo false;
+  Acsl_extension.register_behavior ~plugin:"myplugin1" "unfold" type_foo false
+
+let () =
+  Format.printf "[test-extend_errors] Linking.@.";
+  Acsl_extension.register_behavior ~plugin:"myplugin1" "foo" type_foo false;
+  Acsl_extension.register_behavior ~plugin:"myplugin2" "foo" type_foo false;
+  Acsl_extension.register_behavior ~plugin:"myplugin2" "bar" type_foo false;
+
+  if Kernel.GeneralDebug.get () = 1 then begin
+    cover_warnings ();
+    cover_errors ()
+  end
diff --git a/tests/spec/Extend_kernel.i b/tests/spec/Extend_kernel.i
deleted file mode 100644
index a53a4fe67fd5e8890a93c7887ddaa6fb1a50d49e..0000000000000000000000000000000000000000
--- a/tests/spec/Extend_kernel.i
+++ /dev/null
@@ -1,13 +0,0 @@
-/* run.config
-  EXIT: 1
-  STDOPT:
-*/
-
-int g(int x){
-  return x + 42;
-}
-
-int f(int x) {
-  //@ \kernel::calls g;
-  return g(x);
-}
diff --git a/tests/spec/Extend_plugin.ml b/tests/spec/Extend_plugin.ml
deleted file mode 100644
index 0a826d2968832b86943e011f35eadfdcf9e3a2b6..0000000000000000000000000000000000000000
--- a/tests/spec/Extend_plugin.ml
+++ /dev/null
@@ -1,22 +0,0 @@
-open Logic_typing
-
-include
-  Plugin.Register
-    (struct
-      let name = "MyPlugin"
-      let shortname = "myplugin"
-      let help = ""
-    end)
-
-let type_foo typing_context _loc l =
-  let preds =
-    List.map
-      (typing_context.type_predicate
-         typing_context typing_context.pre_state)
-      l
-  in
-  Cil_types.Ext_preds preds
-
-let () =
-  Acsl_extension.register_behavior ~plugin:"myplugin" "foo" type_foo false;
-  Acsl_extension.register_behavior ~plugin:"myplugin" "foo" type_foo false
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index 7a836e0d1050bb5dc49e69236b8206490419b44b..be862c32953eb3e10296c9907efabec69c275bdd 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -12,12 +12,12 @@ let ext_typing_fooo _typing_context _loc l =
 
 let ext_typing_block typing_context loc_here node =
   match node.extended_node with
-  | Ext_lexpr (name,data)  ->
-    let status,kind = Logic_typing.get_typer name ~typing_context ~loc:node.extended_loc data in
-    Logic_const.new_acsl_extension name loc_here status kind
-  | Ext_extension (name, id, data) ->
-    let status,kind = Logic_typing.get_typer_block name ~typing_context ~loc:node.extended_loc (id,data) in
-    Logic_const.new_acsl_extension name loc_here status kind
+  | Ext_lexpr (name,plugin,data)  ->
+    let status,kind = Logic_typing.get_typer ~plugin name ~typing_context ~loc:node.extended_loc data in
+    Logic_const.new_acsl_extension name plugin loc_here status kind
+  | Ext_extension (name, plugin, id, data) ->
+    let status,kind = Logic_typing.get_typer_block ~plugin name ~typing_context ~loc:node.extended_loc (id,data) in
+    Logic_const.new_acsl_extension name plugin loc_here status kind
 
 let  ext_typing_foo typing_context loc (s,d) =
   let block = List.map (ext_typing_block typing_context loc) d in
diff --git a/tests/spec/Extend_type_token.i b/tests/spec/Extend_type_token.i
deleted file mode 100644
index 938a1551d689ca7147a4a8d458fab5be55aae8c1..0000000000000000000000000000000000000000
--- a/tests/spec/Extend_type_token.i
+++ /dev/null
@@ -1,10 +0,0 @@
-/* run.config
-  MODULE: Extend_plugin
-  EXIT: 1
-  STDOPT:
-*/
-
-//@ \myplugin::integer x == 0;
-int g(int x) {
-  return x;
-}
diff --git a/tests/spec/Extend_warning.i b/tests/spec/Extend_warning.i
deleted file mode 100644
index a1773b04cdccd790ba1bfea2f49ef168aa6d1c91..0000000000000000000000000000000000000000
--- a/tests/spec/Extend_warning.i
+++ /dev/null
@@ -1,12 +0,0 @@
-/* run.config
-  MODULE: Extend_plugin
-  STDOPT: +"-kernel-warn-key=extension-unknown=active"
-*/
-
-/*@ \myplugin::foo x == 0;
-    \myplugin::bar x == 0;
-    \unknown_plugin::bar x == 0;
- */
-int f(int x) {
-  return x;
-}
diff --git a/tests/spec/import.i b/tests/spec/import.i
index 837dffbac760fa5033558c9180fdd888069089e1..0644f8f3da6ea292c4d758d258a6ba72aae82bd1 100644
--- a/tests/spec/import.i
+++ b/tests/spec/import.i
@@ -1,13 +1,20 @@
 /* run.config
-MODULE: @PTEST_NAME@
-OPT: -print
-OPT: -print -kernel-msg-key printer:imported-modules
+  MODULE: Test_import
+  STDOPT: +"-kernel-msg-key acsl-extension"
+  STDOPT: +"-kernel-msg-key acsl-extension -kernel-msg-key printer:imported-modules"
 */
 
-/*@ import foo: A::B; */
-/*@ predicate check1(B::t x) = B::check(x,0); */
-/*@ predicate check2(A::B::t x) = A::B::check(x,0); */
+//@ import \myplugin1::foo: A::B;
+//@ predicate check1(B::t x) = B::check(x,0);
+//@ predicate check2(A::B::t x) = A::B::check(x,0);
 
-/*@ import foo: A::B \as C; */
-/*@ predicate check3(C::t x) = C::check(x,0); */
-/*@ predicate check4(C::t x) = A::B::check(x,0); */
+//@ import \myplugin1::foo: A::B \as C;
+//@ predicate check3(C::t x) = C::check(x,0);
+//@ predicate check4(C::t x) = A::B::check(x,0);
+
+//@ import \myplugin2::foo: X;
+//@ predicate check5(X::t x) = X::check(x,0);
+
+//@ import bar: X::Y;
+//@ predicate check6(Y::t x) = Y::check(x,0);
+//@ predicate check7(X::Y::t x) = X::Y::check(x,0);
diff --git a/tests/spec/import_errors.c b/tests/spec/import_errors.c
new file mode 100644
index 0000000000000000000000000000000000000000..241485254258a6932a3e4d24cdc536f1cb0dc931
--- /dev/null
+++ b/tests/spec/import_errors.c
@@ -0,0 +1,46 @@
+/* run.config
+  MODULE: Test_import
+  COMMENT: Debug is set to distinguish this particular test in the module
+  STDOPT: +"-debug 1 -kernel-msg-key acsl-extension -cpp-extra-args=-DWARNINGS"
+  EXIT: 1
+  STDOPT: +"-cpp-extra-args=-DERR_DRIVER_AMBIGUITY"
+  STDOPT: +"-cpp-extra-args=-DERR_UNKNOWN_DRIVER1"
+  STDOPT: +"-cpp-extra-args=-DERR_UNKNOWN_DRIVER2"
+*/
+
+#ifdef WARNINGS
+// Wrong token identifier (here parsed as BEHAVIORS)
+//@ import \myplugin1::behaviors: A;
+
+//@ import \myplugin1::foo: B;
+
+// Silently ignored, duplicated import
+//@ import \myplugin1::foo: B;
+
+// Already imported with different driver
+//@ import \myplugin1::bar: B;
+// Already imported with different plugin
+//@ import \myplugin2::foo: B;
+
+/*@
+  module C {
+    type t;
+    predicate check(t x, ℤ k) ;
+  }
+  // Module C already defined
+  import \myplugin1::foo: C;
+*/
+#endif
+
+#ifdef ERR_DRIVER_AMBIGUITY
+//@ import foo: A::B \as D;
+#endif
+
+#ifdef ERR_UNKNOWN_DRIVER1
+//@ import \myplugin1::toto: E;
+#endif
+
+#ifdef ERR_UNKNOWN_DRIVER2
+//@ import toto: F;
+#endif
+
diff --git a/tests/spec/module.c b/tests/spec/module.c
index 6fa3d132da5e5acc9cf49cb54232485521ec6110..2c2d027f58c08131b7a3027b6e8f0e73b0ee6f31 100644
--- a/tests/spec/module.c
+++ b/tests/spec/module.c
@@ -81,6 +81,21 @@ logic integer z = b::a; // KO
     import foo::jazz ;
     logic a f_ko(a x) = bar::f(x);  // KO, ill typed
   }
- */
+*/
 
+/*@
+  // Duplicated module
+  module Foo {
+    type t;
+  }
+*/
+
+/*@
+  // Nested module in axiomatix is not supported yet
+  axiomatic p {
+    module Bar {
+      type t;
+    }
+  }
+*/
 #endif
diff --git a/tests/spec/oracle/Extend_conflict.res.oracle b/tests/spec/oracle/Extend_conflict.res.oracle
deleted file mode 100644
index ae562310f5f3e42f74fba518fc11712b7ef73f59..0000000000000000000000000000000000000000
--- a/tests/spec/oracle/Extend_conflict.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-[kernel:acsl-extension] Warning: 
-  Trying to register ACSL extension foo twice. Ignoring second extension
-[kernel] Parsing Extend_conflict.i (no preprocessing)
-[kernel] Extend_conflict.i:7: User Error: 
-  Extension 'foo' is from myplugin and not eva
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_errors.0.res.oracle b/tests/spec/oracle/Extend_errors.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1cd048aac0469548c28d44a6a86bd09efa947bf6
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.0.res.oracle
@@ -0,0 +1,43 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
+[test-extend_errors] Linking.
+[kernel:acsl-extension] Registering acsl extension \myplugin1::foo
+[kernel:acsl-extension] Registering acsl extension \myplugin2::foo
+[kernel:acsl-extension] Registering acsl extension \myplugin2::bar
+[kernel:acsl-extension] Registering acsl extension \myplugin1::foo
+[kernel:acsl-extension] Warning: 
+  Trying to register ACSL extension foo twice with plugin myplugin1. Ignoring the second extension
+[kernel:acsl-extension] Registering acsl extension \myplugin1::unfold
+[kernel:acsl-extension] Warning: 
+  Trying to register ACSL extension unfold reserved by frama-c. Rename this extension to avoid conflict with the kernel. Ignored extension
+[kernel] Triggering User Error :
+[kernel] <unknown location> User Error: 
+  Conflicts on extension named 'foo' registered by different plugins (myplugin2,
+  myplugin1), use '\plugin::ext_name' syntax to avoid this ambiguity
+[kernel] Triggering Unsupported :
+[kernel] <unknown location> Failure: 
+  Unsupported clause extension named '\myplugin1::bar'
+[kernel] Parsing Extend_errors.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ \myplugin1::foo x ≡ 0;
+    \myplugin2::foo x ≡ 0; */
+int ok(int x)
+{
+  /* sid:2 */
+  return x;
+}
+
+
diff --git a/tests/spec/oracle/Extend_errors.1.res.oracle b/tests/spec/oracle/Extend_errors.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cc45c5f924580ee9e40d4fdb72828189e6160a4c
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.1.res.oracle
@@ -0,0 +1,11 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ \myplugin1::foo x ≡ 0;
+    \myplugin2::foo x ≡ 0; */
+int ok(int x)
+{
+  return x;
+}
+
+
diff --git a/tests/spec/oracle/Extend_errors.2.res.oracle b/tests/spec/oracle/Extend_errors.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..27de177ede17483e80c4f77715ce8f736b3a109d
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.2.res.oracle
@@ -0,0 +1,13 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+[kernel:annot-error] Extend_errors.c:21: Warning: 
+  unexpected token '\myplugin1::__FC_FILENAME__'
+/* Generated by Frama-C */
+/*@ \myplugin1::foo x ≡ 0;
+    \myplugin2::foo x ≡ 0; */
+int ok(int x)
+{
+  return x;
+}
+
+
diff --git a/tests/spec/oracle/Extend_errors.3.res.oracle b/tests/spec/oracle/Extend_errors.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c12d7dc67efde446c9feaab6790b0eebbe0c0ffe
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.3.res.oracle
@@ -0,0 +1,8 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+[kernel:extension-unknown] Extend_errors.c:32: Warning: 
+  Ignoring unregistered extension 'bar' of plug-in myplugin1
+[kernel:plugin-not-loaded] Extend_errors.c:33: Warning: 
+  Ignoring extension 'bar' for unloaded plug-in unknown_plugin
+[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_errors.4.res.oracle b/tests/spec/oracle/Extend_errors.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..62c309ecec02490037b75acc0049944787d40efc
--- /dev/null
+++ b/tests/spec/oracle/Extend_errors.4.res.oracle
@@ -0,0 +1,6 @@
+[test-extend_errors] Linking.
+[kernel] Parsing Extend_errors.c (with preprocessing)
+[kernel] Extend_errors.c:39: User Error: 
+  Conflicts on extension named 'foo' registered by different plugins (myplugin2,
+  myplugin1), use '\plugin::ext_name' syntax to avoid this ambiguity
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_kernel.res.oracle b/tests/spec/oracle/Extend_kernel.res.oracle
deleted file mode 100644
index 80c8ec0df28d879e5e5dda6af4daa9c49b67c132..0000000000000000000000000000000000000000
--- a/tests/spec/oracle/Extend_kernel.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing Extend_kernel.i (no preprocessing)
-[kernel] Extend_kernel.i:11: User Error: 
-  Extension 'calls' from frama-c's kernel should not be used with the syntax \kernel::calls
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_type_token.res.oracle b/tests/spec/oracle/Extend_type_token.res.oracle
deleted file mode 100644
index b14752a485d1137cc1583229f04d3e595ff355a3..0000000000000000000000000000000000000000
--- a/tests/spec/oracle/Extend_type_token.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-[kernel:acsl-extension] Warning: 
-  Trying to register ACSL extension foo twice. Ignoring second extension
-[kernel] Parsing Extend_type_token.i (no preprocessing)
-[kernel] Extend_type_token.i:7: User Error: 
-  Type token 'integer' received instead of extension identifier
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/Extend_warning.res.oracle b/tests/spec/oracle/Extend_warning.res.oracle
deleted file mode 100644
index 9ba50241a6703558932aff596c850b04ed7697c0..0000000000000000000000000000000000000000
--- a/tests/spec/oracle/Extend_warning.res.oracle
+++ /dev/null
@@ -1,15 +0,0 @@
-[kernel:acsl-extension] Warning: 
-  Trying to register ACSL extension foo twice. Ignoring second extension
-[kernel] Parsing Extend_warning.i (no preprocessing)
-[kernel:extension-unknown] Extend_warning.i:7: Warning: 
-  Ignoring unregistered extension 'bar' of plug-in myplugin
-[kernel:plugin-not-loaded] Extend_warning.i:8: Warning: 
-  Ignoring extension 'bar' for unloaded plug-in unknown_plugin
-/* Generated by Frama-C */
-/*@ \myplugin::foo x ≡ 0; */
-int f(int x)
-{
-  return x;
-}
-
-
diff --git a/tests/spec/oracle/import.0.res.oracle b/tests/spec/oracle/import.0.res.oracle
index f0f5707e2ba6de2ef31dda0f96f9bc8b235a3fa2..4f812b2f7f04f7290d6821ee603f04883d600741 100644
--- a/tests/spec/oracle/import.0.res.oracle
+++ b/tests/spec/oracle/import.0.res.oracle
@@ -1,9 +1,28 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
 [test-import] Linking.
-[test-import] Registering 'foo'.
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::bar
+[kernel:acsl-extension] Registering importer extension \myplugin2::foo
 [kernel] Parsing import.i (no preprocessing)
 [test-import:7] Loading A::B.
+[test-import:15] Loading X.
+[test-import:18] Loading X::Y.
 /* Generated by Frama-C */
-/*@ import foo: A::B \as _ ;
+/*@ import \myplugin1::foo: A::B \as _ ;
  */
 /*@ predicate check1(A::B::t x) = A::B::check(x, 0);
  */
@@ -13,4 +32,14 @@
  */
 /*@ predicate check4(A::B::t x) = A::B::check(x, 0);
  */
+/*@ import \myplugin2::foo: X \as _ ;
+ */
+/*@ predicate check5(X::t x) = X::check(x, 0);
+ */
+/*@ import bar: X::Y \as _ ;
+ */
+/*@ predicate check6(X::Y::t x) = X::Y::check(x, 0);
+ */
+/*@ predicate check7(X::Y::t x) = X::Y::check(x, 0);
+ */
 
diff --git a/tests/spec/oracle/import.1.res.oracle b/tests/spec/oracle/import.1.res.oracle
index b5236c1c99d2aa32e40c018dc31bfb639b8e0beb..51394dba248fed554665362775208e42afdee295 100644
--- a/tests/spec/oracle/import.1.res.oracle
+++ b/tests/spec/oracle/import.1.res.oracle
@@ -1,22 +1,64 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
 [test-import] Linking.
-[test-import] Registering 'foo'.
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::bar
+[kernel:acsl-extension] Registering importer extension \myplugin2::foo
 [kernel] Parsing import.i (no preprocessing)
 [test-import:7] Loading A::B.
+[test-import:15] Loading X.
+[test-import:18] Loading X::Y.
 /* Generated by Frama-C */
-/*@ // import foo:
-    module A::B {
+/*@
+// import \myplugin1::foo:
+module A::B {
+  type t;
+  
+  predicate check(t x, ℤ k) ;
+  
+  }
+ */
+/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ // import \myplugin2::foo:
+    module X {
       type t;
       
       predicate check(t x, ℤ k) ;
       
       }
  */
-/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
+/*@ predicate check5(X::t x) = X::check(x, 0);
  */
-/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+/*@ // import bar:
+    module X::Y {
+      type t;
+      
+      predicate check(t x, ℤ k) ;
+      
+      }
  */
-/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+/*@ predicate check6(X::Y::t x) = X::Y::check(x, 0);
  */
-/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+/*@ predicate check7(X::Y::t x) = X::Y::check(x, 0);
  */
 
diff --git a/tests/spec/oracle/import_errors.0.res.oracle b/tests/spec/oracle/import_errors.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3b7826751f3ec0553556f2cf3ac1f8d680ff4691
--- /dev/null
+++ b/tests/spec/oracle/import_errors.0.res.oracle
@@ -0,0 +1,43 @@
+[kernel:acsl-extension] Registering acsl extension unfold
+[kernel:acsl-extension] Registering acsl extension calls
+[kernel:acsl-extension] Registering acsl extension instanceof
+[kernel:acsl-extension] Registering acsl extension \eva::widen_hints
+[kernel:acsl-extension] Registering acsl extension \eva::slevel
+[kernel:acsl-extension] Registering acsl extension \eva::unroll
+[kernel:acsl-extension] Registering acsl extension \eva::split
+[kernel:acsl-extension] Registering acsl extension \eva::merge
+[kernel:acsl-extension] Registering acsl extension \eva::dynamic_split
+[kernel:acsl-extension] Registering acsl extension \eva::subdivide
+[kernel:acsl-extension] Registering acsl extension \eva::eva_allocate
+[kernel:acsl-extension] Registering acsl extension \eva::array_partition
+[kernel:acsl-extension] Registering acsl extension \eva::eva_domain_scope
+[kernel:acsl-extension] Registering acsl extension \eva::taints
+[kernel:acsl-extension] Registering acsl extension \eva::taint
+[test-import] Linking.
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::bar
+[kernel:acsl-extension] Registering importer extension \myplugin2::foo
+[kernel:acsl-extension] Registering importer extension \myplugin1::foo
+[kernel:acsl-extension] Warning: 
+  Trying to register importer extension foo twice with plugin myplugin1. Ignoring the second extension
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel:annot-error] import_errors.c:13: Warning: 
+  unexpected token '\myplugin1::behaviors:'
+[test-import:15] Loading B.
+[kernel:annot-error] import_errors.c:21: Warning: 
+  Module B already imported with driver \myplugin1::foo (at import_errors.c:15). Ignoring global annotation
+[kernel:annot-error] import_errors.c:23: Warning: 
+  Module B already imported with driver \myplugin1::foo (at import_errors.c:15). Ignoring global annotation
+[kernel:annot-error] import_errors.c:31: Warning: 
+  Module C already defined (at import_errors.c:26). Ignoring global annotation
+/* Generated by Frama-C */
+/*@ import \myplugin1::foo: B \as _ ;
+ */
+/*@ module C {
+      type t;
+      
+      predicate check(t x, ℤ k) ;
+      
+      }
+ */
+
diff --git a/tests/spec/oracle/import_errors.1.res.oracle b/tests/spec/oracle/import_errors.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e9fce01548fc762cbcda8bedf91b1e120c58c9f5
--- /dev/null
+++ b/tests/spec/oracle/import_errors.1.res.oracle
@@ -0,0 +1,6 @@
+[test-import] Linking.
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel] import_errors.c:36: User Error: 
+  Conflicts on extension named 'foo' registered by different plugins (myplugin2,
+  myplugin1), use '\plugin::ext_name' syntax to avoid this ambiguity
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/import_errors.2.res.oracle b/tests/spec/oracle/import_errors.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5d38e6ba8805c146746a5f19e092dc31ab4f7766
--- /dev/null
+++ b/tests/spec/oracle/import_errors.2.res.oracle
@@ -0,0 +1,6 @@
+[test-import] Linking.
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel:extension-unknown] import_errors.c:40: Warning: 
+  Ignoring unregistered importer extension 'toto' of plug-in myplugin1
+[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/import_errors.3.res.oracle b/tests/spec/oracle/import_errors.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6d3621d8f3db1df1458213d7cd8a56ab66339e45
--- /dev/null
+++ b/tests/spec/oracle/import_errors.3.res.oracle
@@ -0,0 +1,6 @@
+[test-import] Linking.
+[kernel] Parsing import_errors.c (with preprocessing)
+[kernel:extension-unknown] import_errors.c:44: Warning: 
+  Ignoring unregistered importer extension 'toto'
+[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/module.1.res.oracle b/tests/spec/oracle/module.1.res.oracle
index b59f47ec8eac8cf2157e152182df5cb5a034f9e7..edccf24cec35ec507c026df1ffffc67627b35a55 100644
--- a/tests/spec/oracle/module.1.res.oracle
+++ b/tests/spec/oracle/module.1.res.oracle
@@ -7,6 +7,10 @@
   unbound logic variable b::a. Ignoring global annotation
 [kernel:annot-error] module.c:82: Warning: 
   incompatible types foo::jazz::a and foo::bar::a. Ignoring global annotation
+[kernel:annot-error] module.c:88: Warning: 
+  Duplicated module Foo (first occurrence at module.c:7). Ignoring global annotation
+[kernel:annot-error] module.c:96: Warning: 
+  Nested module and axiomatic. Ignoring body of Bar. Ignoring global annotation
 /* Generated by Frama-C */
 /*@
 module Foo {
diff --git a/tests/spec/import.ml b/tests/spec/test_import.ml
similarity index 51%
rename from tests/spec/import.ml
rename to tests/spec/test_import.ml
index ca99db7c9845d4dee600b58794a88ec373f6402c..08eb2eab11d305c31678f11479c5bf113cfb9c69 100644
--- a/tests/spec/import.ml
+++ b/tests/spec/test_import.ml
@@ -1,6 +1,23 @@
 open Cil_types
 open Logic_typing
 
+
+module Plugin1 =
+  Plugin.Register
+    (struct
+      let name = "MyPlugin1"
+      let shortname = "myplugin1"
+      let help = ""
+    end)
+
+module Plugin2 =
+  Plugin.Register
+    (struct
+      let name = "MyPlugin2"
+      let shortname = "myplugin2"
+      let help = ""
+    end)
+
 let () = Format.printf "[test-import] Linking.@."
 
 let loader (ctxt: module_builder) (loc: location) (m: string list) =
@@ -17,9 +34,10 @@ let loader (ctxt: module_builder) (loc: location) (m: string list) =
   end
 
 let register () =
-  begin
-    Format.printf "[test-import] Registering 'foo'.@." ;
-    Acsl_extension.register_module_importer "foo" loader ;
-  end
+  Acsl_extension.register_module_importer ~plugin:"myplugin1" "foo" loader;
+  Acsl_extension.register_module_importer ~plugin:"myplugin1" "bar" loader;
+  Acsl_extension.register_module_importer ~plugin:"myplugin2" "foo" loader;
+  if Kernel.GeneralDebug.get () = 1 then
+    Acsl_extension.register_module_importer ~plugin:"myplugin1" "foo" loader
 
 let () = Cmdline.run_after_extended_stage register