advance.tex

%%% Local Variables:
%%% TeX-master: "developer.tex"
%%% ispell-local-dictionary: "english"
%%% End:

\chapter{Advanced Plug-in Development}\label{chap:advance}
\lstset{language=Ocaml} %% makes Ocaml the default language for listings, eg. \lstinline.

This chapter details how to use services provided by \framac in order to be
fully operational with the development of plug-ins. Each section describes
technical points a developer should be aware of. Otherwise,
one could find oneself in one or more of the following situations
\footnote{It
  is fortunately quite difficult (but not impossible) to fall into the worst
  situation by mistake if you are not a kernel developer.}
(from bad to worse):
\begin{enumerate}
\item reinventing the (\framac) wheel;
\item being unable to do some specific things (\eg saving
  results\index{Saving} of an analysis on disk, see
  Section~\ref{proj:states});
\item introducing bugs in his/her code;
\item introducing bugs in other plug-ins using his/her code;
\item breaking the kernel consistency\index{Consistency} and so potentially
  breaking all \framac plug-ins (\eg if s/he modifies the
  AST\index{AST!Modification} without changing project\index{Project}, see
  Section~\ref{proj:use}).
\end{enumerate}

In this chapter, we suppose that the reader is able to write a minimal plug-in
like \texttt{hello}\index{Hello} described in chapter~\ref{chap:tutorial} and
knows about the software architecture of \framac (chapter~\ref{chap:archi}). Moreover
plug-in development requires the use of advanced features of
\caml (module system, classes and objects, \emph{etc}).
Plug-in development also requires some familiarity with the Dune build system.

Note that the following subsections can be read in no particular
order: their contents are indeed quite independent from one another even if
there are references from one section to another one.

\section{Plug-in dependencies}\label{adv:dependencies}

\begin{target}standard plug-in developers.\end{target}

\begin{prereq}
  Basic knowledge of the Dune build system.
\end{prereq}

Some plug-ins only depend on the \framac kernel, and in this case, require no
special configuration. However, many plug-ins depend either on other \framac
plug-ins, or on external libraries, tools and components. In both cases, it is
important to specify such dependencies, to avoid the user trying and failing
to compile or run your plug-in.

Plug-in dependencies are usually defined in the plug-in's \verb|dune| file.
There are mainly two kinds of dependencies: {\em mandatory} and {\em optional}.
Mandatory dependencies are necessary for the plug-in to run {\em at all}, and
their absence means the plug-in must be disabled. Optional dependencies do not
prevent compilation and usage of the plug-in, but it may work less efficiently,
precisely, or fail when specific features are requested.

\begin{important}
  Plug-in developers must ensure that optional dependencies are tested for
  their absence and dealt with gracefully; a plug-in must {\em not} crash when
  optional dependencies are missing.
\end{important}

