diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 1940518ffe3bb21b2931d57d51ef298dd09eb705..bf66ceccfdaf5daf3e4c883cca46b4e7c047e0ec 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -318,7 +318,7 @@
     | IDENTIFIER s ->
       if Plugin.is_present plugin then
         Kernel.warning ~once:true ~wkey:Kernel.wkey_extension_unknown ~source
-          "Unregistered extension %s for plug-in %s" s plugin
+          "Unregistered extension '%s' for plug-in %s" s plugin
       else
         Kernel.warning ~once:true ~wkey:Kernel.wkey_plugin_not_loaded ~source
           "Ignored extensions for unloaded plug-in %s" plugin;
@@ -328,9 +328,13 @@
     | EXT_GLOBAL_BLOCK s
     | EXT_CONTRACT s ->
       let plugin_from = Logic_env.extension_from s in
+      if plugin_from = plugin && plugin = "kernel" then
+        Kernel.abort ~source
+          "Extension '%s' from frama-c's kernel should not be used with the syntax \
+          \\kernel::%s" s s;
       if plugin_from <> plugin then
         Kernel.abort ~source
-          "Extension %s is from %s and not %s" s plugin_from plugin;
+          "Extension '%s' is from %s and not %s" s plugin_from plugin;
       tok
     | _ ->
       Kernel.abort ~source
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index b22e748f786d374dafa9144de16288d89120468d..e50accda3665485cc4fb50bcbf959f9bf61350ea 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -191,12 +191,17 @@ module Extensions = struct
   let print name printer fmt kind =
     let ext_common = find_common name in
     let plugin = ext_common.plugin in
+    let full_name =
+      if Datatype.String.equal plugin "kernel" then name
+      else
+        Format.sprintf "\\%s::%s" plugin name
+    in
     let pp = ext_common.printer printer in
     match kind with
     | Ext_annot (id,_) ->
-      Format.fprintf fmt "@[<v 2>@[\\%s::%s %s {@]@\n%a}@]" plugin name id pp kind
+      Format.fprintf fmt "@[<v 2>@[%s %s {@]@\n%a}@]" full_name id pp kind
     | _ ->
-      Format.fprintf fmt "@[<hov 2>\\%s::%s %a;@]" plugin name pp kind
+      Format.fprintf fmt "@[<hov 2>%s %a;@]" full_name pp kind
 
   let short_print name printer fmt kind =
     let pp = (find_common name).short_printer in
diff --git a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
index 28c7599a5a849e737c035d64b34f18d7d7352fd4..f0391a4fd077e704388470a183efd48c1060b6b3 100644
--- a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
@@ -508,10 +508,10 @@ int main(int c)
   int __retres;
   /*@ ghost main_pre_func(c); */
   if (c) pf = & f; else pf = & g;
-  /*@ \kernel::calls f, g; */
+  /*@ calls f, g; */
   (*pf)();
   if (c) pf = & g; else pf = & f;
-  /*@ \kernel::calls f, g; */
+  /*@ calls f, g; */
   (*pf)();
   __retres = 0;
   /*@ ghost main_post_func(__retres); */
diff --git a/tests/spec/Extend_kernel.i b/tests/spec/Extend_kernel.i
new file mode 100644
index 0000000000000000000000000000000000000000..a53a4fe67fd5e8890a93c7887ddaa6fb1a50d49e
--- /dev/null
+++ b/tests/spec/Extend_kernel.i
@@ -0,0 +1,13 @@
+/* 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/oracle/Extend_conflict.res.oracle b/tests/spec/oracle/Extend_conflict.res.oracle
index f483db984ec30e916c96eb5155ead8a523abbb32..ae562310f5f3e42f74fba518fc11712b7ef73f59 100644
--- a/tests/spec/oracle/Extend_conflict.res.oracle
+++ b/tests/spec/oracle/Extend_conflict.res.oracle
@@ -2,5 +2,5 @@
   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
+  Extension 'foo' is from myplugin and not eva
 [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
new file mode 100644
index 0000000000000000000000000000000000000000..80c8ec0df28d879e5e5dda6af4daa9c49b67c132
--- /dev/null
+++ b/tests/spec/oracle/Extend_kernel.res.oracle
@@ -0,0 +1,4 @@
+[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_warning.res.oracle b/tests/spec/oracle/Extend_warning.res.oracle
index e897425bd86a1d476c6219130006d1103378cd11..204dbfafe718e623046dedc8491f09593eaeba18 100644
--- a/tests/spec/oracle/Extend_warning.res.oracle
+++ b/tests/spec/oracle/Extend_warning.res.oracle
@@ -2,7 +2,7 @@
   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: 
-  Unregistered extension bar for plug-in myplugin
+  Unregistered extension 'bar' for plug-in myplugin
 [kernel:plugin-not-loaded] Extend_warning.i:8: Warning: 
   Ignored extensions for unloaded plug-in unknown_plugin
 /* Generated by Frama-C */