From 398d4c79f0fcec11b1d800f0ce977b64fe17dde2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 26 Jul 2019 18:40:47 +0200
Subject: [PATCH] [doc] expand a little bit the documentation of MODULE ptests'
directive
---
doc/developer/advance.tex | 11 +++++++++--
1 file changed, 9 insertions(+), 2 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index bb9770b2580..76c7992b597 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -993,7 +993,7 @@ the sequence above is read in order and defines a configuration level
\begin{itemize}
\item
- \texttt{CMD} allows to change the command that is used for the
+ \texttt{CMD} allows changing the command that is used for the
following \texttt{OPT} directives (until a new \texttt{CMD}
directive is found). No new test case is generated
if there is no further \texttt{OPT} directive. At a given
@@ -1068,7 +1068,14 @@ or
\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}.
+ pre-defined macros are listed in section~\ref{sec:ptests-macros}.
+\item \texttt{MODULE}\nscodeidx{Test!Directive}{MODULE}
+ directive takes as argument the name of a \texttt{.cmxs}
+ module. It will then add a directive to compile this file with the
+ command \texttt{@PTEST\_MAKE\_MODULE@ <MODULE>} where
+ \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 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
--
GitLab