From fc9d8662d2e7dedea4c0a6d8a158eb2cc9f51812 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 16 Jul 2020 17:55:41 +0200
Subject: [PATCH] [devman] documentation for NOFRAMAC
---
doc/developer/advance.tex | 17 ++++++++++++++---
doc/developer/changes.tex | 10 ++++++++--
doc/developer/tutorial.tex | 4 ++--
3 files changed, 24 insertions(+), 7 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index b72c6e159f1..2489c968a19 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 8abcd5df6a1..2230467a8ad 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 457004dd0a5..93fb2b73b80 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.
--
GitLab