diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index ab52d0e4172a463551bc077c473c1306fb0e39bc..4ce9e948e29de1c21f184f401c6168901f8de54d 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -49,7 +49,7 @@ else
 		-load-script ./examples/acsl_extension \
 		-load-script ./hello_world/hello_world.ml \
        | tee check.log
-	if grep -e "user error" check.log; then \
+	if grep -e "User Error" check.log; then \
            echo "Examples script do not compile with current Frama-C."; \
            echo "Please examine check.log and make appropriate changes"; \
            exit 1; \
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 143998fb5bafd5450637a72f3459223a9e3d69de..d6dceaa1bf73026c3a1f3f6ba952b3c59e8b5504 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1062,8 +1062,8 @@ or
   line. Once such a directive has been encountered, each occurrence of
   \texttt{@macro-name@} in a \texttt{CMD}, \texttt{LOG}, \texttt{OPT},
   \texttt{STDOPT} or \texttt{EXECNOW} directive at this configuration level
-  or in any level below it will be replaced by \texttt{content}. Existing 
-  pre-defined macros are listed in section~\ref{sec:ptests-macros}.
+  or in any level below it will be replaced by \texttt{content}. Existing
+  pre-defined macros are listed in section~\ref{sec:ptests-macros}. 
 \item The \texttt{FILEREG}\sscodeidxdef{Test}{Directive}{FILEREG}
   directive contains a regular expression indicating which files in
   the directory containing the current test suite are actually part of
@@ -1072,6 +1072,14 @@ or
   configuration file.
 \end{itemize}
 
+\begin{important}
+\paragraph{\texttt{@} in the text of a directive}
+As mentioned above, \texttt{@} is recognized by \ptests as the beginning of
+a macro. If you need to have a literal \texttt{@} in the text of the directive
+itself, it needs to be doubled, {\it i.e.} \texttt{@@} will be translated as
+\texttt{@}.
+\end{important}
+
 \begin{important}
   \textbf{Summary: ordering of test executions}
 
@@ -3918,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}
@@ -3933,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 9cea38cf3336f6cfee986e8aa135ac3e60aca6f6..41a4ee2c9fcad9a77f029873c808627b60b45efe 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -7,6 +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/doc/developer/examples/acsl_extension.ml b/doc/developer/examples/acsl_extension.ml
index b4848615dd58d2c19e6d4e1bb5d098f0a820d044..9c677e002004f551f2cbfe95d296cdc3caa23997 100644
--- a/doc/developer/examples/acsl_extension.ml
+++ b/doc/developer/examples/acsl_extension.ml
@@ -14,4 +14,4 @@ let type_foo ~typing_context ~loc:_loc l =
   in
   Ext_terms res
 
-let () = Logic_typing.register_behavior_extension "foo" type_foo
+let () = Logic_typing.register_behavior_extension "foo" false type_foo
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 61d3b38decb7b848f2810cfc9d23433148f28fe0..d99f688a4ac700f140617be5cb866a6d4711002d 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -493,7 +493,7 @@ end = struct
 
 end
 
-let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]+\\)@\\(.*\\)"
+let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]*\\)@\\(.*\\)"
 
 type execnow =
     {
@@ -585,15 +585,19 @@ let replace_macros macros s =
       let rest = Str.matched_group 3 s in
       let new_n = Str.group_end 1 in
       let n, new_s =
-        try
-          if !verbosity >= 2 then lock_printf "macro is %s\n%!" macro;
-          let replacement =  StringMap.find macro macros in
-          if !verbosity >= 1 then
-            lock_printf "replacement for %s is %s\n%!" macro replacement;
-          new_n,
-          String.sub s 0 n ^ start ^ replacement ^ rest
-        with
+        if macro = "" then begin
+          new_n + 1, String.sub s 0 new_n ^ "@" ^ rest
+        end else begin
+          try
+            if !verbosity >= 2 then lock_printf "macro is %s\n%!" macro;
+            let replacement =  StringMap.find macro macros in
+            if !verbosity >= 1 then
+              lock_printf "replacement for %s is %s\n%!" macro replacement;
+            new_n,
+            String.sub s 0 n ^ start ^ replacement ^ rest
+          with
           | Not_found -> Str.group_end 2 + 1, s
+        end
       in
        if !verbosity >= 2 then lock_printf "new string is %s\n%!" new_s;
       let new_acc = ptest_file_matched, new_s in
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 ->
diff --git a/tests/rte/twofunc3.c b/tests/rte/twofunc3.c
index b7102aaf7086db45e0bfbf0924a346a8edab1bcb..fab3e66a5abf45ebcf5d3ea1c88983614b468ef6 100644
--- a/tests/rte/twofunc3.c
+++ b/tests/rte/twofunc3.c
@@ -1,6 +1,6 @@
 /* run.config
    EXECNOW: make -s @PTEST_DIR@/rte_api/rte_get_annot.cmxs
-   OPT: -load-module @PTEST_DIR@/rte_api/rte_get_annot -journal-disable
+   OPT: -rte-select @@all -load-module @PTEST_DIR@/rte_api/rte_get_annot -journal-disable
 */