diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index f6889b211e87aa0308445dd162a9c19002432f03..d6dceaa1bf73026c3a1f3f6ba952b3c59e8b5504 100644
--- a/doc/developer/advance.tex
+++ b/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,
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 6e3243e90cf7d9ccafd1efb318c0ca05e7b19777..41a4ee2c9fcad9a77f029873c808627b60b45efe 100644
--- a/doc/developer/changes.tex
+++ b/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}
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index a05bd2a0ebba3432098286cae6c3596702b3463c..c204d9df8e233d2970b951de6848ad4b04e0c0eb 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/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 ->