[devman] fixes version in Change section + doc `status` flag in ACSL extensions

doc/developer/advance.tex

@@ -3926,7 +3926,7 @@ the corresponding list is traversed normally by the visitor
 (see section~\ref{adv:visitors}).
 
 In order for the extension to be recognized by the parser, it must be
-registered by one of the following functions, depending on its category:
+registered by one of the following functions, depending on its category.
 \begin{itemize}
 \item \texttt{Logic\_typing.register\_behavior\_extension}%
 \scodeidx{Logic\_typing}{register\_behavior\_extension}
@@ -3941,6 +3941,15 @@ registered by one of the following functions, depending on its category:
 \item \texttt{Logic\_typing.register\_code\_annot\_next\_both\_extension}%
 \scodeidx{Logic\_typing}{register\_code\_annot\_next\_loop\_extension}
 \end{itemize}
+
+Each function takes three arguments:
+\begin{itemize}
+\item \texttt{kw} the name of the extension,
+\item \texttt{status}, a boolean flag indicating whether the extended annotation
+  may have a validity status, and
+\item \texttt{f} the type-checking function itself.
+\end{itemize}
+
 After a call to the appropriate registration function,
 a clause of the form \verb|kw e1,...,en;|, where each \verb|ei| can be
 any syntactically valid ACSL term or predicate,

doc/developer/changes.tex

@@ -7,7 +7,12 @@ This chapter summarizes the major changes in this documentation between each
 
 \section*{Frama-C+dev}
 \begin{itemize}
+\item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
 \item \textbf{Testing}: Document of usage \texttt{@@} in a directive
+\end{itemize}
+
+\section*{18.0 Argon}
+\begin{itemize}
 \item \textbf{Logging Services}: Document \texttt{error} and \texttt{failure} behaviors.
 \item \textbf{ACSL Extensions}: New extension categories, for global and plain code annotations
 \end{itemize}

src/kernel_services/ast_queries/logic_typing.mli

@@ -172,6 +172,7 @@ type typing_context = {
 
     @since Carbon-20101201
     @modify Silicon-20161101 change type of the function
+    @Frama-C+dev add [status] argument
 *)
 val register_behavior_extension:
   string -> bool ->