diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 7763e2d7650dbe7d97224e6c16ab0a0dd88b184f..1f8932359316c700ca728840c37ff5ead4719ebd 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 cbece5ab43e7ba9114065fea0a77882b5244660c..7ae80ec8fab481029d614b6189111ade287e21c1 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 222fd58a7509a24fefe4b47c07ca1a06134bb1e5..20c0eaa647cc4ad9b6b9352394bbfa3014336507 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