From b924bdb9479128fe6b60e938b8f49bcdfb766034 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 12 Oct 2021 14:23:11 +0200
Subject: [PATCH] [Ptests] updates the developper manual
---
doc/developer/advance.tex | 7 +++++++
doc/developer/changes.tex | 2 +-
doc/developer/refman.tex | 6 +++++-
3 files changed, 13 insertions(+), 2 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 7763e2d7650..1f893235931 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -958,6 +958,10 @@ the configuration header of a test (or a test suite).
& Plugins to be loaded with each subsequent run.
& \texttt{from inout eva scope variadic} for tests under \texttt{./tests} directory
\\
+& \texttt{LIBS}\nscodeidxdef{Test!Directive}{LIBS}
+& Libraries to be loaded with each subsequent run (their compilation is not managed by \texttt{ptests} contrary to the modules of \texttt{MODULE} directive).
+& \textit{None}
+\\
& \texttt{CMD}\nscodeidxdef{Test!Directive}{CMD}
& Program to run
& \texttt{./bin/toplevel.opt}
@@ -1166,6 +1170,9 @@ or
\texttt{@PTEST\_MAKE\_MODULE@} defaults to \texttt{make -s}. Option
\texttt{-load-module <MODULE>} will then be appended to any subsequent Frama-C
command triggered by the test.
+\item \texttt{LIBS}\nscodeidx{Test!Directive}{LIBS}
+ directive takes as argument the name of a \texttt{.cmxs}
+ module. The \texttt{-load-module <LIBS>} will then be appended to any subsequent Frama-C command triggered by the test. The compilation is not managed by \texttt{ptests}.
\item The \texttt{FILEREG}\nscodeidx{Test!Directive}{FILEREG}
directive contains a regular expression indicating which files in
the directory containing the current test suite are actually part of
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index cbece5ab43e..7ae80ec8fab 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -7,7 +7,7 @@ This chapter summarizes the major changes in this documentation between each
\section*{dev}
\begin{itemize}
-\item \textbf{Testing}: Document new directive \texttt{PLUGIN} and new predefined macros for \texttt{ptests}.
+\item \textbf{Testing}: Document new directives (\texttt{PLUGIN} and \texttt{LIBS}) and new predefined macros for \texttt{ptests}.
\end{itemize}
\section*{22.0 Titanium}
diff --git a/doc/developer/refman.tex b/doc/developer/refman.tex
index 222fd58a750..20c0eaa647c 100644
--- a/doc/developer/refman.tex
+++ b/doc/developer/refman.tex
@@ -871,15 +871,19 @@ one for regular tests (if more than one \verb|OPT|).\\
\hline
\verb|PTEST_MODULE| & current list of module defined by the \verb|MODULE| directive\\
\hline
+\verb|PTEST_LIBS| & current list of module defined by the \verb|LIBS| directive\\
+\hline
\verb|PTEST_PLUGIN| & current list of plugins defined by the \verb|PLUGIN| directive\\
\hline
\verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-journal-disable| \verb|-check| \verb|-no-autoload-plugins|\\
\hline
\verb|PTEST_LOAD_MODULE| & the \verb|-load-module| option related to the \verb|MODULE| directive\\
\hline
+\verb|PTEST_LOAD_LIBS| & the \verb|-load-module| option related to the \verb|LIBS| directive\\
+\hline
\verb|PTEST_LOAD_PLUGIN| & the \verb|-load-module| option related to the \verb|PLUGIN| directive\\
\hline
-\verb|PTEST_LOAD_OPTIONS| & shorthand alias to \spverb|@PTEST_LOAD_PLUGIN@ @PTEST_LOAD_MODULE@|\\
+\verb|PTEST_LOAD_OPTIONS| & shorthand alias to \spverb|@PTEST_LOAD_PLUGIN@ @PTEST_LOAD_LIBS@ @PTEST_LOAD_MODULE@|\\
\hline
\verb|PTEST_OPTIONS| & the current list of options related to \verb|OPT| and \verb|STDOPT| directives (for \verb|CMD| directives)\\
\hline
--
GitLab