From 1e3b09425e04e3be2503cca0b59226be711e3fb1 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 4 Sep 2024 18:59:08 +0200
Subject: [PATCH] [kernel] Better warning messages for acsl extensions
---
src/kernel_internals/parsing/logic_lexer.mll | 4 ++--
tests/spec/oracle/Extend_warning.res.oracle | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 70a9d8cc29d..5e118c127e8 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -310,10 +310,10 @@
| 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
+ "Ignoring unregistered extension '%s' of 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;
+ "Ignoring extension '%s' for unloaded plug-in %s" s plugin;
IDENTIFIER_EXT s
| EXT_CODE_ANNOT s
| EXT_GLOBAL s
diff --git a/tests/spec/oracle/Extend_warning.res.oracle b/tests/spec/oracle/Extend_warning.res.oracle
index 204dbfafe71..9ba50241a67 100644
--- a/tests/spec/oracle/Extend_warning.res.oracle
+++ b/tests/spec/oracle/Extend_warning.res.oracle
@@ -2,9 +2,9 @@
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
+ Ignoring unregistered extension 'bar' of plug-in myplugin
[kernel:plugin-not-loaded] Extend_warning.i:8: Warning:
- Ignored extensions for unloaded plug-in unknown_plugin
+ Ignoring extension 'bar' for unloaded plug-in unknown_plugin
/* Generated by Frama-C */
/*@ \myplugin::foo x ≡ 0; */
int f(int x)
--
GitLab