Most dependencies (OCaml library dependencies, such as other plug-ins or OCaml
modules) are specified using Dune's \verb|library| stanza%
\footnote{Full documentation about Dune's \texttt|library| stanza is available
at \url{https://dune.readthedocs.io/en/stable/concepts.html\#library-deps}}.
As is often the case, examples are very instructive; here is an example of
mandatory dependencies from the \textsf{Dive} plug-in's \verb|dune| file:

\begin{lstlisting}
(library
  [...]
  (libraries frama-c.kernel frama-c-studia.core frama-c-server.core)
)
\end{lstlisting}

The \verb|libraries| field contains \verb|frama-c.kernel| (essential for all
plug-ins), but also \verb|frama-c-studia.core| and \verb|frama-c-server.core|,
meaning this plug-in requires both the \textsf{Studia} and \textsf{Server}
plug-ins to be enabled. If any of them is disabled (either due to
missing dependencies, or as a result of a user request), then \textsf{Dive}
will also be disabled.

{\em Note: to explicitly disable a plug-in, use the
  \verb|dev/disable-plugins.sh| script.}

Note that OCaml libraries can also be specified, e.g. adding \verb|zarith|
to \verb|libraries| above would require that Zarith be installed and available
via \verb|ocamlfind|.

\subsection{Declaring dependencies}

Optional dependencies can be detected and disabled in different ways:

\begin{itemize}
\item If the module is dynamically accessible via \verb|Db| (see
  Section~\ref{adv:static-registration} for more details), the detection
  can be done directly in OCaml and requires no special handling in the
  \verb|dune| file;
\item Otherwise, you can define two versions of the implementation
  (both implementing the same interface), in two different files.
  One of these files will use the required module, while the other will
  implement a dummy version without it.
  The \verb|select| notation from the \verb|library| stanza allows telling
  Dune which file to compile.
\end{itemize}

Here is an example of \verb|select| from the \textsf{Aoraï} plug-in,
which defines an optional dependency on the \textsf{Eva} plug-in:

\begin{lstlisting}
(libraries [...]
 (select aorai_eva_analysis.ml from
  (frama-c-eva.core -> aorai_eva_analysis.enabled.ml)
  (  -> aorai_eva_analysis.disabled.ml)
 )
\end{lstlisting}

In the example above, \textsf{Aoraï} defines two files:
\verb|aorai_eva_analysis.enabled.ml| and \verb|aorai_eva_analysis.disabled.ml|
(we recommend this naming convention, but it is not enforced by \verb|dune|).
The general form of the \verb|select| stanza is:

\begin{lstlisting}
(select <file> from
  (<cond_1> -> <file_1>)
  (<cond_2> -> <file_2>)
  ...
  ( -> <default>)
)
\end{lstlisting}

It then checks for each condition \verb|<cond_i>| in order, and the first one
that matches is selected, otherwise it will be the fallback/default one. The
selected \verb|<file_i>| will be renamed to \verb|<file>| and used in the build.

\subsection{Notifying users via frama-c-configure}

\framac has a special Dune target, \verb|@frama-c-configure|, which prints a
summary of the configuration as seen by Dune when run via
\verb|dune build @frama-c-configure|. It is especially helpful to
understand why a given plug-in is disabled.

Plug-in developers should {\em always} include such a section in their
\verb|dune| file, listing each optional library and its current availability,
via the \verb|%{lib-available:<lib>}| special variable.

Here is an example from \textsf{Frama-Clang}, which requires the following
libraries:

\begin{lstlisting}
(libraries frama-c.kernel frama-c-wp.core camlp-streams zarith)
\end{lstlisting}

Its plug-in library name is \verb|frama-c-clang.core|. Its availability
must be displayed as the ``summary'' of the configuration, written as the first
line, with each dependency as a subitem:

\begin{lstlisting}
(rule
 (alias frama-c-configure)
 (deps (universe))
 (action (progn
          (echo "Clang:" %{lib-available:frama-c-clang.core} "\n")
          (echo "  - zarith:" %{lib-available:zarith} "\n")
          (echo "  - camlp5:" %{lib-available:camlp5} "\n") ; for gen_ast
          (echo "  - camlp-streams:" %{lib-available:camlp-streams} "\n")
          (echo "  - wp:" %{lib-available:frama-c-wp.core} "\n")
  )
  )
)
\end{lstlisting}

Note that \verb|camlp5| is not among the dependencies declared in
\verb|libraries|; it is used by another component, \verb|gen_ast|.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{\framac Makefiles}\label{adv:make}\codeidxdef{Makefile}

\begin{target}standard plug-in developers.\end{target}

\begin{prereq}
  Knowledge of \make.
\end{prereq}

Since the adoption of Dune, \framac's \texttt{Makefile}s were largely
simplified. They are still used for some tasks, partially due to conciseness
(\verb|make| is shorter than \verb|dune build|), partially because some tasks
are better suited for them. Some standard targets are defined in various
Makefiles that are installed in \framac's shared directory.

A minimal plugin's \verb|Makefile| can thus be the following:

\listingname{Makefile}
\makeinput{./tutorial/hello/src/Makefile}

\texttt{Makefile.testing} introduces various targets related to \framac's
testing infrastructure (see Section~\ref{adv:ptests}). This includes notably
\texttt{tests} to run all the tests of the plugin, after having taken care of
generating the corresponding \texttt{dune} files.

\texttt{Makefile.installation} provides two targets, \texttt{install} and
\texttt{uninstall}. By default, installation will occur in the current
\texttt{opam} switch, but this can be modified by using the \texttt{PREFIX}
variable (note that if you install your plugin in a non-default place, you will
have to explicitly instruct \framac to load it through option
\texttt{-load-plugin}.

Other Makefiles include \texttt{Makefile.documentation}, providing the
\texttt{doc} for generating the documentation (see Section~\ref{tut2:doc}),
and \texttt{Makefile.headers} and \texttt{Makefile.linting} which are used
by \framac itself to manage headers and perform various syntactic checks
(though, of course, you can reuse them at will).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Testing}\label{adv:ptests}\index{Test|bfit}

In this section, we present \ptests, a tool provided by \framac in order to
perform non-regression and unit tests.

\begin{important}
  Historically, \ptests has been developed before \framac switched to Dune.
  It has been ported to Dune, but some features had to be adapted and others
  became redundant; it is likely that in the future \ptests will be
  replaced with direct usage of the Dune testing framework.
\end{important}

\ptests\index{Ptests|bfit} is a test preparation tool that parses specially
crafted \C comments to create several Dune test targets, so that users can
more easily create test cases with custom \framac commands.

The generated test targets are then run via Dune.
Each result of the execution is compared with the previously saved result
(called the \emph{oracle}\index{Oracle|bfit}). A test is successful if and only
if there is no difference.  Actually, the number of results is twice the
number of tests, because standard and error outputs are compared separately.

First, Section~\ref{ptests:use} explains how to use \ptests.
Next, Section~\ref{ptests:structure} describes the test file structure for
\framac plug-ins.
Section~\ref{ptests:header} introduces the syntax of test headers, that is,
how to define test cases and their options. Section~\ref{ptests:dependencies}
explains how to declare test dependencies (files other than the test itself).
Last, Section~\ref{ptests:directives} presents the full list of \ptests
directives.

\subsection{Using \ptests}\label{ptests:use}

\ptests only {\em prepares} tests (by creating appropriate dune files), but
does not run them. Whenever a new test file is added, or test headers of
existing test files are modified, you need to run \verb|frama-c-ptests| to
regenerate them.
Note that, to run all of \framac tests (which include several directories, plus
the tests of many plug-ins), you should run \verb|make run-ptests| instead,
which will call \verb|frama-c-ptests| with the proper arguments to generate
test targets for {\em all} directories.

If new tests are created (by adding a new file, or adding an extra test case to
an existing file), you must run \verb|frama-c-ptests -create-missing-oracles|.
This will create empty test oracles for Dune.

Then, to run the tests, use \verb|dune build @ptests|.
If there are differences between the current run and oracles from previous runs,
Dune will indicate them and mark the tests as failures. If the changes are
intended, after manual inspection you can {\em promote} them as new oracles,
via \verb|dune promote|. This will simply replace the existing oracles with the
new ones. Finally, you can use \verb|frama-c-ptests -remove-empty-oracles|
to remove empty oracles (typically, messages sent to the standard error)
before committing the files to version control.

If you simply want to re-run all tests for your plug-in, run \verb|make tests|.

\subsection{Test directory structure}\label{ptests:structure}

This is the file structure of the \verb|tests| directory, where \framac
plug-ins are expected to place their tests:

\begin{lstlisting}
<plug-in directory>
+- tests
   +- ptests_config
   +- test_config
   +- suite1
      +- test1.c
      +- ...
      +- oracle
         +- test1.res.oracle
         +- test1.err.oracle
         +- ...
      +- result
         +- test1.res.log
         +- test1.err.log
         +- ...
  +- ...
\end{lstlisting}

\subsubsection{Files \texttt{test\_config} and \texttt{ptests\_config}}

Inside \verb|tests|, two files are mandatory:
\verb|ptests_config| and \verb|test_config|.

\verb|ptests_config|\codeidx{ptests\_config} usually contains a single line
with the list of {\em test suites} for that plug-in, prefixed with
\verb|DEFAULT_SUITES=|.
A test suite\index{Test!Suite|bfit} is a sub-directory of the current \texttt{tests}
directory.

\begin{lstlisting}
DEFAULT_SUITES=basic parsing misc options
\end{lstlisting}

In the example above, our plug-in has at least four sub-directories inside the
\verb|tests| directory. Each test suite can contain any number of test files.

\verb|test_config|\codeidx{test\_config} contains a list of
common {\em directives} to be applied to each test, in all test suites.
It typically contains a line \verb|PLUGIN: <module>| with the name of the
plug-in being developed (for more details about \verb|PLUGIN:|, check
Section~\ref{ptests:directives}).

Each test suite can also contain its own \verb|test_config| file. Each test
case in that suite will then inherit the directives from the parent
\verb|test_config| as well as those from the \verb|test_config| in its
directory.

Finally, different {\em test configurations} can be specified by creating
other files, e.g. the existence of a file \verb|test_config_prove| will
create a configuration named \verb|prove|. A test case can contain multiple
{\em test headers} (to be detailed in the next section), with different
directives for each configuration. Configurations are specified
when running tests, e.g. instead of running \verb|dune build @ptests|,
you can run instead \verb|dune build @ptests_config_prove| to run tests only
from the \verb|prove| configuration.

\begin{important}
  All Dune \verb|@ptests|-related targets must be run {\em after}
  \verb|frama-c-ptests| (or \verb|make run-ptests|) has been run, otherwise
  Dune may not find the generated files and report errors such as
  {\em Alias "ptests\_config" specified on the command line is empty}.
\end{important}

The catch-all command \verb|make tests| run tests for {\em all} suites, and
{\em all} configurations.

\subsubsection{Test headers}\label{ptests:header}

Inside each test suite, we find one or more test files: either \verb|.c|
or \verb|.i| files which typically start with the following
header\index{Test!Header}:

\begin{listing-nonumber}
/* run.config
  // test directives, one per line
  ...
*/
\end{listing-nonumber}

That is, a multiline C comment block (\verb|/* */|) with \verb|run.config|
and a list of lines containing test directives. This test header
tells \ptests how to generate the test commands.

Note that a configuration suffix can be added to \verb|run.config|. Also,
we can define multiple test headers, such as:

\begin{listing-nonumber}
/* run.config
  STDOPT:
*/
/* run.config_eva
  STDOPT: +"-eva"
*/
\end{listing-nonumber}

This will create a test case for the default configuration, and a different one
for the \verb|eva| configuration.

Multiple configurations may share the same set of directives:
\begin{listing-nonumber}
/* run.config, run.config_<name> [, ...]
   ... common directives ...
*/
\end{listing-nonumber}
The following wildcard is also supported, and matches any
configuration: \lstinline+/* run.config* +.
Note that it does not define a new configuration, but generates tests for
every existing configuration in the directory (as defined by the existence of
\verb|test_config_*| files).

\subsubsection{\texttt{oracle} and \texttt{result} directories}\label{ptests:oracles}

Inside each test suite, there are two directories, \verb|oracle| and
\verb|result|\footnote{If there are other configurations, there will also be
an \texttt{oracle\_<config>} and a \texttt{result\_<config>} directory per
configuration.}, each containing at least one file per test case
(remember that a single test file can contain several test cases, one per
directive).

The \verb|oracle| directory contains the test oracles, that is, the expected
results saved from previous runs.

The \verb|result| directory contains the generated Dune files produced by
\ptests.

\begin{important}
  The naming of these directories is due to historical reasons; the
  \verb|result| directory used to contain the current test outputs,
  which were then compared to the oracles, mirroring their directory
  structure. Nowadays, it could be called \verb|targets|, for instance.
\end{important}

Oracle files are named \verb|<test_name><optional_test_number>.<stream>.oracle|.
\verb|<test_name>| is simply the filename of the test file, minus its
extension\footnote{Note that this prevents having two tests in the same
suite which differ only by their extension, e.g. \texttt{test1.c} and
\texttt{test1.i}.}. \verb|<optional_test_number>| is a 0-numbered list of
test numbers for files with multiple tests: \verb|.0|, then \verb|.1|,
\verb|.2|, etc. It is omitted if the test file defines a single test case.
\verb|<stream>| is \verb|out| for \verb|stdout| (standard output) and
\verb|err| for \verb|stderr| (standard error). Therefore, there are two
oracle files for each test case. An absent oracle is equivalent to an empty one.

Files in \verb|result| are named \verb|<test_name>.<test_number>.exec.wtests|
(or, in case there are \verb|EXECNOW|\footnote{See
Section~\ref{ptests:directives} for details about this and other directives.}
directives, they end with \verb|.execnow.wtests|). They are always 0-numbered,
even when there is a single test case per file.
These are JSON files containing the data to be used (by \verb|frama-c-wrapper|
via the generated \verb|dune| file) in each test, e.g.
the command-line to be run, the output file name, and the associated oracle.
These \verb|.wtests| files are not generated when the use of \verb|frama-c-wrapper|
is not required (via \ptests' option \verb|-wrapper ""|).

\subsection{What happens when you run a test}\label{ptests:inside}

Complex tests using relative paths or extra files require understanding how
Dune runs the tests, so that they can be properly written.

By default, Dune will create a \verb|_build| directory where it stores compiled
files and other resources the user may request. When a test is run, Dune will
copy the test file and its dependencies (detailed in the next section)
to a subdirectory inside \verb|_build| (usually, mirroring the original
directory structure), \verb|cd| to the test subdirectory, and run the test
command from there. It will redirect the standard and error streams to
two files (\verb|<test>.res.log| and \verb|<test>.err.log|), and compare them
to the test oracles. If they are identical, by default Dune will not report
anything. Otherwise, it will print a message and the diff between the current
result and the previous oracle.

\subsubsection{Test dependencies}\label{ptests:dependencies}

Dune tracks dependencies between files so that it knows when objects must be
rebuilt and tests must be run again. For compiling \ocaml files, it usually
computes this information automatically. For tests, however, such information
must come from the user. \ptests will use it to generate Dune rules that
will ensure tests are re-run if their dependencies are modified.
Properly annotating test dependencies is essential to ensure reproducible,
parallelizable tests. Otherwise, non-deterministic behavior may occur.

One way to declare dependencies is to use a \verb|DEPS| directive%
\footnote{Section~\ref{ptests:directives} provides details about \ptests
directives.} with a space-separated list of files. For instance, a test
\verb|file.c| which \#includes a \verb|file.h| must declare it as a dependency:

\begin{lstlisting}[language=C]
/* run.config
   DEPS: file.h
*/
#include "file.h"
...
\end{lstlisting}

When tests mention their dependencies in the command line, a shorter syntax is
available, using the Dune special variable \verb|%{dep:<file>}|.
For instance, tests from \verb|saveload| typically consist of multiple
sub-tests, one creating a session file with \verb|-save| and another loading it
with \verb|-load|.
The second test obviously must run {\em after} the first one; adding the
dependency will ensure that Dune will sequence them correctly. In the example
below, each \verb|STDOPT| directive defines a test case.

\begin{lstlisting}[language=C]
/* run.config
   STDOPT: +"-save test1.sav"
   STDOPT: +"-load %{dep:test1.sav}"
*/
...
\end{lstlisting}

You can combine \verb|DEPS| and \verb|%{dep:}| as you wish in your tests.
Prefer \verb|%{dep:}| for local dependencies, since it does not accumulate
towards following tests, and \verb|DEPS| for dependencies which are common to
several tests.

Note that forgetting to specify dependencies can lead to test failures in
unexpected ways, such as the dependencies not being copied to Dune's test
directory, or two tests running in parallel and reading/writing concurrently
to the same file.

\subsubsection{Working directory and relative paths}

Any directive can identify a file using a relative path.
The current working directory (considered as \texttt{.}) will be a directory
inside Dune's sandbox, that is, a \verb|result| directory inside the ``mirror''
directory of the test file. This ``mirror'' directory structure is created
by Dune (by default, inside a \verb|_build| directory in the root of the Dune
project), with dependencies copied lazily for each test. Therefore, pay
attention to the fact that references to the parent directory
(\verb|..|) will likely not match what you expect.

\subsection{Detailed directives}\label{ptests:directives}\index{Test!Directive}

Directives can have various functions: some create test cases, while others
modify the environment (and therefore affect other directives).
Each directive is specified in a separate line and has the form
\begin{listing-nonumber}
DIRECTIVE: value (everything until the newline character)
\end{listing-nonumber}

\begin{example}
  Test \texttt{tests/sparecode/calls.c} declares the following directives.
  \nscodeidx{Test!Directive}{OPT}
\begin{listing-nonumber}
/* run.config
   OPT: -sparecode-analysis
   OPT: -slicing-level 2 -slice-return main -slice-print
*/
\end{listing-nonumber}
These directives state that we want to test sparecode and slicing analyses on
this file. Two test cases are defined, each with its specific set of options.
The default command (\texttt{frama-c}) will be run with these arguments, plus
the test file name, plus a few other implicit options (\verb|-check|,
\verb|-no-autoload-plugins|, \verb|-load-module|, etc).
\end{example}

Table~\ref{fig:test-directives} shows all the directives that can be used in
the configuration header of a test (or a test suite). Those whose name are
underlined are the directives that {\em actually} create test cases; the others
modify or disable test cases.
\begin{longtable}{|l|p{9cm}|p{4cm}|}
\hline
\textbf{Name} & \textbf{Specification} & \textbf{default}\\
\hline
\texttt{CMD}\nscodeidxdef{Test!Directive}{CMD}
& Program to run.
& \texttt{frama-c}
\\
\hline
\texttt{COMMENT}\nscodeidxdef{Test!Directive}{COMMENT}
& A configuration comment; this directive does nothing.
& \textit{None}
\\
\hline
\texttt{DEPS}\nscodeidxdef{Test!Directive}{DEPS}
& The list of files this test depends on.
& \textit{None}
\\
\hline
\texttt{DONTRUN}\nscodeidxdef{Test!Directive}{DONTRUN}
& Disable this test file for the current configuration.
& \textit{None}
\\
\hline
\texttt{\underline{EXECNOW}}\nscodeidxdef{Test!Directive}{EXECNOW}
& Run a custom command.
& \textit{None}
\\
\hline
\texttt{EXIT}\nscodeidxdef{Test!Directive}{EXIT}
& Indicate expected exit code, if not 0.
& \textit{None}
\\
\hline
\texttt{FILEREG}\nscodeidxdef{Test!Directive}{FILEREG}
& File name pattern of files considered as test cases.
& \texttt{.*\bss.\bss(c|i\bss)}
\\
\hline
\texttt{FILTER}\nscodeidxdef{Test!Directive}{FILTER}
& Command reading the standard input used to filter results.
In such a command, the predefined macro \texttt{@PTEST\_ORACLE@} is set to the
basename of the oracle.
& \textit{None}
\\
\hline
\texttt{LIBS}\nscodeidxdef{Test!Directive}{LIBS}
& Libraries to be loaded with each subsequent run (their compilation is not
  managed by \ptests, contrary to the modules of \texttt{MODULE} directive).
& \textit{None}
\\
\hline
\texttt{LOG}\nscodeidxdef{Test!Directive}{LOG}
& Add an additional file that the test must generate and compare against an
oracle. Note that this directive is only used by `OPT` and `STDOPT` directives.
The syntax for \texttt{EXECNOW} related to that need is different
(see the description of \texttt{EXECNOW} directive).
& \textit{None}
\\
\hline
\texttt{MACRO}\nscodeidxdef{Test!Directive}{MACRO}
& Define a new macro.
& \textit{None}
\\
\hline
\texttt{MODULE}\nscodeidxdef{Test!Directive}{MODULE}
& Register a dynamic module to be built and loaded with each subsequent test.
& \textit{None}
\\
\hline
\texttt{NOFRAMAC}\nscodeidxdef{Test!Directive}{NOFRAMAC}
& Empty the list of frama-c commands to be launched
(\texttt{EXECNOW} directives are still executed). Used when the test must not
run \texttt|frama-c|, but another command.
& \textit{None}
\\
\hline
\texttt{\underline{OPT}}\nscodeidxdef{Test!Directive}{OPT}
& Options given to the program.
& \textit{None} (but usually defined in \texttt{test\_config})
\\
\hline
\texttt{PLUGIN}\nscodeidxdef{Test!Directive}{PLUGIN}
& Plugins to be loaded with each subsequent run.
& \textit{None} (but usually defined in \texttt{test\_config})
\\
\hline
\texttt{\underline{STDOPT}}\nscodeidxdef{Test!Directive}{STDOPT}
& Add and remove options from the default set (see text for syntax details).
& \textit{None}
\\
\hline
\texttt{TIMEOUT}\nscodeidxdef{Test!Directive}{TIMEOUT}
& Kill the test after the given duration (in seconds of CPU user time)
and report a failure.
& \textit{None}
\\
\hline
\caption{Directives in configuration headers of test files.
  Underlined directives are the only ones which actually generate test cases.
}\label{fig:test-directives}
\end{longtable}

In the following, we detail some aspects of several directives.

\begin{itemize}
\item \texttt{DONTRUN} and \texttt{NOFRAMAC} directives
  do not need 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).
\item
  \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. For a given
  configuration level, the default value for directive
  \texttt{CMD}\nscodeidx{Test!Directive}{CMD} is the last
  \texttt{CMD} directive of the preceding configuration level.
\item \texttt{LOG} adds a file to be compared against an oracle in the
  next \texttt{OPT} or \texttt{STDOPT} directive. Several files can be
  monitored from a single \texttt{OPT}/\texttt{STDOPT} directive,
  through several \texttt{LOG} directives.
  These files must be generated in the result
  directory of the corresponding suite (and potentially alternative
  configuration).
  After an \texttt{OPT} or \texttt{STDOPT} directive is encountered,
  the set of additional \texttt{LOG} files is reset to its default.
  Note that \texttt{EXECNOW} directives can also be prefixed with
  \texttt{LOG}s, but they are written in the same line, without the
  separating colon (\texttt{:}).
\item By default, the test command (usually, \texttt|frama-c|) is expected
  to return successfully (i.e., with an exit status of 0).
  If a test is supposed to lead to an error, an \texttt{EXIT} directive must be
  used. It takes as argument an integer
  (typically 1 to denote a user error) representing the expected exit status
  for the subsequent tests. All tests triggered by \texttt{OPT} or
  \texttt{STDOPT} directives encountered after the \texttt{EXIT} directive
  will be expected to exit with the corresponding status, until a new
  \texttt{EXIT} directive is encountered. (\texttt{EXIT: 0} will thus
  indicate that subsequent tests are expected to exit normally).
\item If there are several \texttt{OPT} directives in the same
  configuration level, they correspond to different test cases. The
  \texttt{OPT} directives of a given configuration level replace
  the ones of the preceding level.
\item The \texttt{STDOPT}\nscodeidx{Test!Directive}{STDOPT}
  directive takes as default set of options
  the last \texttt{OPT} directive(s) of the preceding configuration
  level. If the preceding configuration level contains several
  \texttt{OPT} directives, hence several test cases, \texttt{STDOPT}
  is applied to each of them, leading to the same number of test cases.
  The syntax for this directive is the following.
  \begin{code}
    STDOPT: [[+#-]"opt" ...]
  \end{code}
  unlike in \texttt{OPT}, here \textbf{options are always given between quotes}.
  An option following a \texttt{+}
  (resp. \texttt{\#}) is added to the end (resp. start) of the current set of
  options, while an option following a \texttt{-} is removed from it.
  The directive can be empty (meaning that the corresponding test will use the
  standard set of options). As with \texttt{OPT}, each \texttt{STDOPT}
  corresponds to a different (set of) test case(s).
  \texttt{LOG} directives preceding an \texttt{STDOPT} are taken into account.
\item The syntax for \texttt{EXECNOW}\nscodeidx{Test!Directive}{EXECNOW}
  directives is the following.
  \begin{code}
    EXECNOW: [ [ LOG file | BIN file ] ... ] cmd
  \end{code}
  Files after \texttt{LOG} are log files generated by command \texttt{cmd} and
  compared from oracles, whereas files after \texttt{BIN} are binary files, also
  generated by \texttt{cmd}, but not compared to any oracles. Full access path to
  these files has to be specified only in \texttt{cmd}. Execution order between
  different \texttt{OPT}/\texttt{STDOPT}/\texttt{EXECNOW} directives is
  unspecified, unless there are dependencies between them (see \texttt{DEPS}
  directive).
  \texttt{EXECNOW} directives from a given level are added to the directives of
  the following levels.

  \textbf{Note:} An \texttt{EXECNOW} command without \verb|BIN| and without
  \verb|LOG| will not be be executed by Dune; a warning is emitted in this case.

\item The \texttt{MACRO}\nscodeidx{Test!Directive}{MACRO} directive
  has the following syntax:
  \begin{code}
    MACRO: macro-name content
  \end{code}
  where \texttt{macro-name} is any sequence of characters containing neither
  a blank nor an \texttt{@}, and \texttt{content} extends until the end of the
  line. Once such a directive has been encountered, each occurrence of
  \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
  predefined macros are listed in section~\ref{sec:ptests-macros}.
\item The \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{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
  the suite. This directive is only
  usable in a \texttt{test\_config}\codeidx{test\_config}
  configuration file.
\item The \texttt{FILTER}\nscodeidx{Test!Directive}{FILTER} directive specifies
  a transformation on the test result files before the comparison to the oracles.
  The filtering command read the result from the standard input and the oracle
  will be compared with the standard output of that command.
  In such a directive, the predefined macro \texttt{@PTEST\_ORACLE@} is set to the
  basename of the oracle.
  That allows running a \texttt{diff} command with the oracle of another
  test configuration \texttt{config}:
  \begin{code}
FILTER: diff --new-file @PTEST_DIR@/oracle_config/@PTEST_ORACLE@ -
  \end{code}
  Chaining multiple filter commands is possible by defining several \texttt{FILTER} directives (they are applied in the reverse order),
  and an empty command drops the previous \texttt{FILTER} directives.
\item The \texttt{DEPS}\nscodeidx{Test!Directive}{DEPS} directive takes a set
  of filepaths and adds them to the set of dependencies for the next
  \texttt{OPT}/\texttt{STDOPT}/\texttt{EXECNOW} directives.
  Whenever these dependencies change, the test
  cases depending on them must be re-run. Otherwise, Dune does not re-run
  successful tests. Dependencies also ensure that tests which require output
  from others are run serially and not in parallel.
  Note that Dune also has a special variable notation which can be used to
  specify dependencies: \verb|%{dep:<file>}|. For instance, the following
    block:
    \begin{code}
      DEPS: file1.h file2.c
      OPT: -cpp-extra-args="-Ifile1.h" file2.c
    \end{code}
    Is equivalent to:
    \begin{code}
      OPT: -cpp-extra-args="-I%\{dep:file1.h\}" %\{dep:file2.c\}
    \end{code}
    The special variable notation is interpreted by Dune before executing the
    command. All dependencies (either via \texttt{DEPS} or \verb|%{dep:}|) are
    collected and added to the set of dependencies for the test case.
\item
  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.
\end{itemize}

\begin{important}
\paragraph{\texttt{@} in the text of a directive}
As mentioned above, \texttt{@} is recognized by \ptests as the beginning of
a macro. If you need to have a literal \texttt{@} in the text of the directive
itself, it needs to be doubled, {\it i.e.} \texttt{@@} will be translated as
\texttt{@}.
\end{important}

\begin{important}
  \textbf{Summary: ordering of test executions}

  There is no total ordering between the tests in a test file header.
  The only ordering is dictated by the dependencies declared in the test cases.
  Dune will by default run tests in parallel.

  A consequence of this ordering is that, if you need a test to produce output
  that will be consumed by another test, the consumer \emph{must} declare the
  produced file as a dependency.
\end{important}

\subsection{Pre-defined macros for tests commands}\label{sec:ptests-macros}
Table~\ref{tab:ptests-macros} gives the definition of the predefined macros that
can be used in \ptests' directives.
\begin{longtable}{|p{4.5cm}|p{10cm}|}
\hline
Name & Expansion \\
\hline
\verb|frama-c| & path to \framac executable \\
\hline
\verb|PTEST_CONFIG| & either the empty string or \verb|_| followed by the
name of the current alternative configuration 
(see section~\ref{ptests:structure}). \\
\hline
\verb|PTEST_DIR| & current test suite directory \\
\hline
\verb|PTEST_RESULT| & current result directory \\
\hline
\verb|PTEST_FILE| & path to the current test file \\
\hline
\verb|PTEST_NAME| & basename of the current test file (without suffix) \\
\hline
\verb|PTEST_NUMBER| & rank of current test in the test file. There are in
fact two independent numbering schemes: one for \verb|EXECNOW| commands and
one for regular tests (if more than one \verb|OPT|).\\
\hline
\verb|PTEST_RESULT| & shorthand alias to \verb|@PTEST_DIR@/result@PTEST_CONFIG@|
(the result directory dedicated to the tested configuration)\\
\hline
\verb|PTEST_ORACLE| & basename of the current oracle file (macro only usable in FILTER directives)\\
\hline
\verb|PTEST_MODULE| & current list of modules defined by the \verb|MODULE| directive\\
\hline
\verb|PTEST_LIBS| & current list of modules defined by the \verb|LIBS| directive\\
\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|-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_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
\verb|frama-c| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@|\\
\hline
\verb|frama-c-cmd| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@|\\
\hline
\verb|frama-c-exe| & set to the value of the \verb|TOPLEVEL_PATH| variable from \verb|./tests/ptests_config| file\\
\hline
\caption{Predefined macros for ptests}\label{tab:ptests-macros}
\end{longtable}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Plug-in Migration from Makefile to Dune}\label{adv:dune-migration}

\begin{target}developers who have an existing plug-in for Frama-C 25 or less and
  want to migrate this plug-in to Frama-C 26 or more.\end{target}

\begin{prereq}
  Being familiar with the plug-in to migrate. Depending on how complex the
  plug-in is, it may require an advanced knowledge of the Dune build system.
\end{prereq}

Please note that this section is a best effort procedure for making the
migration as smooth as possible. If the plug-in is particularly complex,
please contact us if you need some help for migrating it.

\subsection{Files organization changes}

\begin{important}
Due to the way \texttt{dune} operates, it is preferable to work on the migration
starting from a ``clean'' directory, without compilation and tests
(in \texttt{result} directory of the test suites) artifacts. Otherwise,
\texttt{dune} will complain about conflicts between files being both present
in the original source directory and the target of a compilation rule.
\end{important}

Previously for a plug-in named \texttt{Plugin}, only the file
\texttt{Plugin.mli} was necessary to expose the signature of the plug-in. Now,
one has to also provide an implementation file \texttt{Plugin.ml}.
On the other hand, it is not necessary that it begins with a capital letter
anymore: you can have \texttt{plugin.ml} and \texttt{plugin.mli}. If these files
are not present, all functions included in the modules constituting the
plug-in will be exported.

For most plug-ins, the \texttt{autoconf} and \texttt{configure} will be useless.
In particular, \framac does not provide any \texttt{autoconf} and
\texttt{configure} features anymore. So for most plug-ins these files will be
entirely removed (see~\ref{adv:dune-migration:conf}). Thus, the
\texttt{Makefile.in} does not exist anymore. A \texttt{Makefile} may be useful
to provide some shortcuts.

If a plugin has a graphical user-interface, it is recommended to put the related
files into a separate directory in the directory of the plug-in
(see~\ref{adv:dune-migration:gui}).

It was previously possible to indicate \texttt{.} as a test suite for \ptests.
In such a case, tests source files were directly in the \texttt{tests} directory.
This is not possible anymore. If the plug-in tests follow this architecture,
these tests should be moved in a subdirectory of \texttt{tests} and the oracles
updated before starting the migration.

\subsection{Template \texttt{dune} file}

This basic template should be enough for most plug-ins. The next sections
explain how to add more information to this file to handle some common cases.

\begin{lstlisting}[language=Dune]
( rule
  (alias frama-c-configure)
  (deps (universe))
  (action ( progn
            (echo "MyPlugin:" %{lib-available:frama-c-myplugin.core} "\n")
            (echo " - Frama-C:" %{lib-available:frama-c.kernel} "\n")
          )
  )
)

( library
  (optional)
  (name myplugin)
  (public_name frama-c-myplugin.core)
  (flags -open Frama_c_kernel :standard)
  (libraries frama-c.kernel)
)

( plugin
  (optional)
  (name myplugin) (libraries frama-c-myplugin.core) (site (frama-c plugins))
)
\end{lstlisting}

For the creation of the \texttt{dune-project} file, please refer to
Section~\ref{tut2:hello}.

\subsection{\texttt{autoconf} and \texttt{configure}}\label{adv:dune-migration:conf}

Indicating whether a plug-in is available and why (availability of the
dependencies) is now handled via the \texttt{frama-c-configure} rule.

When working in the Frama-C \texttt{src/plugins} directory, enabling or
disabling the plug-in at build time is done thanks to the script
\texttt{dev/disable-plugins.sh}.

Plug-ins dependencies are now declared in the \texttt{dune} file. In the
\texttt{libraries} field. For instance, if in the \texttt{autoconf} of the
plug-in, the following lines are present:

\begin{lstlisting}
plugin_require_external(myplugin,zmq)
plugin_use_external(myplugin,zarith)
plugin_require(myplugin,wp)
plugin_use(myplugin,eva)
\end{lstlisting}

The \texttt{libraries} should be now:
\begin{lstlisting}[language=Dune]
  (libraries
     frama-c.kernel
     zmq
     (select zarith_dependent.ml from
       (%{lib-available:zarith} -> zarith_dependent.ok.ml)
       ( -> zarith_dependent.ko.ml)
     )
     frama-c-wp.core
     (select eva_dependent.ml from
       (%{lib-available:frama-c-eva.core} -> eva_dependent.ok.ml)
       ( -> eva_dependent.ko.ml)
     )
  )
\end{lstlisting}
For external binaries, the keywod is \texttt{bin-available}.

In the case some file must be generated at build time, it is recommended to use