From 4f16554b58dd3b838e31bbab75bd081af9996d78 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 20 Feb 2024 18:05:04 +0100
Subject: [PATCH] Refuse/Do not print new syntax for kernel extensions
---
src/kernel_internals/parsing/logic_lexer.mll | 8 ++++++--
src/kernel_services/ast_queries/acsl_extension.ml | 9 +++++++--
.../aorai/tests/ya/oracle/function_ptr.res.oracle | 4 ++--
tests/spec/Extend_kernel.i | 13 +++++++++++++
tests/spec/oracle/Extend_conflict.res.oracle | 2 +-
tests/spec/oracle/Extend_kernel.res.oracle | 4 ++++
tests/spec/oracle/Extend_warning.res.oracle | 2 +-
7 files changed, 34 insertions(+), 8 deletions(-)
create mode 100644 tests/spec/Extend_kernel.i
create mode 100644 tests/spec/oracle/Extend_kernel.res.oracle
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 1940518ffe3..bf66ceccfda 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 b22e748f786..e50accda366 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 28c7599a5a8..f0391a4fd07 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 00000000000..a53a4fe67fd
--- /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 f483db984ec..ae562310f5f 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 00000000000..80c8ec0df28
--- /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 e897425bd86..204dbfafe71 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 */
--
GitLab