[doc] Add userman section on ACSL extension syntaxes

doc/userman/user-acsl.tex

 \chapter{ACSL extensions} % here we do not use the macro (avoids a warning)
 \label{cha:acsl-extensions}
+\section{Extension syntaxes}
+\label{acsl:syntax}
+
+When a plug-in registers an extension, it can be used in \acsl annotations
+with 2 different syntaxes. As an example, with an extension \lstinline|bar|
+registered by the plug-in \lstinline|foo|, we can use the short syntax
+\lstinline|bar _| and the complete syntax \lstinline|\foo::bar _|.
+
+The complete syntax is usefull to print better warning/error messages, and to
+better understand which plug-in introduced the extension. Additionnaly, all
+extensions coming from an unloaded plug-in can be ignored this way. For
+example, if \Eva is not loaded, \lstinline|\eva::unroll _| annotations will be
+ignored with a warning, unlike \lstinline|unroll _| which by default will be
+treated as a user error. 
+
 \section{Handling indirect calls with \texttt{calls}}
 \label{acsl:calls}
 

src/kernel_internals/parsing/logic_lexer.mll

@@ -321,7 +321,7 @@
           "Unregistered extension %s for plug-in %s" s plugin
       else
         Kernel.warning ~once:true ~wkey:Kernel.wkey_plugin_not_loaded ~source
-          "Ignored extensions for unregistered plug-in %s" plugin;
+          "Ignored extensions for unloaded plug-in %s" plugin;
       IDENTIFIER_EXT s
     | EXT_CODE_ANNOT s
     | EXT_GLOBAL s
@@ -594,8 +594,7 @@ and comment = parse
       | Logic_utils.Not_well_formed (loc, m) ->
         output ~source:(fst loc) "%s" m;
         None
-      | Logic_utils.Unknown_ext ->
-        None
+      | Logic_utils.Unknown_ext -> None
       | Log.FeatureRequest(source,_,msg) ->
         let source = Option.value ~default:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) source in
         output ~source "unimplemented ACSL feature: %s" msg; None

tests/spec/oracle/Extend_warning.res.oracle

@@ -4,7 +4,7 @@
 [kernel:extension-unknown] Extend_warning.i:7: Warning: 
   Unregistered extension bar for plug-in myplugin
 [kernel:plugin-not-loaded] Extend_warning.i:8: Warning: 
-  Ignored extensions for unregistered plug-in unknown_plugin
+  Ignored extensions for unloaded plug-in unknown_plugin
 /* Generated by Frama-C */
 /*@ \myplugin::foo x ≡ 0; */
 int f(int x)