diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll index 70a9d8cc29de5daa1f27bc9ad387494a30ea1039..5e118c127e815d5750f7737124fe3cb8fcbb6ce3 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 204dbfafe718e623046dedc8491f09593eaeba18..9ba50241a6703558932aff596c850b04ed7697c0 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)