diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 1f8932359316c700ca728840c37ff5ead4719ebd..132d43441a24706cb11501a00a7ae7aa72a56900 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{SCRIPT}\nscodeidxdef{Test!Directive}{SCRIPT} +& ML scripts to be loaded with each subsequent run (their compilation is performed by the \texttt{frama-c] command). +& \textit{None} +\\ & \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} @@ -1173,6 +1177,9 @@ or \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 \texttt{SCRIPT}\nscodeidx{Test!Directive}{SCRIPT} + directive takes as argument the name of a \texttt{.ml} + file. The \texttt{-load-script <SCRIPT>} will then be appended to any subsequent Frama-C command triggered by the test. \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 7ae80ec8fab481029d614b6189111ade287e21c1..0060a75cda8dfa2308dca5e503acbdd5ac89e1fc 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 directives (\texttt{PLUGIN} and \texttt{LIBS}) and new predefined macros for \texttt{ptests}. +\item \textbf{Testing}: Document new directives (\texttt{PLUGIN}, \texttt{SCRIPT} 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 20c0eaa647cc4ad9b6b9352394bbfa3014336507..3c0f1ec51989d413c9cfab797fc2dc0a1e29f0dc 100644 --- a/doc/developer/refman.tex +++ b/doc/developer/refman.tex @@ -875,6 +875,8 @@ one for regular tests (if more than one \verb|OPT|).\\ \hline \verb|PTEST_PLUGIN| & current list of plugins defined by the \verb|PLUGIN| directive\\ \hline +\verb|PTEST_SCRIPT| & current list of plugins defined by the \verb|SCRIPT| 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\\ @@ -883,7 +885,9 @@ one for regular tests (if more than one \verb|OPT|).\\ \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_LIBS@ @PTEST_LOAD_MODULE@|\\ +\verb|PTEST_LOAD_SCRIPT| & the \verb|-load-script| option related to the \verb|SCRIPT| directive\\ +\hline +\verb|PTEST_LOAD_OPTIONS| & shorthand alias to \spverb|@PTEST_LOAD_PLUGIN@ @PTEST_LOAD_LIBS@ @PTEST_LOAD_MODULE@ @PTEST_LOAD_SCRIPT@|\\ \hline \verb|PTEST_OPTIONS| & the current list of options related to \verb|OPT| and \verb|STDOPT| directives (for \verb|CMD| directives)\\ \hline