diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index b72c6e159f18d91636b3c4064b7b6db58b1ea0c8..2489c968a1927c694a9065eb189fe51d7caf914d 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -994,6 +994,11 @@ test
 & kill the test after the given duration and report a failure
 & \textit{None}
 \\
+& \texttt{NOFRAMAC}\nscodeidxdef{Test!Directive}{NOFRAMAC}
+& empty the list of frama-c commands to be launched
+(\texttt{EXEC} and \texttt{EXECNOW} directives are still executed).
+& \textit{None}
+\\
 \hline \multirow{2}{23mm}{\centering{Test suite}}
 & \texttt{DONTRUN}\nscodeidxdef{Test!Directive}{DONTRUN}
 & Do not execute this test
@@ -1021,11 +1026,17 @@ test
 Any directive can identify a file using a relative path.
 The default directory considered for \texttt{.} is always the parent
 directory of directory \texttt{tests}\codeidx{tests}. The
-\texttt{DONTRUN} directive does not need to have any content, but it
-is useful to provide an explanation of why the test should not be run
-({\it e.g} test of a feature that is currently developed and not fully
+\texttt{DONTRUN} and \texttt{NOFRAMAC} directives
+do not need to have any content, but it might be
+useful to provide an explanation of why the test should not be run
+({\it e.g} test of a feature that is under development and not fully
 operational yet).
 
+If there are \texttt{OPT}/\texttt{STDOPT} directives \textit{after} a
+\texttt{NOFRAMAC} directive, they will be executed, unless
+they are themselves discarded by another subsequent \texttt{NOFRAMAC}
+directive.
+
 As said in Section~\ref{ptests:configuration}, these directives can be
 found in different places:
 \begin{enumerate}
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 8abcd5df6a1cd67926d25c5ce1f67f9767945b43..2230467a8ad62f1b5512330c647279b02c6a2b70 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -5,6 +5,12 @@
 This chapter summarizes the major changes in this documentation between each
 \framac release, from newest to oldest.
 
+\section*{Frama-C+dev}
+\begin{itemize}
+\item \textbf{Testing}: Document new directives \texttt{TIMEOUT} and
+\texttt{NOFRAMAC}
+\end{itemize}
+
 \section*{21.0 Scandium}
 \begin{itemize}
 \item \textbf{Configure}: Documentation of \texttt{configure\_pkg},
@@ -13,13 +19,13 @@ This chapter summarizes the major changes in this documentation between each
 
 \section*{20.0 Calcium}
 \begin{itemize}
-\item \textbf{Ptests}: Documentation of the new directive \texttt{MODULE}.
+\item \textbf{Testing}: Documentation of the new directive \texttt{MODULE}.
 \end{itemize}
 
 \section*{19.0 Potassium}
 \begin{itemize}
 \item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
-\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
+\item \textbf{Testing}: Document usage of \texttt{@@} in a directive
 \item \textbf{Profiling with Landmarks}: New section
 \end{itemize}
 
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 457004dd0a5643c0c65fbd40384b55d8085f3e9c..93fb2b73b8082593784f4a27498f584285773672 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -548,11 +548,11 @@ For this tutorial, there will be no such source code. A file
 \texttt{./tests/hello/hello\_test.c} is then created:
 
 \listingname{./tests/hello/hello\_test.c}
-\sscodeidx{Test}{Directive}{OPT}
+\nscodeidx{Test!Directive}{OPT}
 \lstinputlisting[style=c]{./tutorial/hello/generated/with_test/tests/hello/hello_test.c}
 
 In this file, there is only one directive
-\texttt{OPT: -hello}\sscodeidx{Test}{Directive}{OPT} which requires
+\texttt{OPT: -hello}\nscodeidx{Test!Directive}{OPT} which requires
 to run \framac on this test with the \texttt{-hello} option.
 A look at Section~\ref{ptests:directives} gives you an idea of the kind of
 directives which can be used to test plug-ins.