From 3518e275f32bfb19c1a273b7ebcfa131c0672c26 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 25 Feb 2019 18:54:59 +0100
Subject: [PATCH] [devman] document ptests update
---
doc/developer/advance.tex | 12 ++++++++++--
doc/developer/changes.tex | 1 +
2 files changed, 11 insertions(+), 2 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 143998fb5ba..f6889b211e8 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}
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 9cea38cf333..6e3243e90cf 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -7,6 +7,7 @@ This chapter summarizes the major changes in this documentation between each
\section*{Frama-C+dev}
\begin{itemize}
+\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
\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}
--
GitLab