diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 06ce6817dd38bcb5fd4dd82734776275bc1d86a0..6647eca22ae390d903e3ed76bb1019beb8aa6ac2 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -71,7 +71,7 @@ want full details about specific parts.
In this Section, we detail how to modify the file \texttt{configure.in} in
order to configure plug-ins (\framac configuration has been introduced in
-Section~\ref{tut2:configure} and~\ref{tut2:makefile}).
+%Section~\ref{tut2:configure} and~\ref{tut2:makefile}).
First Section~\ref{conf:principle} introduces the general principle and
organisation of \texttt{configure.in}. Then Section~\ref{conf:add} explains how
@@ -487,24 +487,25 @@ have to:
\item include \texttt{Makefile.dynamic}.
\end{enumerate}
-\begin{example}
-A minimal \texttt{Makefile} is shown below. That is the Makefile of the plug-in
-\texttt{Hello World} presented in the tutorial (see
-Section~\ref{tut2:hello}). Each variable set in this example has to be set
-by any plug-in.
-\codeidx{Makefile.dynamic}
-\codeidx{FRAMAC\_SHARE}
-\codeidx{PLUGIN\_CMO}
-\codeidx{PLUGIN\_NAME}
-\makefileinput{./tutorial/hello/generated/makefile_multiple/Makefile}
-\texttt{FRAMAC\_SHARE} must be set to the \framac share directory.
-\texttt{PLUGIN\_NAME} is the capitalized name of your plug-in while
-\texttt{PLUGIN\_CMO} is the list of the files $.cmo$ generated from your \caml
-sources.
-Note that, by default, during compilation of your plug-in all warnings are
-disabled; it is recommended to define environment variable
-\texttt{DEVELOPMENT=yes} to enable the standard set of compilation warnings.
-\end{example}
+TODO : replace example
+%% \begin{example}
+%% A minimal \texttt{Makefile} is shown below. That is the Makefile of the plug-in
+%% \texttt{Hello World} presented in the tutorial (see
+%% Section~\ref{tut2:hello}). Each variable set in this example has to be set
+%% by any plug-in.
+%% \codeidx{Makefile.dynamic}
+%% \codeidx{FRAMAC\_SHARE}
+%% \codeidx{PLUGIN\_CMO}
+%% \codeidx{PLUGIN\_NAME}
+%% \makefileinput{./tutorial/hello/generated/makefile_multiple/Makefile}
+%% \texttt{FRAMAC\_SHARE} must be set to the \framac share directory.
+%% \texttt{PLUGIN\_NAME} is the capitalized name of your plug-in while
+%% \texttt{PLUGIN\_CMO} is the list of the files $.cmo$ generated from your \caml
+%% sources.
+%% Note that, by default, during compilation of your plug-in all warnings are
+%% disabled; it is recommended to define environment variable
+%% \texttt{DEVELOPMENT=yes} to enable the standard set of compilation warnings.
+%% \end{example}
\begin{important}
To run your specific Makefile, you must have properly installed \framac
diff --git a/doc/developer/macros.sty b/doc/developer/macros.sty
index 86469e96b81d7243fb571078f0fb284983601754..4cba3d771a41dc20a45abb9d1a40bd0e15fb2f10 100644
--- a/doc/developer/macros.sty
+++ b/doc/developer/macros.sty
@@ -48,6 +48,7 @@
\newcommand{\lablgtksourceview}{\langage{Lablgtksourceview2}}
\newcommand{\dottool}{\langage{DOT}}
\newcommand{\ocamldoc}{\langage{ocamldoc}}
+\newcommand{\odoc}{\langage{odoc}}
\newcommand{\make}{\langage{make}}
\newcommand{\jessie}{\langage{Jessie}}
\newcommand{\why}{\langage{Why}}
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 03ff6f1008dca324f795738aeab8612decd61e72..9a6ca0453450397f9608c1c944e1bcdca5f4aaa9 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -4,94 +4,40 @@
\begin{target}beginners.\end{target}
-This chapter aims at helping a developer to write his first \framac plug-in. At
-the end of the tutorial, any developer should be able to extend \framac with a
-simple analysis available as a \framac plug-in. This chapter was written as a
+This chapter aims at helping a developer to write their first \framac plug-in.
+At the end of the tutorial, any developer should be able to extend \framac with
+a simple analysis available as a \framac plug-in. This chapter was written as a
step-by-step explanation on how to proceed towards this goal. It will get you
started, but it does not tell the whole story. You will get it with your own
experiments, and by reading the other chapters of this guide as needed.
-First, Section~\ref{tut2:environment} describes how to quickly setup a
+Section~\ref{tut2:environment} provides some tips for setting up a
development environment for \framac.
Section~\ref{tut2:architecture} shows what a plug-in looks like. Then
Section~\ref{tut2:hello} explains the basis for writing a standard \framac
plug-in\index{Plug-in}, while Section \ref{tut2:cfg} details how to interact
with \framac and other plug-ins to implement analyzers of \C programs.
-\section{Quick Setup of a Development Environment}\label{tut2:environment}
+\section{Development Environment}\label{tut2:environment}
-This setup is based on Emacs as the IDE, with OPAM for OCaml package
-installation and Merlin for OCaml source code navigation.
-Similar environments can be setup using other editors, such as Vim and
-Sublime Text, but they are not detailed here; please refer to the Merlin
-documentation for further details on how to setup other editors for OCaml
-development.
+The \framac team currently recommends using
+VS~Code\footnote{\url{https://code.visualstudio.com}} as IDE.
+It offers extensions (automatically suggested when you open an OCaml source
+file) which provide type checking, syntax highlighting, and code navigation
+features.
+The \framac team currently uses the \texttt{ocp-indent} opam package
+for code indentation. Consider installing it if you want to ensure your
+code follows the same conventions.
-\subsection{Emacs Configuration Files}
+Other IDEs often used for OCaml development include Vim and Emacs. For them,
+Merlin\footnote{\url{https://ocaml.github.io/merlin}} (code navigation, typing
+and auto-completion tool) is currently the main editor service.
+It is used by OCaml-LSP\footnote{\url{https://github.com/ocaml/ocaml-lsp}},
+which is an implementation of LSP ({\em Language Server Protocol} for OCaml.
-The \framac source distribution includes, in its \texttt{share} directory,
-some \texttt{frama-c-*.el} files ({\em Emacs-lisp} scripts)
-with default settings for an OCaml development environment based on
-Emacs + OPAM + Merlin. To set it up, do the following:
-
-\begin{enumerate}
-\item Install Emacs, OPAM, and OPAM packages \textsf{merlin}, \textsf{tuareg}
- and \textsf{ocp-indent};
-\item Copy \texttt{share/emacs/frama-c-*.el} to a directory in your Emacs load-path;
-\item Add \texttt{(load-library "frama-c-recommended")} to your \texttt{.emacs}
- init file.
-\end{enumerate}
-
-For instance, run these commands (after having installed OPAM):
-
-\begin{verbatim}
-opam install merlin tuareg ocp-indent
-mkdir ~/.emacs.d/frama-c
-cp <path to frama-c sources>/share/emacs/frama-c-*.el ~/.emacs.d/frama-c/
-\end{verbatim}
-
-And then add this in the beginning of your \texttt{\textasciitilde/.emacs}:
-
-\begin{verbatim}
-(add-to-list 'load-path "~/.emacs.d/frama-c")
-(load-library "frama-c-recommended")
-\end{verbatim}
-
-You can replace \texttt{frama-c-recommended} with \texttt{frama-c-dev} in the
-above line. The former contains some extra, optional settings, while the latter
-contains only the most important settings for OCaml development. We recommend
-you review the definitions in \texttt{frama-c-recommended} and remove those you
-find unnecessary.
-
-\subsection{Quick Merlin guide}
-
-Merlin\footnote{Merlin is available on Github
- (\url{https://github.com/the-lambda-church/merlin}) and as an OPAM package.}
-is a tool for OCaml type information, source code navigation and
-auto-completion.
-
-Detailed instructions for using Merlin with Emacs are available at
-\url{https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch}.
-
-The \framac Makefile contains a target \textsf{merlin} that generates an
-appropriate \texttt{.merlin} file to be used when editing \framac
-\texttt{.ml/.mli} files. Run \texttt{make merlin} after compiling \framac,
-and the generated \texttt{.merlin} file will be automatically used when opening
-\framac OCaml sources.
-
-Here is a quick summary of the most useful commands when editing
-\texttt{.ml/.mli} files:
-
-\begin{itemize}
-\item \texttt{Ctrl+c Ctrl+t}: display type information
- (repeat it to further expand types)
-\item \texttt{Ctrl+c Ctrl+l}: jump to definition
- (for variables, types, modules, etc.)
-\item \texttt{Ctrl+c Ctrl+x}: jump to next error in current buffer
-\end{itemize}
-
-Merlin also includes an auto-complete feature. Check its website for
-further documentation.
+Overall, it is \textbf{strongly} suggested to use an OCaml-aware IDE and take
+the time to set it up. Plug-ins use several different parts of the \framac API,
+and a properly setup IDE greatly improves productivity.
\section{What Does a Plug-in Look Like?}\label{tut2:architecture}
\index{Plug-in!Architecture}\index{Architecture!Plug-in}
@@ -138,21 +84,21 @@ platform. This tutorial focuses on specific parts of this figure.
}
};
- \coordinate[yshift=\padding] (makefile-se) at (gui.north east);
- \coordinate (makefile-nw) at (gui.west |- implem.north);
+ \coordinate[yshift=\padding] (dune-se) at (gui.north east);
+ \coordinate (dune-nw) at (gui.west |- implem.north);
\node[fill=palered, rounded corners=5pt,node font=\large,
- fit=(makefile-nw) (makefile-se),
+ fit=(dune-nw) (dune-se),
inner sep=0pt,draw]
- (makefile)
- {Makefile};
+ (dune)
+ {dune\\dune-project\\frama-c-plug-in.opam};
\node[node font={\Large\bfseries},yshift=\padding,anchor=south]
- at ($(implem.north west)!0.5!(makefile.north east)$)
+ at ($(implem.north west)!0.5!(dune.north east)$)
(plugin-title)
{Plug-in directory};
\begin{scope}[on background layer]
\node[fill=LightCyan, rounded corners=7pt,draw,
- fit=(implem) (gui) (makefile) (plugin-title), inner sep=\padding]
+ fit=(implem) (gui) (dune) (plugin-title), inner sep=\padding]
(plugin-dir)
{};
\end{scope}
@@ -168,10 +114,6 @@ platform. This tutorial focuses on specific parts of this figure.
\node[anchor=south east,xshift=-\padding] at (registration.north west)
{\usebox{\captionbox}};
- \node[anchor=south,yshift=\bigpadding,fill=palered,draw,
- minimum height=1.5\designheight]
- at (plugin-dir.north -| gui.north) (makefile-dynamic) {Makefile.dynamic};
-
\newlength{\kernelwidth}
\setlength{\kernelwidth}{\widthof{Dynamic}}%TODO:compute dynamically
\node[xshift=-\bigpadding,anchor=east] at (plugin-dir.west) {
@@ -187,7 +129,6 @@ platform. This tutorial focuses on specific parts of this figure.
\end{tikz-vbox}
};
- \draw[-Latex] (makefile.north) -- (makefile-dynamic.south);
\draw[-Latex] (gui.south) -- (design.north);
\coordinate (main-pt) at ($(db-main.east)+(0.9\bigpadding,0)$);
\draw (register.west) -| (main-pt);
@@ -229,66 +170,133 @@ the next section shows how to:
\section{The Hello plug-in}\label{tut2:hello}
-This simple plug-in explain how to make your plug-in interact basically
-with several aspects of the \framac framework: registration, getting
-command-line options, compilation and installation, console output,
-testing, and documentation. (In case of difficulty, it is explained at
-the end of this section how to generate the whole plug-in.)
+This simple plug-in illustrates how to create your own plug-in basically with
+several aspects of the \framac framework: building the plugin and installing the
+plug-in, registration, getting command-line options, console output, testing and
+documentation. (In case of difficulty, it is explained at the end of this
+section how to generate the whole plug-in.)
-\subsection{A Simple Script}\label{tut2:script}
-\index{Plug-in!Script}
+\subsection{Creating a new plug-in}\label{tut2:basic}
+\index{Plug-in!Basic}
-The easiest way to extend \framac is to write a simple script. A
-simple 'Hello World' script consists of a single \ocaml file:
+A plug-in is built using Dune\footnote{\url{https://dune.build}}. It is composed
+minimally of the following files:
+
+\begin{itemize}
+ \item a \texttt{dune-project} file that describes the project;
+ \item a \texttt{dune} file that describes the build of the project;
+ \item a \texttt{<My\_plugin>.ml} file that defines the API of the plugin
+ (which can be empty).
+\end{itemize}
+
+For example, for the Hello plugin:
+
+\listingname{./dune-project}
+\duneinput{./tutorial/hello/v1-simple/dune-project}
+
+\listingname{./dune}
+\duneinput{./tutorial/hello/v1-simple/dune}
+
+\texttt{Hello.ml} is just an empty file.
+
+Then the plugin can be built using the following command:
+
+\lstinline{dune build}
+
+If Dune is installed, this should compile the project successfully.
+Note that Dune emits messages {\em during} compilation, but erases them
+afterwards. In case of success, there will be no visible output at the end.
+
+\begin{important}
+ Dune always looks for \texttt{dune-project} files in the parent directories,
+ so make sure that your Hello directory is not inside another one containing
+ a Dune project (\eg if you are running this directly from the \framac source
+ archive), otherwise \verb|dune build| may fail. You can always add option
+ ``\verb|--root .|'' to force Dune to ignore parent directories.
+\end{important}
+
+Note a few details about the naming conventions:
+
+\begin{itemize}
+ \item in the \texttt{dune-project} file, the name of the plugin is
+ \texttt{frama-c-<my-plugin>}
+ \item in the \texttt{dune} file, the name of:
+ \begin{itemize}
+ \item the library is \texttt{My\_plugin} (it is a module name);
+ \item the public name of the library is \texttt{frama-c-<my-plugin>.core}
+ (dune project name core);
+ \item the name of the plugin is \texttt{my-plugin};
+ \item the plugin must at least include the library
+ \texttt{frama-c-<my-plugin>.core}.
+ \end{itemize}
+\end{itemize}
-\listingname{./hello\_world.ml\footnotemark}
-\ocamlinput{./tutorial/hello/generated/script/hello_world.ml}
-\sscodeidx{Db}{Main}{extend}
+Of course, for now, our plug-in does nothing, so let us change that.
-This script defines a simple function that writes a message to an
-output file, then registers the function \texttt{run} as an entry point for the
-script. \framac will call it among the other plug-in entry points if the script
-is loaded.
+\subsection{A Very Simple Plug-in}\label{tut2:simple}
+\index{Plug-in!Simple}
-The script is compiled, loaded and run with the command
-\texttt{frama-c -load-script hello\_world.ml}. Executing this command
-creates a \texttt{hello.out} file in the current directory.
+Let us add a simple file to our plug-in:
-\subsection{Registering a Script as a Plug-in}\label{tut2:plugin}
+\listingname{./hello\_world.ml}
+\ocamlinput{./tutorial/hello/v1-simple/hello_world.ml}
+\sscodeidx{Db}{Main}{extend}
+
+This file defines a simple function that writes a message to an output file,
+then registers the function \texttt{run} as an entry point. \framac will call
+it among the other plug-in entry points if the plug-in is loaded.
+
+The plug-in is compiled the same way as previously explained in~\ref{tut2:basic}.
+Then, one can execute the script using the command:
+
+\lstinline{dune exec -- frama-c}
+
+Executing this command creates a \texttt{hello.out} file in the current
+directory.
+
+\begin{important}
+ You can think of \verb+dune exec --+ as a wrapper for \texttt{frama-c}
+ which adds your plug-in to those already present in \framac.
+ It operates on a local Dune sandbox, allowing you to test it without
+ risking ``polluting'' your installed \framac.
+\end{important}
+
+\subsection{Registering a Plug-in in Frama-C}\label{tut2:plugin}
\index{Plug-in!Registration}
To make this script better integrated into \framac, its code must register
-itself as a plug-in. Such a registration provides general services, such as
-outputting on the \framac console, or extending \framac with new command-line
+itself as a plug-in. Registration provides general services, such as
+outputting to the \framac console and extending \framac with new command-line
options.
Registering a plug-in is achieved through the use of the
\texttt{Plugin.Register} functor:
\listingname{./hello\_world.ml}
-\ocamlinput{./tutorial/hello/generated/with_registration/hello_world.ml}
+\ocamlinput{./tutorial/hello/v2-register/hello_world.ml}
\sscodeidx{Db}{Main}{extend}
\scodeidx{Plugin}{Register}
-The argument for this functor is a module with three values:
+The argument to the \texttt{Plugin.Register} functor is a module with three
+values:
\begin{itemize}
\item \texttt{name} is an arbitrary, non-empty string containing the full name
of the module.
-\item \texttt{shortname} is a small string containing the short name of the
- module, usually used as a prefix for plug-in options. No space is allowed in
- that string.
-\item \texttt{help} is a string containing free-form text, containing a
+\item \texttt{shortname} is a small string containing the {\em short name} of
+ the module, to be used as a prefix for all plug-in options\footnote{\framac
+ does not enforce that all plug-in options are prefixed with its shortname,
+ but it is customary to do so.}. It cannot contain spaces.
+\item \texttt{help} is a string containing free-form text, with a
description of the module.
\end{itemize}
Visible results of the registration include:
\begin{itemize}
-\item ``hello world'' appears in the list of available plug-ins
- (consultable with \texttt{frama-c -load-script
- hello\_world.ml -plugins});
+\item ``hello world'' appears in the list of available plug-ins;
+ you can check it by running
+ \verb|dune exec -- frama-c -plugins|;
\item default options for the plug-in work, including the inline help
- (available with \texttt{frama-c -load-script
- hello\_world.ml -hello-help}).
+ (available with \verb|dune exec -- frama-c -hello-help|).
\end{itemize}
\subsection{Displaying Messages}\label{tut2:messages}
@@ -298,81 +306,86 @@ The signature of the module \texttt{Self} obtained by applying
\texttt{Plugin.Register} is \texttt{General\_services}. One of these general
services is logging, \ie message display. In \framac, one should never attempt
to write messages directly to \texttt{stderr} or \texttt{stdout}: use the
-general services instead\footnote{However writing to a new file using standard
+general services instead\footnote{However, writing to a new file using standard
\ocaml primitives is OK.}.
\listingname{./hello\_world.ml}
-\ocamlinput{./tutorial/hello/generated/with_log/hello_world.ml}
+\ocamlinput{./tutorial/hello/v3-log/hello_world.ml}
\sscodeidx{Db}{Main}{extend}
\scodeidx{Plugin}{Register}
Running this script yields the following output:
\begin{shell}
-\$ frama-c -load-script hello_world.ml
+\$ dune exec -- frama-c
[hello] Hello, world!
[hello] 11 * 5 = 55
\end{shell}
The \texttt{result} routine is the function to use to output results of your
-plug-in. The \framac output routines takes the same arguments than the \caml
-function \texttt{Format.printf}.
-
-The function \texttt{feedback} outputs messages that show progress to the
-user. In this example, we gave to feedback a log level of 2, because
-we estimated that in most case the user is not interested in seeing
-the progress of a fast operation (simple multiplication). The default
+plug-in. The \framac output routines take the same arguments as the \caml
+function \texttt{Format.printf}\footnote{The
+\href{https://v2.ocaml.org/api/Format.html}{Format} module is part of the
+OCaml standard library and provides advanced pretty-printing features.
+If you are not familiar with it, consider grepping some \framac messages
+to get a feel for how to use it.}.
+
+Function \texttt{feedback} outputs messages that show progress to the
+user. In this example, we decided to emit a feedback message with a log level
+of 2, because we estimated that in most cases the user is not interested in
+seeing the progress of a fast operation (simple multiplication). The default
log level is 1, so by default this message is not displayed. To see
it, the verbosity of the \texttt{hello} plug-in must be increased:
\begin{shell}
-\$ frama-c -load-script hello_world.ml -hello-verbose 2
+\$ dune exec -- frama-c -hello-verbose 2
[hello] Hello, world!
[hello] Computing the product of 11 and 5...
[hello] 11 * 5 = 55
\end{shell}
-For a comprehensive list of the logging routines and options, see
+For a comprehensive list of logging routines and options, see
Section~\ref{adv:log}.
-\subsection{Adding Command Line Options}\label{tut2:basic-options}
-\index{Plug-in!Command Line Options}\index{Command Line}
+\subsection{Adding Command-Line Options}\label{tut2:basic-options}
+\index{Plug-in!Command-Line Options}\index{Command Line}
We now extend the \texttt{hello world} plug-in with new options.
-If the plug-in is installed (with \texttt{make install}), it will be loaded and
-executed on every invocation of \texttt{frama-c}, which is surely not what you
-want. To avoid this behavior, we add a boolean option, set by default to false,
-that conditionally enables the execution of the main function of the plug-in
-(the usual convention for the name of the option is to take the short name of
-the module with no suffix, \ie \texttt{-hello} in our case).
+If the plug-in is installed (globally, with \verb|make install|, or locally,
+with \verb|dune exec|), it will be loaded and
+executed on {\em every} invocation of \texttt{frama-c}, which is not how most
+plug-ins work. To change this behavior, we add a boolean option, set by default
+to false, that conditionally enables the execution of the main function of the
+plug-in. The usual convention for the name of this option is the short
+name of the module, without suffix, \ie \texttt{-hello} in our case.
We also add another option, \texttt{-hello-output}, that takes a string
argument. When set, the hello message is displayed in the file given as
argument.
\listingname{./hello\_world.ml}
-\ocamlinput{./tutorial/hello/generated/with_options/hello_world.ml}
+\ocamlinput{./tutorial/hello/v4-options/hello_world.ml}
Registering these new options is done by calling the \texttt{Self.False} and
-\texttt{Self.String} functors, which respectively creates a new boolean option
-whose default value is false and a new string option with a user-defined default
-value (here \texttt{"-"}). The values of these options are obtained \via
-\texttt{Enabled.get ()} and \texttt{Output\_file.get ()}.
+\texttt{Self.String} functors, which respectively create a new boolean option
+whose default value is false and a new string option with a user-defined
+default value (here, \texttt{"-"}). The values of these options are obtained
+\via \texttt{Enabled.get ()} and \texttt{Output\_file.get ()}.
With this change, the hello message is displayed only if \framac is
executed with the \texttt{-hello} option.
\begin{shell}
-\$ frama-c
-\$ frama-c -load-script hello_world.ml -hello
+\$ dune exec -- frama-c
+\$ dune exec -- frama-c -hello
[hello] Hello, world!
-\$ frama-c -load-script hello_world.ml -hello -hello-output hello.out
+\$ dune exec -- frama-c -hello -hello-output hello.out
\$ ls hello.out
hello.out
\end{shell}
These new options also appear in the inline help for the hello plug-in:
\begin{shell}
-\$ frama-c -load-script hello_world.ml -hello-help
+\$ dune exec -- frama-c -hello-help
...
***** LIST OF AVAILABLE OPTIONS:
@@ -383,111 +396,70 @@ These new options also appear in the inline help for the hello plug-in:
...
\end{shell}
+\subsection{About the plug-in build process}
-\subsection{Writing a Makefile}\label{tut2:basic-makefile}
-\index{Plug-in!Makefile}
-
-The use of \texttt{load-script} is ideal for small experimentations,
-or when writing very specific extensions. When a plug-in becomes larger,
-or more general-purpose, and must be split into several files, it is a
-good idea to build and install it properly. \framac provides means to
-simplify this through the use of \texttt{Makefile}s.
-
-First, lets us create a \texttt{hello} directory that will contain all
-of our plug-in files. We put \verb+hello_world.ml+ inside it, and then
-create our \texttt{Makefile} there.
-
-\subsubsection*{A simple Makefile}
-
-% TODO: Recuperer toutes les informations du tutoriel 1
+As mentioned before, each plug-in needs a module declaring its public API.
+In our examples, this was file \verb|Hello.ml|, which was left empty.
+To make it more explicit to future users of our plug-in, it is customary to
+add a comment such as the following:
-We write a simple \texttt{./Makefile} for our
-\texttt{./hello\_world.ml} plug-in:
-
-\listingname{./Makefile}
-\codeidx{Makefile.dynamic}
-\codeidx{FRAMAC\_SHARE}
-\codeidx{PLUGIN\_CMO}
-\codeidx{PLUGIN\_NAME}
-\makefileinput{./tutorial/hello/generated/makefile_single/Makefile}
-
-This \texttt{Makefile} sets some variables before including the generic
-\texttt{Makefile.dynamic} which is installed within \framac. It may be
-customized in several ways to help building a plug-in (see
-Section~\ref{adv:dynamic-make} for details).
+\listingname{./Hello.ml}
+\ocamlinput{./tutorial/hello/v5-multiple/Hello.ml}
\begin{important}
- The name of each compilation unit (here \texttt{hello\_world}) must be
- different from the plug-in name set by the \texttt{Makefile} (here
- \texttt{Hello}), from any other plug-in names (\eg \texttt{value}\footnote{
- \texttt{value} is the technical plug-in name of the \texttt{Eva} plug-in})
- and from any other \framac kernel \caml files (\eg \texttt{plug-in}).
+ Note the unusual capitalization of the filename \texttt{Hello.ml}, which
+ must correspond to the name of the plug-in specified in the Dune file
+ (the \texttt{name} part inside \texttt{library}).
\end{important}
-The plug-in also needs an interface file. Indeed, thanks to
-\texttt{Makefile.dynamic}, each plug-in is packed into a single module
-\texttt{\$(PLUGIN\_NAME)}\codeidx{PLUGIN\_NAME} (here \texttt{Hello}) which
-needs an interface. Here we simply export an empty interface in order to hide
-the whole implementation to other developers.
+Note that, to avoid issues, the name of each compilation unit
+(here \texttt{hello\_world}) must be different from the plug-in name set in
+the \texttt{dune} file (here \texttt{Hello}), from any other plug-in names
+(\eg \texttt{eva}, \texttt{wp}, etc.) and from any other \framac kernel
+\caml files (\eg \texttt{plugin}).
-\listingname{./Hello.mli}
-\ocamlinput{./tutorial/hello/src/Hello.mli}
-\begin{important}
- Note the unusual capitalization of the filename \texttt{Hello.mli} which is
- required for compilation purposes.
-\end{important}
+The module name chosen by a plug-in (here \texttt{Hello}) is used by Dune to
+{\em pack} that plug-in; any functions declared in it become part of the
+plug-in's public API. They become accessible to other plug-ins and need to be
+maintained by the plug-in developer. Leaving it empty avoids exposing
+unnecessary implementation details.
-Inside the plug-in's directory, run \texttt{make} to compile it. Note that the
-compiled files are copied into a \texttt{top} (for {\em top-level}) subdirectory
-(if our plug-in had GUI-dependent modules, they would be placed in a
-\texttt{gui} subdirectory).
-The module can then be loaded and executed by using
-\texttt{frama-c -load-module top/Hello}.
+Inside the plug-in's directory, \texttt{dune build} compiles it and creates the
+packed module. It can be installed along with the other \framac plug-ins using
+\verb|dune install|.
-Then run \texttt{make install} to install the plug-in (you need to have write
-access to the \texttt{plugins} directory, located at the path given by the
-command \texttt{frama-c-config -print-libpath}).
+You can then just launch \texttt{frama-c} (without any options), and the
+\texttt{Hello} plug-in will be automatically loaded. Check it with the command
+\verb|frama-c -hello-help|.
-Just launch \texttt{frama-c} (without any option): the \texttt{Hello}
-plug-in is now always loaded, without the need to pass other options to
-the command line. Check it with the command \texttt{frama-c -hello-help}.
+You can uninstall it by running \verb|dune uninstall|.
\subsubsection*{Splitting your source files}
Here is a slightly more complex example where the plug-in has been split into
-several files. Usually plug-in registration through \texttt{Plugin.Register}
+several files. Usually, plug-in registration through \texttt{Plugin.Register}
should be done at the bottom of the module hierarchy, while registration of the
-run function through \texttt{Db.Main.extend} should be at the top, as in the
-following example. The \texttt{PLUGIN\_CMO} variable must contain the list of
-file names, in the correct \ocaml build order.
-
-\listingname{./Makefile}
-\codeidx{Makefile.dynamic}
-\codeidx{FRAMAC\_SHARE}
-\codeidx{PLUGIN\_CMO}
-\codeidx{PLUGIN\_NAME}
-\makefileinput{./tutorial/hello/generated/makefile_multiple/Makefile}
-
+\texttt{run} function through \texttt{Db.Main.extend} should be at the top.
The three following files completely replace the \texttt{./hello\_world.ml}
from the previous section. Modules are directly called by their name in the
classical \ocaml way.
\listingname{./hello\_options.ml}
-\ocamlinput{./tutorial/hello/generated/makefile_multiple/hello_options.ml}
+\ocamlinput{./tutorial/hello/v5-multiple/hello_options.ml}
\scodeidx{Plugin}{Register}
\listingname{./hello\_print.ml}
-\ocamlinput{./tutorial/hello/generated/makefile_multiple/hello_print.ml}
+\ocamlinput{./tutorial/hello/v5-multiple/hello_print.ml}
\listingname{./hello\_run.ml}
-\ocamlinput{./tutorial/hello/generated/makefile_multiple/hello_run.ml}
+\ocamlinput{./tutorial/hello/v5-multiple/hello_run.ml}
\sscodeidx{Db}{Main}{extend}
The plug-in can be tested again by running:
\begin{shell}
-\$ make
-\$ make install
+\$ dune build
+\$ dune install
<...>
\$ frama-c -hello -hello-output hello.out
\$ more hello.out
@@ -504,192 +476,291 @@ Frama-C supports non-regression testing of plug-ins. This is useful to check
that further plug-in modifications do not introduce new bugs. The tool allowing
to perform the tests is called \ptests\index{Ptests}.
-To build these tests, the location of the subdirectories containing them must
-be indicated in the \texttt{Makefile} through the variable
-\texttt{PLUGIN\_TESTS\_DIRS}\codeidx{PLUGIN\_TESTS\_DIRS} set at
-\texttt{hello} as this will be the name of the
-subdirectory of \texttt{.tests/} where the plug-in's tests will be located:
+\begin{important}
+ Historically, \texttt{ptests} was developed before \framac used Dune. It was
+ adapted to Dune to maintain backwards compatibility, but new plug-ins may
+ prefer using Dune's test sytem directly.
+\end{important}
-\listingname{./Makefile}
-\codeidx{Makefile.dynamic}
-\codeidx{FRAMAC\_SHARE}
-\codeidx{PLUGIN\_CMO}
-\codeidx{PLUGIN\_NAME}
-\codeidx{PLUGIN\_TESTS\_DIRS}
-\makefileinput{./tutorial/hello/generated/with_test/Makefile}
+This is the general layout of the \texttt{tests} directory in a \framac
+plug-in; each file will be explained later.
-This enables the creation of a
-\texttt{./tests/ptests\_config} file holding the environement needed by
-\ptests to run the plug-in's tests by running:
-\begin{shell}
-\$ mkdir tests
-\$ make
-<...>
-Generating tests/ptests_config
+\begin{shell}[breaklines=true]
+<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{shell}
-For non-regression testing, the current behaviour of a program is taken as
+Inside the \texttt{tests} directory, \verb|ptests_config| lists the
+{\em test suites}, \ie directories containing tests.
+
+\listingname{./tests/ptests\_config}
+\makefileinput{./tutorial/hello/v5-multiple/tests/ptests_config}
+
+Small plug-ins typically have a single test directory with the plug-in name.
+
+Then, a default configuration must be provided for the tests. This is done by
+adding a \texttt{test\_config} file to the \texttt{tests} directory.
+
+\listingname{./tests/test\_config}
+\makefileinput{./tutorial/hello/v5-multiple/tests/test_config}
+
+This configuration must include the plug-ins required by the test; usually, the
+plug-in itself, but also other plug-ins on which it depends. The plug-in name
+is the one provided in the \texttt{plugin} section of the \texttt{dune} file.
+
+For non-regression testing, the current behavior of a program is taken as
the oracle against which future versions will be tested. In this tutorial, the
test will be about the correct \texttt{Hello, world!} output made by the option
\texttt{-hello} of the plug-in.
-Each test directory must contain a
+Each test file should contain a
\texttt{run.config}\index{Test!Configuration}\index{Test!Header}
-comment with the test directives\index{Test!Directive} and the C
-source code used for the test.
-(There are other ways to declare and control tests as developed
-in Section~\ref{ptests:configuration}.)
-For this tutorial, there will be no such source code. A file
-\texttt{./tests/hello/hello\_test.c} is then created:
+comment with test directives\index{Test!Directive} and the C
+source code used for the test (note: there are other ways to declare and
+control tests, as detailed in Section~\ref{ptests:configuration}).
+
+For this tutorial, no actual C code is needed, so
+\texttt{./tests/hello/hello\_test.c} will only contain the run.config header:
\listingname{./tests/hello/hello\_test.c}
\nscodeidx{Test!Directive}{OPT}
-\lstinputlisting[style=c]{./tutorial/hello/generated/with_test/tests/hello/hello_test.c}
+\lstinputlisting[style=c]{./tutorial/hello/v5-multiple/tests/hello/hello_test.c}
-In this file, there is only one directive
-\texttt{OPT: -hello}\nscodeidx{Test!Directive}{OPT} which requires
-to run \framac on this test with the \texttt{-hello} option.
-A look at Section~\ref{ptests:directives} gives you an idea of the kind of
+In this file, there is only one directive,
+\texttt{OPT: -hello}\nscodeidx{Test!Directive}{OPT}, which specifies that
+\framac will set option \texttt{-hello} when running the test.
+A look at Section~\ref{ptests:directives} gives you an idea of the kinds of
directives which can be used to test plug-ins.
-Once the \texttt{run.config} has been configured, it becomes possible to
-get the output generated by the plug-in:
+Once \texttt{run.config} has been configured, it becomes possible to generate
+Dune test files via the \ptests tool:
+
\begin{shell}[breaklines=true]
-\$ ptests.opt -show
-Env:
-<...>
-Command:
-/usr/local/bin/frama-c.byte tests/hello/hello_test.c -check -hello 2>tests/hello/result/hello_test.err.log >tests/hello/result/hello_test.res.log
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing tests/hello/hello_test.c (with preprocessing)
-[hello] Hello, world!
-Env:
-<...>
-Command:
-<...>
+\$ frama-c-ptests tests
+Test directory: tests
+Total number of generated dune files: 2
\end{shell}
-The option \texttt{-show} runs the tests and shows the output
-(but not their examination). Other options are detailed
-in Section~\ref{ptests:options} to give a better idea of the
-extent to which \ptests is configurable.
-Under \texttt{Env} is displayed the context (coming from the file
-\texttt{./hello/ptests\_config}).
-Then, \texttt{Command} shows the executed command for this test case followed
-by bash pipes to control the dataflow. (Note the \texttt{-hello}
-option which has been passed to \framac as requested by \texttt{OPT: -hello}
-in the \texttt{run.config}.)
-Two outputs are considered as results for each test:
-an \emph{error} output and a \emph{result} output.
-These outputs are logged in the two following files:
-\texttt{./tests/hello/result/hello\_test.err.log} and
-\texttt{./tests/hello/result/hello\_test.res.log}.
-The three lines beginning by \texttt{[kernel]} and \texttt{[hello]}
-are the actual non-erroneous outputs made by \framac: two of them are generated
-by the kernel (which could be muted by changing the verbosity) while the third
-one is generated by our plug-in \texttt{Hello}. \texttt{Env} and
-\texttt{Command} parts appear once again because some test strategies need it,
-which is not the case in the simple setting of this tutorial.
-
-Once you have verified the output is as expected, set it as an
-oracle to be used for later non-regression tests by running:
+
+This must be done each time a test configuration is modified or a test file or
+directory is added.
+
+Then, one can execute the tests and get the output generated by the plug-in:
+
+\begin{shell}[breaklines=true]
+\$ dune build @tests/ptests
+Files ../oracle/hello_test.res.oracle and hello_test.res.log differ
+% dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
+(cd _build/default/tests/hello/result && diff --new-file "hello_test.res.log"
+"../oracle/hello_test.res.oracle")
+File "tests/hello/oracle/hello_test.res.oracle", line 1, characters 0-0:
+diff --git a/_build/default/tests/hello/oracle/hello_test.res.oracle
+ b/_build/default/tests/hello/result/hello_test.res.log
+index e69de29..5f6ab23 100644
+--- a/_build/default/tests/hello/oracle/hello_test.res.oracle
++++ b/_build/default/tests/hello/result/hello_test.res.log
+@@ -0,0 +1,2 @@
++[kernel] Parsing hello_test.c (with preprocessing)
++[hello] Hello, world!
+\end{shell}
+
+There is a lot of information in the output. The relevant parts
+can be summarized as:
+
+\begin{itemize}
+\item Dune runs its tests inside a {\em sandboxed} environment, in directory
+ \verb|_build/default|, which is (approximately) a copy of the plug-in
+ file tree;
+\item Dune compared two files, none of which existed before running the test:
+ \verb|result/hello_test.res.log| and \verb|oracle/hello_test.res.oracle|;
+\item The last lines (which should be colored, if your terminal supports colors)
+ show the textual difference between the expected and actual outputs.
+\end{itemize}
+
+The first file, \verb|result/hello_test.res.log|, is the {\em actual} output of
+the execution of the test command.
+The second file, \verb|oracle/hello_test.res.oracle|, is the {\em expected}
+output of the test.
+
+The result file is re-generated each time the test is run.
+The oracle file, however, is supposed to exist beforehand
+(unless the test produces no output).
+
+In reality, there are 2 pairs of files for each test: a pair
+\texttt{.res.\{log,oracle\}} and another \texttt{.err.\{log,oracle\}}.
+The first one contains results sent to the standard output ({\em stdout}),
+while the second one contains messages sent to the standard error
+({\em stderr}). In our example, the error output is empty, so it generates no
+differences. Note that Dune only outputs messages in case of errors,
+\ie tests producing the expected result are silent.
+
+Finally, concerning the actual diff in the test (last two lines), the first
+line (starting with \texttt{[kernel]}) is emitted by the \framac kernel,
+and the second one is our plug-in's result, as expected.
+
+Once you have verified the actual output is the one {\em you} expected,
+you can {\em promote} it to the status of ``official oracle'' for future
+non-regression tests, by running:
+\begin{shell}
+\$ dune promote
+\end{shell}
+Note, however, that if the oracles do not exist, they must be created:
+\begin{shell}
+\$ frama-c-ptests -create-missing-oracles tests
+\$ dune promote
+\end{shell}
+
+The option \texttt{-create-missing-oracles} always creates both result and
+error oracles. Most of the time, however, only the former is useful.
+After promoting tests, it is useful to remove empty oracles:
+
\begin{shell}
-\$ ptests.opt -update
+\$ frama-c-ptests -remove-empty-oracles tests
\end{shell}
-This command copies the two log files to
-\texttt{./tests/hello/oracle/hello\_test.err.oracle} and
-\texttt{./tests/hello/oracle/hello\_test.res.oracle}.
-The setting of this test case is now finished.
-Let's now assume the plug-in is later erroneously modified as follows:
+\begin{important}
+ Once your plug-in has test files, the \verb|dune build| command presented
+ earlier will not only compile your plug-in, but also run its tests.
+ Therefore, if you want to simply compile it, you will have to run
+ \verb|dune build @install| instead. Despite the name, the command will
+ {\em not} install your plug-in (that is performed by \verb|dune install|).
+\end{important}
+
+Now, let's introduce an error. Assume the plug-in has been modified as follows:
\listingname{./hello\_run.ml}
-\ocamlinput{./tutorial/hello/generated/with_test/hello_run_bug.ml}
+\ocamlinput{./tutorial/hello/v6-test-with-bug/hello_run.ml}
\sscodeidx{Db}{Main}{extend}
-where \texttt{Hello, world!} is incorrectly changed to \texttt{Hello world!}.
-Running the command:
+We assume that ``\texttt{Hello, world!}'' has been unintentionally changed to
+``\texttt{Hello world!}''.
+Running these commands:
\begin{shell}[breaklines=true]
-\$ make
-<...>
-\$ make tests
-TESTING PLUG-IN Hello
-% Dispatch finished, waiting for workers to complete
-Env:
-<...>
-Command:
+\$ dune build @install
<...>
-% Comparisons finished, waiting for diffs to complete
---- tests/hello/oracle/hello_test.res.oracle 2017-06-02 14:39:49.407624816 +0200
-+++ tests/hello/result/hello_test.res.log 2017-06-02 14:40:03.483624679 +0200
-@@ -1,3 +1,3 @@
- [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
- [kernel] Parsing tests/hello/hello_test.c (with preprocessing)
+\$ dune build @tests/ptests
+Files ../oracle/hello_test.res.oracle and hello_test.res.log are different
+% dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
+ (cd _build/default/tests/hello/result && diff --new-file "hello_test.res.log" "../oracle/hello_test.res.oracle")
+File "tests/hello/oracle/hello_test.res.oracle", line 1, characters 0-0:
+diff --git a/_build/default/tests/hello/oracle/hello_test.res.oracle b/_build/default/tests/hello/result/hello_test.res.log
+index 5f6ab2389a..cf2e5c010c 100644
+--- a/_build/default/tests/hello/oracle/hello_test.res.oracle
++++ b/_build/default/tests/hello/result/hello_test.res.log
+@@ -1,2 +1,2 @@
+ [kernel] Parsing hello_test.c (with preprocessing)
-[hello] Hello, world!
+[hello] Hello world!
-% Diffs finished. Summary:
-Run = 1
-Ok = 1 of 2
-Time = 0.380000 s.
-real 0.45
-user 0.38
-sys 0.03
\end{shell}
-displays the differences (Ã la \texttt{diff}) between the current executions
-and the saved oracles. Here the diff clearly shows that the only difference is
+displays the differences (Ã la \texttt{diff}) between the current execution
+and the saved oracles. Here, the diff clearly shows that the only difference is
the missing comma in the generated message due to our (erroneous) modification.
-One test is marked as being successful: that is the test comparing
-\texttt{stderr} (which contains an empty string). After fixing the \ocaml code,
-running \texttt{make \&\& make tests} again shows that all test cases are
-successful.
+After fixing the \ocaml code, running again the previous commands shows that all
+test cases are successful.
-You may use other \framac's plug-ins as examples of how to integrate a
+You may check other \framac plug-ins as examples of how to integrate a
plug-in with \ptests. Small plug-ins such as \texttt{Report} and
\texttt{Variadic} are good examples (see directories
-\texttt{src/plugins/report/tests/} and \texttt{src/plugins/variadic/tests/}).
+\texttt{src/plugins/report/tests} and \texttt{src/plugins/variadic/tests}).
Please note \framac offers no particular support for other kinds of testing
-purposes, such as test-driven development (TDD)\footnote{For the purpose of
-driving the development of a plug-in, one should have to manually create
-\texttt{./tests/*/oracle/*.err.oracle} and
-\texttt{./tests/*/oracle/*.res.oracle} files for example.} for instance.
+purposes, such as test-driven development (TDD)\footnote{For instance, one
+required feature for TDD that \texttt{ptests} does not support, is to
+{\em force} the user to manually create \texttt{./tests/*/oracle/*.oracle}
+files before running a new test.}.
Additional information about plug-in testing is available in
Sections~\ref{adv:ptests} and~\ref{sec:ptests}.
+\subsubsection{Summary of Testing Operations}
+
+Here's a summarized list of operations in order to add a new test:
+
+\begin{enumerate}
+\item Create a test case (\texttt{.c} or \texttt{.i} file in
+ \texttt{tests/<suite>}).
+\item Add a \texttt{run.config} header to the test.
+\item \verb|frama-c-ptests|
+\item \verb|frama-c-ptests -create-missing-oracles|
+\item \verb|dune build @tests/ptests|
+\item Manually inspect oracle diffs to check that they are ok.
+\item \verb|dune promote|
+\item \verb|frama-c-ptests -remove-empty-oracles|
+\end{enumerate}
+
+Operations to perform when modifying the plug-in code:
+
+\begin{enumerate}
+\item \verb|dune build @install|
+\item \verb|dune build @tests/ptests|
+\item If there are expected diffs, run \verb|dune promote|;
+ otherwise, fix code and re-run the first steps.
+\end{enumerate}
+
\subsection{Documenting your Source Code}
\label{tut2:doc}
\index{Plug-in!Documentation}
-\framac automatically generates the documentation of plug-ins when the command
-\texttt{make doc} is run\footnote{Frama-C kernel needs to have been
-installed with code documentation support. If this was not the case, you can
-run \texttt{make doc install-doc-code} in Frama-C's main directory as hinted
-by the error message appearing in the terminal before trying again to generate
-the documentation of the plug-in.}. This relies on \ocamldoc and
-requires the plug-in to be documented following the \ocamldoc guidelines
-(please refer to the corresponding chapter in \cite{caml}).
+One can generate the documentation of a plugin using the command:
+
+\lstinline{dune build @doc}
+
+This relies on \odoc and requires the plug-in to be documented following the
+\odoc guidelines (check \url{https://ocaml.github.io/odoc} for details).
We show here how the Hello plug-in could be slightly documented and use
-\ocamldoc features such as @-tags and cross references:
+\odoc features such as @-tags and cross references. First, we modify the
+\texttt{Hello.ml} file to export all inner modules, otherwise \odoc will not
+generate documentation for them:
+
+\listingname{./Hello.ml}
+\ocamlinput{./tutorial/hello/v7-doc/Hello.ml}
+
+Then, we add some documentation tags to our modules:
\listingname{./hello\_options.ml}
-\ocamlinput{./tutorial/hello/generated/with_doc/hello_options.ml}
+\ocamlinput{./tutorial/hello/v7-doc/hello_options.ml}
\scodeidx{Plugin}{Register}
\listingname{./hello\_print.ml}
-\ocamlinput{./tutorial/hello/generated/with_doc/hello_print.ml}
+\ocamlinput{./tutorial/hello/v7-doc//hello_print.ml}
\listingname{./hello\_run.ml}
-\ocamlinput{./tutorial/hello/generated/with_doc/hello_run.ml}
+\ocamlinput{./tutorial/hello/v7-doc//hello_run.ml}
\sscodeidx{Db}{Main}{extend}
-The documentation files of the plug-in are added to
-\texttt{./doc/code/} and the link to this
-is added to the plug-ins index file
-\texttt{./doc/code/index.html}.
+Running \verb|dune build @doc| will generate documentation files in
+\texttt{./\_build/default/\_doc/\_html}. Open \texttt{index.html} in your
+browser and navigate to see them. Note that \odoc may report some warnings
+due to absence of annotation data for \framac's modules:
+
+\begin{shell}
+Warning: Couldn't find the following modules:
+ Frama_c_kernel Frama_c_kernel__Plugin
+\end{shell}
+
+This should not prevent the generation of documentation for the library itself;
+but links to modules such as \texttt{Enabled} and \texttt{Output\_file} will
+not work.
-This simple tutorial now comes to its end. It focused on the standard features of
-architectures and interfaces of \framac plug-ins. A companion archive
+\subsection{Conclusion}
+
+This simple tutorial now comes to its end. It focused on the standard features
+of architectures and interfaces of \framac plug-ins. A companion archive
\texttt{hello.tar.gz} is available in the download section of the \framac
-website\footnote{The direct link is: \url{http://frama-c.com/download.html}.}.
+website\footnote{The direct link is:
+\url{https://www.frama-c.com/download/hello.tar.gz}.}.
The next tutorial will make you dive in \C analysis.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -699,11 +770,10 @@ The next tutorial will make you dive in \C analysis.
In this section, we create a new ViewCfg plug-in that computes the control
flow graph of a function and outputs it in the \dottool format. Through its
implementation, we explain some of \framac APIs such as how to visit
-an AST\footnote{Abstract Syntax Tree}, to hook a plug-in, to interface
-a plug-in with other plug-ins, to extend the
-GUI\footnote{Graphical User Interface}, to make a plug-in usable by
-others, to configure a script,
-and to make a plug-in usable in a multi-projects setting.
+an AST\footnote{Abstract Syntax Tree}, how to hook a plug-in, how to interface
+a plug-in with other plug-ins, how to extend the
+GUI\footnote{Graphical User Interface}, how to make a plug-in usable by
+others, and how to make a plug-in usable in a multi-project setting.
This section assumes the reader is already familiar with the basics of plug-ins
for \framac as covered by the Hello plug-in in the previous
@@ -713,7 +783,7 @@ section.
\index{Visitor}
Writing an analysis for \C programs is the primary purpose of a \framac
-plug-in. That usually requires to visit the AST to compute information for some
+plug-in. That usually requires visiting the AST to compute information for some
\C constructs. There are two different ways of doing that in \framac:
\begin{itemize}
\item through a direct recursive descent; or
@@ -727,12 +797,12 @@ to combine both ways to tune it to specific needs.
\subsubsection*{Pretty-printing with direct recursive descent}
Frama-C already has a function to pretty-print statements (namely
-\texttt{Printer.pp\_stmt}\scodeidx{Printer\_api}{S.pp\_stmt}), but it is not suitable
-for us, as it will recursively print substatements of compound statements
-(blocks, if, while, ...) while we only want to pretty print the node representing the
-current statement: substatements will be represented by other nodes. Thus we
-will use the following small function:
-\ocamlinput{./tutorial/viewcfg/src/print_stmt.ml}
+\texttt{Printer.pp\_stmt}\scodeidx{Printer\_api}{S.pp\_stmt}), but it is not
+suitable for us, as it will recursively print substatements of compound
+statements (blocks, if, while, ...), while we only want to pretty-print
+the node representing the current statement: substatements will be represented
+by other nodes. Thus we will use the following small function:
+\ocamlinput[firstline=29,lastline=43]{./tutorial/viewcfg/v1/view_cfg.ml}
\sscodeidx{Cil\_types}{stmtkind}{Instr}
\sscodeidx{Cil\_types}{stmtkind}{Return}
\sscodeidx{Cil\_types}{stmtkind}{Goto}
@@ -752,22 +822,24 @@ The \texttt{Cil\_types} module contains the definition of the AST of a \C
program, like constructors \texttt{Cil\_types.Instr},
\texttt{Cil\_types.Return}, and so on which are of type
\texttt{Cil\_types.stmtkind}. The \texttt{Printer} module contains
-functions that prints the different Cil types. The documentation of these module
+functions that print the different Cil types. The documentation of these module
is available on the \framac website\footnote{From
- \url{http://frama-c.com/download.html}.}, or by typing \texttt{make doc} in
+\url{https://www.frama-c.com/html/framac-versions.html};
+look for {\em API Documentation} inside the page corresponding to your \framac
+version.}, or by typing \texttt{make doc} in
the \framac source distribution.
\subsubsection*{Creating the graphs with a visitor}
In order to create our output, we must make a pass through the whole
-AST. An easy way to do that is to use \framac visitor mechanism. A
+AST. An easy way to do that is to use the \framac visitor mechanism. A
visitor is a class with one method per type of the AST, whose default
behavior is to just call the method corresponding to each of its
children. By inheriting from the visitor, and redefining some of the
methods, one can perform actions on selected parts of the AST, without
the need to traverse the AST explicitly.
-\ocamlinput{./tutorial/viewcfg/src/print_cfg_begin.ml}
+\ocamlinput[firstline=45,lastline=46]{./tutorial/viewcfg/v1/view_cfg.ml}
\scodeidx{Visitor}{frama\_c\_inplace}
Here we used the so-called ``in place'' visitor, which should be used for
@@ -777,21 +849,25 @@ section~\ref{sec:visitors-projects}).
There are three kinds of nodes where we have something to do. First,
at the file level, we create the whole graph structure.
+%\footnote{{\em Note}:
+%in the code below, the fancy 'at'-terms such as ``\texttt{@[<hov 2>}'' are
+% related to OCaml's Format module, and can be ignored for now.}.
-\ocamlinput{./tutorial/viewcfg/src/print_cfg_vfile.ml}
+\ocamlinput[firstline=48,lastline=50]{./tutorial/viewcfg/v1/view_cfg.ml}
\sscodeidx{Cil}{visitAction}{DoChildrenPost}
\sscodeidx{Cil}{cilVisitor}{vfile}
\texttt{Cil.DoChildrenPost} is one of the possible
-\texttt{visitAction}, that tells the visitor what to do after the
+\texttt{visitAction}\,s, that tells the visitor what to do after the
function is executed. With \texttt{DoChildrenPost func}, the \texttt{func}
-argument is called once the children have been executed: here we close the
-parenthesis once that all functions have been printed in the file.
+argument is called once, after all children have been executed. Therefore,
+we use it to close the curly braces after all functions have been printed
+in the file.
Then, for each function, we encapsulate the CFG in a subgraph, and do
nothing for the other globals.
-\ocamlinput{./tutorial/viewcfg/src/print_cfg_vglob.ml}
+\ocamlinput[firstline=52,lastline=58]{./tutorial/viewcfg/v1/view_cfg.ml}
\sscodeidx{Cil}{visitAction}{DoChildrenPost}
\sscodeidx{Cil}{visitAction}{SkipChildren}
\sscodeidx{Visitor}{frama\_c\_visitor}{vglob\_aux}
@@ -806,7 +882,7 @@ should have been used instead.}.
Last, for each statement, we create a node in the graph, and create
the edges toward its successors:
-\ocamlinput{./tutorial/viewcfg/src/print_cfg_vstmt_aux_novalue.ml}
+\ocamlinput[firstline=60,lastline=65]{./tutorial/viewcfg/v1/view_cfg.ml}
\sscodeidx{Cil}{visitAction}{DoChildren}
\sscodeidx{Visitor}{frama\_c\_visitor}{vstmt\_aux}
@@ -815,21 +891,49 @@ This code could be optimized, for instance by replacing the final
cannot contain other statements, like \texttt{Instr}, and avoid
visiting the expressions.
-Finally we close the \texttt{object} definition:
-\ocamlinput{./tutorial/viewcfg/src/print_cfg_end.ml}
+Finally, we close the \texttt{object} definition:
+\ocamlinput[firstline=67,lastline=67]{./tutorial/viewcfg/v1/view_cfg.ml}
\subsubsection*{Hooking into \framac}
-It just remains to hook this script into \framac.
+Now we need to ensure the code is called at the appropriate time when
+\framac is run. Note that if we simply add a function at the toplevel
+(\ie \verb|let () = run ()|), it will {\em not} work, because \framac
+will not have had the time to parse the sources and produce its AST
+(used by \verb|Ast.get ()|). For more details about initialization issues,
+see Section~\ref{adv:init}.
+
+\ocamlinput[firstline=69,lastline=75]{./tutorial/viewcfg/v1/view_cfg.ml}
+
+Now, since \framac uses Dune, this code needs to be integrated as a Dune
+project, as has been done in the Hello tutorial. We need to create a new
+directory. In it, we will put all of the code seen so far, in an \texttt{.ml}
+file. We will then add the corresponding \texttt{dune} and
+\texttt{dune-project} files:
+
+\listingname{dune}
+\duneinput[linerange={23-999}]{./tutorial/viewcfg/v1/dune}
-\ocamlinput{./tutorial/viewcfg/src/extend_with_simple_run.ml}
+\listingname{dune-project}
+\duneinput[linerange={1-1,24-999}]{./tutorial/viewcfg/v1/dune-project}
+
+Finally, we need an (empty) interface file, called \texttt{ViewCfg.ml}, in
+the same directory.
+
+With all of this, we can compile the project with:
+
+\begin{shell}
+ dune build
+\end{shell}
+
+And run it as a \framac plugin:
-Assuming the script is called \texttt{cfg\_print.ml}, it can then be run with:
\begin{shell}
- frama-c -load-script cfg_print.ml [other_options] file.c [file2.c]
+ dune exec -- frama-c [options] file.c [file2.c]
\end{shell}
-And the graph can be visualized with
+And the graph can be visualized with an external tool, such as {\em dotty} or
+{\em xdot}.
\begin{shell}
dotty cfg.out
\end{shell}
@@ -856,24 +960,23 @@ There are many possible enhancements to this code:
\begin{itemize}
\item There is a bug when trying to print statements that contain
- strings (such as \verb|printf("Hello\n")| such statements must be
- protected using the \verb|"%S"| Format directive;
-\item The script could be transformed into a regular plug-in, by
- registering into \framac, and taking options from the command line;
- for instance to compute the control flow graph of a single function
- given as an argument;
+ strings (such as \verb|printf("Hello\n")|, due to double quotes.
+ Such statements must be protected using the \verb|"%S"| Format directive;
+\item The plug-in could be properly registered as such, allowing it to
+ accept command-line options, for instance to compute the control flow graph
+ of a single function given as argument;
\item The graphs could be fancier, in particular by distinguishing
- between branching nodes and plain ones, or showing exit of blocks as
- well as their beginning; or linking a call with the called function.
+ between branching nodes and plain ones, or showing block entries and exits;
+ or linking call sites to the called functions.
\end{itemize}
We will concentrate on another extension, which is to reuse the
-analysis of the \texttt{value} \framac plug-in to color unreachable
-nodes.
+analysis of the \texttt{Eva} plug-in to color unreachable nodes.
To do so, because we will combine different plug-ins, we need to ensure their
-correct ordering. This requires the definition of some command-line options.
+correct ordering. This requires the definition of some command-line options
+for our plug-in.
-\subsection{Plug-In registration and command-line options}\label{tut2:options}
+\subsection{Plug-in registration and command-line options}\label{tut2:options}
\index{Plug-in!Command Line Options}\index{Command Line}
We have already seen how to register options in the previous ``Hello'' tutorial.
@@ -1111,10 +1214,6 @@ Here is the listing for the different modules:
% TODO: A script that uses "dump_function" of the CFG plug-in
-\subsection{Writing a Configure Script}\label{tut2:configure}
-\index{Plug-in!Configure}
-\todo
-
% Detect \dottool at compile time.
% Link to section 5.3: plug-in specific configure.in
diff --git a/doc/developer/tutorial/hello/Makefile b/doc/developer/tutorial/hello/Makefile
index dd02c5be8ac68f3ef4afcc543972662f200ea40c..e3d5af7cece0d9a7e1b5d01cad919acf752ed9c0 100644
--- a/doc/developer/tutorial/hello/Makefile
+++ b/doc/developer/tutorial/hello/Makefile
@@ -20,23 +20,35 @@
# #
##########################################################################
-PLUGIN_DIRS = script with_registration with_log makefile_single makefile_multiple with_options with_test with_doc
+PLUGIN_DIRS = empty simple with_registration with_log multiple with_options with_test with_doc
FINAL_PLUGINS = $(patsubst %,generated/%,$(PLUGIN_DIRS))
DIRS = generated $(addprefix generated/, src $(PLUGIN_DIRS))
-MLIS=$(addsuffix /Hello.mli,$(filter-out generated, $(DIRS)))
-all: clean $(FINAL_PLUGINS) $(MLIS)
+all: clean $(FINAL_PLUGINS)
-generated/src/Makefile%: src/Makefile%
+generated/src/dune: src/dune
mkdir -p $(dir $@)
cp $< $@
- headache -r $@
+ headache -c ../../../../headers/headache_config.txt -r $@
+
+generated/src/dune-project: src/dune-project
+ mkdir -p $(dir $@)
+ cp $< $@
+ headache -c ../../../../headers/headache_config.txt -r $@
generated/src/%.ml: src/%.ml
mkdir -p $(dir $@)
cp $< $@
headache -r $@
+generated/src/tests/ptests_config: src/ptests_config
+ mkdir -p $(dir $@)
+ cp $< $@
+
+generated/src/tests/test_config: src/test_config
+ mkdir -p $(dir $@)
+ cp $< $@
+
generated/src/tests/hello/%.c: src/%.c
mkdir -p $(dir $@)
cp $< $@
@@ -46,58 +58,77 @@ generated/src/tests/hello/oracle/%.oracle: src/%.oracle
mkdir -p $(dir $@)
cp $< $@
-generated/%/Hello.mli: src/Hello.mli
+generated/%/Hello.ml: src/Hello.ml
mkdir -p $(dir $@)
cp $< $@
headache -r $@
-generated/script: generated/src/run_print_to_file.ml \
+generated/empty: generated/src/dune \
+ generated/src/dune-project \
+ generated/src/Hello.ml
+ mkdir -p $@
+ cp generated/src/dune $@/dune
+ cp generated/src/dune-project $@/dune-project
+ cp generated/src/Hello.ml $@/Hello.ml
+
+generated/simple: generated/empty \
+ generated/src/run_print_to_file.ml \
generated/src/extend_run.ml
mkdir -p $@
- for i in $^; do cat $$i >> $@/hello_world.ml; echo "" >> $@/hello_world.ml; done
+ cp generated/empty/* $@
+ for i in $(filter %.ml, $^); do \
+ cat $$i >> $@/hello_world.ml; \
+ echo "" >> $@/hello_world.ml; \
+ done
-generated/with_registration: generated/src/help_msg.ml \
+generated/with_registration: generated/empty \
+ generated/src/help_msg.ml \
generated/src/register.ml \
generated/src/run_print_to_file.ml \
generated/src/extend_run.ml
mkdir -p $@
- for i in $^; do cat $$i >> $@/hello_world.ml; echo "" >> $@/hello_world.ml; done
+ cp generated/empty/* $@
+ for i in $(filter %.ml, $^); do \
+ cat $$i >> $@/hello_world.ml; \
+ echo "" >> $@/hello_world.ml; \
+ done
-generated/with_log: generated/src/help_msg.ml \
+generated/with_log: generated/empty \
+ generated/src/help_msg.ml \
generated/src/register.ml \
generated/src/run_log.ml \
generated/src/extend_run.ml
mkdir -p $@
- for i in $^; do cat $$i >> $@/hello_world.ml; echo "" >> $@/hello_world.ml; done
+ cp generated/empty/* $@
+ for i in $(filter %.ml, $^); do \
+ cat $$i >> $@/hello_world.ml; \
+ echo "" >> $@/hello_world.ml; \
+ done
-generated/with_options: generated/src/help_msg.ml \
+generated/with_options: generated/empty \
+ generated/src/help_msg.ml \
generated/src/register.ml \
generated/src/options_enabled.ml \
generated/src/options_output_file.ml \
generated/src/run_with_options.ml \
- generated/src/extend_run.ml \
- generated/src/Makefile.single-file
+ generated/src/extend_run.ml
mkdir -p $@
- cp generated/src/Makefile.single-file $@/Makefile
- for i in $(filter-out generated/src/Makefile.single-file, $^); do \
+ cp generated/empty/* $@
+ for i in $(filter %.ml, $^); do \
cat $$i >> $@/hello_world.ml; \
echo "" >> $@/hello_world.ml; \
done
-generated/makefile_single: generated/with_options generated/src/Makefile.single-file
- mkdir -p $@
- cp generated/with_options/hello_world.ml $@/hello_world.ml
- cp generated/src/Makefile.single-file $@/Makefile
-
-generated/makefile_multiple: generated/src/help_msg.ml \
- generated/src/register.ml \
- generated/src/options_enabled.ml \
- generated/src/options_output_file.ml \
- generated/src/print.ml \
- generated/src/run_call_print.ml \
- generated/src/extend_run.ml \
- generated/src/Makefile.multiple-files
+generated/multiple: generated/empty \
+ generated/src/help_msg.ml \
+ generated/src/register.ml \
+ generated/src/options_enabled.ml \
+ generated/src/options_output_file.ml \
+ generated/src/print.ml \
+ generated/src/run_call_print.ml \
+ generated/src/extend_run.ml
mkdir -p $@
+ cp generated/empty/* $@
cp generated/src/help_msg.ml $@/hello_options.ml
echo "" >> $@/hello_options.ml
cat generated/src/register.ml >> $@/hello_options.ml
@@ -109,25 +140,25 @@ generated/makefile_multiple: generated/src/help_msg.ml \
cp generated/src/run_call_print.ml $@/hello_run.ml
echo "" >> $@/hello_run.ml
cat generated/src/extend_run.ml >> $@/hello_run.ml
- cp generated/src/Makefile.multiple-files $@/Makefile
-generated/with_test: generated/src/run_call_print_bug.ml \
- generated/src/tests/hello/hello_test.c \
- generated/src/tests/hello/oracle/hello_test.res.oracle \
- generated/src/Makefile.test
+generated/with_test: generated/multiple \
+ generated/src/run_call_print_bug.ml \
+ generated/src/tests/ptests_config \
+ generated/src/tests/test_config \
+ generated/src/tests/hello/hello_test.c
mkdir -p $@
- cp generated/makefile_multiple/hello_options.ml $@/hello_options.ml
- cp generated/makefile_multiple/hello_print.ml $@/hello_print.ml
- cp generated/makefile_multiple/hello_run.ml $@/hello_run.ml
- cp generated/src/run_call_print_bug.ml $@/hello_run_bug.ml
- echo "" >> $@/hello_run_bug.ml
- cat generated/src/extend_run.ml >> $@/hello_run_bug.ml
- mkdir -p $@/tests/hello/oracle
+ cp generated/multiple/* $@
+ cp generated/src/run_call_print_bug.ml $@/hello_run.ml.bug
+ echo "" >> $@/hello_run.ml.bug
+ cat generated/src/extend_run.ml >> $@/hello_run.ml.bug
+ mkdir -p $@/tests
+ cp generated/src/tests/ptests_config $@/tests/ptests_config
+ cp generated/src/tests/test_config $@/tests/test_config
+ mkdir -p $@/tests/hello
cp generated/src/tests/hello/hello_test.c $@/tests/hello/hello_test.c
- cp generated/src/tests/hello/oracle/hello_test.res.oracle $@/tests/hello/oracle/hello_test.res.oracle
- cp generated/src/Makefile.test $@/Makefile
-generated/with_doc: generated/src/help_msg.ml \
+generated/with_doc: generated/empty \
+ generated/src/help_msg.ml \
generated/src/register.ml \
generated/src/options_enabled.ml \
generated/src/options_output_file.ml \
@@ -145,9 +176,9 @@ generated/with_doc: generated/src/help_msg.ml \
generated/src/hello_print.doc.ml \
generated/src/hello_run.doc.ml \
generated/src/tests/hello/oracle/hello_test.err.oracle \
- generated/src/tests/hello/oracle/hello_test.res.oracle \
- generated/src/Makefile.test
+ generated/src/tests/hello/oracle/hello_test.res.oracle
mkdir -p $@
+ cp generated/empty/* $@
cp generated/src/hello_options.doc.ml $@/hello_options.ml
echo "" >> $@/hello_options.ml
cat generated/src/help_msg.doc.ml >> $@/hello_options.ml
@@ -177,7 +208,6 @@ generated/with_doc: generated/src/help_msg.ml \
mkdir -p $@/tests/hello/oracle
cp generated/src/tests/hello/oracle/hello_test.err.oracle $@/tests/hello/oracle/hello_test.err.oracle
cp generated/src/tests/hello/oracle/hello_test.res.oracle $@/tests/hello/oracle/hello_test.res.oracle
- cp generated/src/Makefile.test $@/Makefile
tests:
cd generated/script && frama-c -load-script hello_world.ml && cat hello.out
diff --git a/doc/developer/tutorial/hello/src/Hello.mli b/doc/developer/tutorial/hello/src/Hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/src/Hello.mli
rename to doc/developer/tutorial/hello/src/Hello.ml
diff --git a/doc/developer/tutorial/hello/src/dune b/doc/developer/tutorial/hello/src/dune
new file mode 100644
index 0000000000000000000000000000000000000000..e0125f3b102d9ed180a10e5cf5239a677255fdba
--- /dev/null
+++ b/doc/developer/tutorial/hello/src/dune
@@ -0,0 +1,34 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/src/dune-project b/doc/developer/tutorial/hello/src/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..940532b87b78a614c725ac1e6b99cb0f3e5ed449
--- /dev/null
+++ b/doc/developer/tutorial/hello/src/dune-project
@@ -0,0 +1,27 @@
+(lang dune 3.0)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/src/hello_test.c b/doc/developer/tutorial/hello/src/hello_test.c
index 9fcbfc12af7290704fe8367dfa4c18c556751347..d2f4ef3e1bfd30db301c62a3108511e6f6289e55 100644
--- a/doc/developer/tutorial/hello/src/hello_test.c
+++ b/doc/developer/tutorial/hello/src/hello_test.c
@@ -1,4 +1,3 @@
/* run.config
- PLUGIN: Hello
OPT: -hello
*/
diff --git a/doc/developer/tutorial/hello/src/ptests_config b/doc/developer/tutorial/hello/src/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..cd6b8a2ceb30bce514102e1619415edd1ae2cf56
--- /dev/null
+++ b/doc/developer/tutorial/hello/src/ptests_config
@@ -0,0 +1,2 @@
+DEFAULT_SUITES= hello
+
diff --git a/doc/developer/tutorial/hello/src/run_call_print_bug.ml b/doc/developer/tutorial/hello/src/run_call_print_bug.ml
index d8a6411872d0364879c0236ed6551e3f8138a66e..6942999ee4650ce0dc6ac56549db496c58eeeb19 100644
--- a/doc/developer/tutorial/hello/src/run_call_print_bug.ml
+++ b/doc/developer/tutorial/hello/src/run_call_print_bug.ml
@@ -1,3 +1,3 @@
let run () =
if Hello_options.Enabled.get() then
- Hello_print.output "Hello world!"
+ Hello_print.output "Hello world!" (* removed comma *)
diff --git a/doc/developer/tutorial/hello/src/test_config b/doc/developer/tutorial/hello/src/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2a2d5950338b6ac669e5f0b8cb0203909e1ac612
--- /dev/null
+++ b/doc/developer/tutorial/hello/src/test_config
@@ -0,0 +1 @@
+PLUGIN: hello
diff --git a/doc/developer/tutorial/hello/v1-simple/Hello.ml b/doc/developer/tutorial/hello/v1-simple/Hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/doc/developer/tutorial/hello/v1-simple/dune b/doc/developer/tutorial/hello/v1-simple/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7d352870c9efd577409ce95cd429ee8945083900
--- /dev/null
+++ b/doc/developer/tutorial/hello/v1-simple/dune
@@ -0,0 +1,12 @@
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/v1-simple/dune-project b/doc/developer/tutorial/hello/v1-simple/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f1eccde4e9e3b48c5909edf9f8099a850e91f731
--- /dev/null
+++ b/doc/developer/tutorial/hello/v1-simple/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/v1-simple/hello_world.ml b/doc/developer/tutorial/hello/v1-simple/hello_world.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4cc340bc30d2c07a6417f012e124d30c0d533825
--- /dev/null
+++ b/doc/developer/tutorial/hello/v1-simple/hello_world.ml
@@ -0,0 +1,11 @@
+let run () =
+ try
+ let chan = open_out "hello.out" in
+ Printf.fprintf chan "Hello, world!\n";
+ flush chan;
+ close_out chan
+ with Sys_error _ as exc ->
+ let msg = Printexc.to_string exc in
+ Printf.eprintf "There was an error: %s\n" msg
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/hello/v2-register/Hello.ml b/doc/developer/tutorial/hello/v2-register/Hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/doc/developer/tutorial/hello/v2-register/dune b/doc/developer/tutorial/hello/v2-register/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7d352870c9efd577409ce95cd429ee8945083900
--- /dev/null
+++ b/doc/developer/tutorial/hello/v2-register/dune
@@ -0,0 +1,12 @@
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/v2-register/dune-project b/doc/developer/tutorial/hello/v2-register/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f1eccde4e9e3b48c5909edf9f8099a850e91f731
--- /dev/null
+++ b/doc/developer/tutorial/hello/v2-register/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/v2-register/hello_world.ml b/doc/developer/tutorial/hello/v2-register/hello_world.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e5c74452edddbeadc9391e782b657e1b4b963dcf
--- /dev/null
+++ b/doc/developer/tutorial/hello/v2-register/hello_world.ml
@@ -0,0 +1,20 @@
+let help_msg = "output a warm welcome message to the user"
+
+module Self = Plugin.Register
+ (struct
+ let name = "hello world"
+ let shortname = "hello"
+ let help = help_msg
+ end)
+
+let run () =
+ try
+ let chan = open_out "hello.out" in
+ Printf.fprintf chan "Hello, world!\n";
+ flush chan;
+ close_out chan
+ with Sys_error _ as exc ->
+ let msg = Printexc.to_string exc in
+ Printf.eprintf "There was an error: %s\n" msg
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/hello/v3-log/Hello.ml b/doc/developer/tutorial/hello/v3-log/Hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/doc/developer/tutorial/hello/v3-log/dune b/doc/developer/tutorial/hello/v3-log/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7d352870c9efd577409ce95cd429ee8945083900
--- /dev/null
+++ b/doc/developer/tutorial/hello/v3-log/dune
@@ -0,0 +1,12 @@
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/v3-log/dune-project b/doc/developer/tutorial/hello/v3-log/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f1eccde4e9e3b48c5909edf9f8099a850e91f731
--- /dev/null
+++ b/doc/developer/tutorial/hello/v3-log/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/v3-log/hello_world.ml b/doc/developer/tutorial/hello/v3-log/hello_world.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3d9a51c9c604652a63f21c9a4074b6f38ff0fe5a
--- /dev/null
+++ b/doc/developer/tutorial/hello/v3-log/hello_world.ml
@@ -0,0 +1,18 @@
+let help_msg = "output a warm welcome message to the user"
+
+module Self = Plugin.Register
+ (struct
+ let name = "hello world"
+ let shortname = "hello"
+ let help = help_msg
+ end)
+
+let run () =
+ Self.result "Hello, world!";
+ let product =
+ Self.feedback ~level:2 "Computing the product of 11 and 5...";
+ 11 * 5
+ in
+ Self.result "11 * 5 = %d" product
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/hello/v4-options/Hello.ml b/doc/developer/tutorial/hello/v4-options/Hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/doc/developer/tutorial/hello/v4-options/dune b/doc/developer/tutorial/hello/v4-options/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7d352870c9efd577409ce95cd429ee8945083900
--- /dev/null
+++ b/doc/developer/tutorial/hello/v4-options/dune
@@ -0,0 +1,12 @@
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/v4-options/dune-project b/doc/developer/tutorial/hello/v4-options/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f1eccde4e9e3b48c5909edf9f8099a850e91f731
--- /dev/null
+++ b/doc/developer/tutorial/hello/v4-options/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/v4-options/hello_world.ml b/doc/developer/tutorial/hello/v4-options/hello_world.ml
new file mode 100644
index 0000000000000000000000000000000000000000..382621862ec580be5c3723396d727593b07e4161
--- /dev/null
+++ b/doc/developer/tutorial/hello/v4-options/hello_world.ml
@@ -0,0 +1,43 @@
+let help_msg = "output a warm welcome message to the user"
+
+module Self = Plugin.Register
+ (struct
+ let name = "hello world"
+ let shortname = "hello"
+ let help = help_msg
+ end)
+
+module Enabled = Self.False
+ (struct
+ let option_name = "-hello"
+ let help = "when on (off by default), " ^ help_msg
+ end)
+
+module Output_file = Self.String
+ (struct
+ let option_name = "-hello-output"
+ let default = "-"
+ let arg_name = "output-file"
+ let help =
+ "file where the message is output (default: output to the console)"
+ end)
+
+let run () =
+ try
+ if Enabled.get() then
+ let filename = Output_file.get () in
+ let output msg =
+ if Output_file.is_default() then
+ Self.result "%s" msg
+ else
+ let chan = open_out filename in
+ Printf.fprintf chan "%s\n" msg;
+ flush chan;
+ close_out chan;
+ in
+ output "Hello, world!"
+ with Sys_error _ as exc ->
+ let msg = Printexc.to_string exc in
+ Printf.eprintf "There was an error: %s\n" msg
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/hello/v5-multiple/Hello.ml b/doc/developer/tutorial/hello/v5-multiple/Hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..531c36043aac3c1c5312dd673e070335286a5008
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/Hello.ml
@@ -0,0 +1,3 @@
+(** Hello World plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/hello/v5-multiple/dune b/doc/developer/tutorial/hello/v5-multiple/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7d352870c9efd577409ce95cd429ee8945083900
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/dune
@@ -0,0 +1,12 @@
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/v5-multiple/dune-project b/doc/developer/tutorial/hello/v5-multiple/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f1eccde4e9e3b48c5909edf9f8099a850e91f731
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/v5-multiple/hello_options.ml b/doc/developer/tutorial/hello/v5-multiple/hello_options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..089ac6f0a1b25201767d66f4038a4e2d28448ef4
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/hello_options.ml
@@ -0,0 +1,23 @@
+let help_msg = "output a warm welcome message to the user"
+
+module Self = Plugin.Register
+ (struct
+ let name = "hello world"
+ let shortname = "hello"
+ let help = help_msg
+ end)
+
+module Enabled = Self.False
+ (struct
+ let option_name = "-hello"
+ let help = "when on (off by default), " ^ help_msg
+ end)
+
+module Output_file = Self.String
+ (struct
+ let option_name = "-hello-output"
+ let default = "-"
+ let arg_name = "output-file"
+ let help =
+ "file where the message is output (default: output to the console)"
+ end)
diff --git a/doc/developer/tutorial/hello/v5-multiple/hello_print.ml b/doc/developer/tutorial/hello/v5-multiple/hello_print.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5e73dabffc08480dff00de5d29081301dc903b9f
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/hello_print.ml
@@ -0,0 +1,13 @@
+let output msg =
+ try
+ let filename = Hello_options.Output_file.get () in
+ if Hello_options.Output_file.is_default () then
+ Hello_options.Self.result "%s" msg
+ else
+ let chan = open_out filename in
+ Printf.fprintf chan "%s\n" msg;
+ flush chan;
+ close_out chan
+ with Sys_error _ as exc ->
+ let msg = Printexc.to_string exc in
+ Printf.eprintf "There was an error: %s\n" msg
diff --git a/doc/developer/tutorial/hello/v5-multiple/hello_run.ml b/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e688748981644b66e97171f44f68a7506821fcd4
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
@@ -0,0 +1,5 @@
+let run () =
+ if Hello_options.Enabled.get() then
+ Hello_print.output "Hello, world!"
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/hello/v5-multiple/tests/hello/hello_test.c b/doc/developer/tutorial/hello/v5-multiple/tests/hello/hello_test.c
new file mode 100644
index 0000000000000000000000000000000000000000..d2f4ef3e1bfd30db301c62a3108511e6f6289e55
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/tests/hello/hello_test.c
@@ -0,0 +1,3 @@
+/* run.config
+ OPT: -hello
+ */
diff --git a/doc/developer/tutorial/hello/v5-multiple/tests/ptests_config b/doc/developer/tutorial/hello/v5-multiple/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..cd6b8a2ceb30bce514102e1619415edd1ae2cf56
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/tests/ptests_config
@@ -0,0 +1,2 @@
+DEFAULT_SUITES= hello
+
diff --git a/doc/developer/tutorial/hello/v5-multiple/tests/test_config b/doc/developer/tutorial/hello/v5-multiple/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2a2d5950338b6ac669e5f0b8cb0203909e1ac612
--- /dev/null
+++ b/doc/developer/tutorial/hello/v5-multiple/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: hello
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/Hello.ml b/doc/developer/tutorial/hello/v6-test-with-bug/Hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..531c36043aac3c1c5312dd673e070335286a5008
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/Hello.ml
@@ -0,0 +1,3 @@
+(** Hello World plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/dune b/doc/developer/tutorial/hello/v6-test-with-bug/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7d352870c9efd577409ce95cd429ee8945083900
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/dune
@@ -0,0 +1,12 @@
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/dune-project b/doc/developer/tutorial/hello/v6-test-with-bug/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f1eccde4e9e3b48c5909edf9f8099a850e91f731
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/hello_options.ml b/doc/developer/tutorial/hello/v6-test-with-bug/hello_options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..089ac6f0a1b25201767d66f4038a4e2d28448ef4
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/hello_options.ml
@@ -0,0 +1,23 @@
+let help_msg = "output a warm welcome message to the user"
+
+module Self = Plugin.Register
+ (struct
+ let name = "hello world"
+ let shortname = "hello"
+ let help = help_msg
+ end)
+
+module Enabled = Self.False
+ (struct
+ let option_name = "-hello"
+ let help = "when on (off by default), " ^ help_msg
+ end)
+
+module Output_file = Self.String
+ (struct
+ let option_name = "-hello-output"
+ let default = "-"
+ let arg_name = "output-file"
+ let help =
+ "file where the message is output (default: output to the console)"
+ end)
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/hello_print.ml b/doc/developer/tutorial/hello/v6-test-with-bug/hello_print.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5e73dabffc08480dff00de5d29081301dc903b9f
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/hello_print.ml
@@ -0,0 +1,13 @@
+let output msg =
+ try
+ let filename = Hello_options.Output_file.get () in
+ if Hello_options.Output_file.is_default () then
+ Hello_options.Self.result "%s" msg
+ else
+ let chan = open_out filename in
+ Printf.fprintf chan "%s\n" msg;
+ flush chan;
+ close_out chan
+ with Sys_error _ as exc ->
+ let msg = Printexc.to_string exc in
+ Printf.eprintf "There was an error: %s\n" msg
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml b/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e01bf492151dd13574dc8b7abde0e992a417769d
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
@@ -0,0 +1,5 @@
+let run () =
+ if Hello_options.Enabled.get() then
+ Hello_print.output "Hello world!" (* removed comma *)
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/tests/hello/hello_test.c b/doc/developer/tutorial/hello/v6-test-with-bug/tests/hello/hello_test.c
new file mode 100644
index 0000000000000000000000000000000000000000..d2f4ef3e1bfd30db301c62a3108511e6f6289e55
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/tests/hello/hello_test.c
@@ -0,0 +1,3 @@
+/* run.config
+ OPT: -hello
+ */
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/tests/hello/oracle/hello_test.res.oracle b/doc/developer/tutorial/hello/v6-test-with-bug/tests/hello/oracle/hello_test.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5f6ab2389a8695bba00d6527d2135e7cc3389c6b
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/tests/hello/oracle/hello_test.res.oracle
@@ -0,0 +1,2 @@
+[kernel] Parsing hello_test.c (with preprocessing)
+[hello] Hello, world!
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/tests/ptests_config b/doc/developer/tutorial/hello/v6-test-with-bug/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..cd6b8a2ceb30bce514102e1619415edd1ae2cf56
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/tests/ptests_config
@@ -0,0 +1,2 @@
+DEFAULT_SUITES= hello
+
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/tests/test_config b/doc/developer/tutorial/hello/v6-test-with-bug/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2a2d5950338b6ac669e5f0b8cb0203909e1ac612
--- /dev/null
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: hello
diff --git a/doc/developer/tutorial/hello/v7-doc/Hello.ml b/doc/developer/tutorial/hello/v7-doc/Hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5a05e083dfff7075a32a799b516cc6e36de6fec0
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/Hello.ml
@@ -0,0 +1,6 @@
+(** Hello World plug-in.
+ All modules are exported to illustrate documentation generation by odoc. *)
+
+module Hello_run = Hello_run
+module Hello_options = Hello_options
+module Hello_print = Hello_print
diff --git a/doc/developer/tutorial/hello/v7-doc/dune b/doc/developer/tutorial/hello/v7-doc/dune
new file mode 100644
index 0000000000000000000000000000000000000000..7d352870c9efd577409ce95cd429ee8945083900
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/dune
@@ -0,0 +1,12 @@
+(library
+ (name Hello)
+ (public_name frama-c-hello.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name hello)
+ (libraries frama-c-hello.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/hello/v7-doc/dune-project b/doc/developer/tutorial/hello/v7-doc/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f1eccde4e9e3b48c5909edf9f8099a850e91f731
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-hello)
+(package (name frama-c-hello))
diff --git a/doc/developer/tutorial/hello/v7-doc/hello_options.ml b/doc/developer/tutorial/hello/v7-doc/hello_options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0a025af51a2ad6cf00d5709ec220f700e05dc0bf
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/hello_options.ml
@@ -0,0 +1,34 @@
+(** This module contains the possible command line options
+ for the Hello plug-in.
+ @author Anne Onymous
+ @see <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+ Frama-C Developer Manual, Tutorial
+*)
+
+(** Content of the welcome message. *)
+let help_msg = "output a warm welcome message to the user"
+
+(** Registration of the plug-in to Frama-C. *)
+module Self = Plugin.Register
+ (struct
+ let name = "hello world"
+ let shortname = "hello"
+ let help = help_msg
+ end)
+
+(** Enabling of the plug-in. *)
+module Enabled = Self.False
+ (struct
+ let option_name = "-hello"
+ let help = "when on (off by default), " ^ help_msg
+ end)
+
+(** Output of the plug-in. *)
+module Output_file = Self.String
+ (struct
+ let option_name = "-hello-output"
+ let default = "-"
+ let arg_name = "output-file"
+ let help =
+ "file where the message is output (default: output to the console)"
+ end)
diff --git a/doc/developer/tutorial/hello/v7-doc/hello_print.ml b/doc/developer/tutorial/hello/v7-doc/hello_print.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d1d2a44ba4c42f9631976c4dc42eb8646240eccd
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/hello_print.ml
@@ -0,0 +1,24 @@
+(** This module contains the printing method of the Hello plug-in.
+ @author Anne Onymous
+ @see <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+ Frama-C Developer Manual, Tutorial
+*)
+
+(** Outputs a message to the output selected in
+ {!module:Hello_options.Output_file}.
+ @param msg Message to output.
+ @raise Sys_error if filesystem error.
+*)
+let output msg =
+ try
+ let filename = Hello_options.Output_file.get () in
+ if Hello_options.Output_file.is_default () then
+ Hello_options.Self.result "%s" msg
+ else
+ let chan = open_out filename in
+ Printf.fprintf chan "%s\n" msg;
+ flush chan;
+ close_out chan
+ with Sys_error _ as exc ->
+ let msg = Printexc.to_string exc in
+ Printf.eprintf "There was an error: %s\n" msg
diff --git a/doc/developer/tutorial/hello/v7-doc/hello_run.ml b/doc/developer/tutorial/hello/v7-doc/hello_run.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e46b2fe6fc2f72585dccc7fbe40618eb4ab1be43
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/hello_run.ml
@@ -0,0 +1,16 @@
+(** This module contains the main control logic of the Hello plug-in.
+ @author Anne Onymous
+ @see <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+ Frama-C Developer Manual, Tutorial
+*)
+
+(** Controls the output of a given message by
+ {!val:Hello_print.output} depending on the state of
+ {!module:Hello_options.Enabled}.
+*)
+let run () =
+ if Hello_options.Enabled.get() then
+ Hello_print.output "Hello, world!"
+
+(** Definition of the entry point of the hello plug-in. *)
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/hello/v7-doc/tests/hello/hello_test.c b/doc/developer/tutorial/hello/v7-doc/tests/hello/hello_test.c
new file mode 100644
index 0000000000000000000000000000000000000000..d2f4ef3e1bfd30db301c62a3108511e6f6289e55
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/tests/hello/hello_test.c
@@ -0,0 +1,3 @@
+/* run.config
+ OPT: -hello
+ */
diff --git a/doc/developer/tutorial/hello/v7-doc/tests/ptests_config b/doc/developer/tutorial/hello/v7-doc/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..cd6b8a2ceb30bce514102e1619415edd1ae2cf56
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/tests/ptests_config
@@ -0,0 +1,2 @@
+DEFAULT_SUITES= hello
+
diff --git a/doc/developer/tutorial/hello/v7-doc/tests/test_config b/doc/developer/tutorial/hello/v7-doc/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2a2d5950338b6ac669e5f0b8cb0203909e1ac612
--- /dev/null
+++ b/doc/developer/tutorial/hello/v7-doc/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: hello
diff --git a/doc/developer/tutorial/viewcfg/v1/ViewCfg.ml b/doc/developer/tutorial/viewcfg/v1/ViewCfg.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9107a4fed9035f4b36a5a9a0d2f794ccb1174b7d
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1/ViewCfg.ml
@@ -0,0 +1,3 @@
+(** ViewCfg plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/viewcfg/v1/dune b/doc/developer/tutorial/viewcfg/v1/dune
new file mode 100644
index 0000000000000000000000000000000000000000..abc1f859c79bb5241afcae4849d3291206272159
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1/dune
@@ -0,0 +1,34 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(library
+ (name ViewCfg)
+ (public_name frama-c-view-cfg.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (name view-cfg)
+ (libraries frama-c-view-cfg.core)
+ (site (frama-c plugins))
+)
diff --git a/doc/developer/tutorial/viewcfg/v1/dune-project b/doc/developer/tutorial/viewcfg/v1/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..4e3c156be6c4fddb8fe6e3028e4d43e5f0be71a9
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1/dune-project
@@ -0,0 +1,27 @@
+(lang dune 3.0)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(using dune_site 0.1)
+
+(name frama-c-view-cfg)
+(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v1/test.c b/doc/developer/tutorial/viewcfg/v1/test.c
new file mode 100644
index 0000000000000000000000000000000000000000..727f15d69fd2b65025c6f4f2a2127f690c8ea93a
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1/test.c
@@ -0,0 +1,22 @@
+void f(int g)
+{
+ g++;
+ g--;
+
+}
+
+int main(int argc, char **argv)
+{
+ int i = 3;
+
+ if( i > 0)
+ {
+ while(--i);
+ }
+ else
+ {
+ f(3);
+ }
+
+ return 0;
+}
diff --git a/doc/developer/tutorial/viewcfg/v1/view_cfg.ml b/doc/developer/tutorial/viewcfg/v1/view_cfg.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a208d9f1bbb1d892386382af5174415bc9a913cb
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1/view_cfg.ml
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(*
+ This file is used by the ViewCfg tutorial.
+ NOTE: any modifications changing line numbers will impact the
+ generated PDF for the development guide!
+*)
+
+open Cil_types
+
+let print_stmt out = function
+ | Instr i -> Printer.pp_instr out i
+ | Return _ -> Format.pp_print_string out "<return>"
+ | Goto _ -> Format.pp_print_string out "<goto>"
+ | Break _ -> Format.pp_print_string out "<break>"
+ | Continue _ -> Format.pp_print_string out "<continue>"
+ | If (e,_,_,_) -> Format.fprintf out "if %a" Printer.pp_exp e
+ | Switch(e,_,_,_) -> Format.fprintf out "switch %a" Printer.pp_exp e
+ | Loop _ -> Format.fprintf out "<loop>"
+ | Block _ -> Format.fprintf out "<block>"
+ | UnspecifiedSequence _ -> Format.fprintf out "<unspecified sequence>"
+ | TryFinally _ | TryExcept _ | TryCatch _ -> Format.fprintf out "<try>"
+ | Throw _ -> Format.fprintf out "<throw>"
+
+class print_cfg out = object
+ inherit Visitor.frama_c_inplace
+
+ method! vfile _ =
+ Format.fprintf out "digraph cfg {\n";
+ Cil.DoChildrenPost (fun f -> Format.fprintf out "}\n%!"; f)
+
+ method! vglob_aux g =
+ match g with
+ | GFun(f,_) ->
+ Format.fprintf out " subgraph cluster_%a {\n" Printer.pp_varinfo f.svar;
+ Format.fprintf out " graph [label=\"%a\"];\n" Printer.pp_varinfo f.svar;
+ Cil.DoChildrenPost (fun g -> Format.fprintf out " }\n"; g)
+ | _ -> Cil.SkipChildren
+
+ method! vstmt_aux s =
+ Format.fprintf out " s%d [label=%S];\n"
+ s.sid (Pretty_utils.to_string print_stmt s.skind);
+ List.iter (fun succ -> Format.fprintf out " s%d -> s%d;\n" s.sid succ.sid)
+ s.succs;
+ Cil.DoChildren
+
+end
+
+let run () =
+ let chan = open_out "cfg.out" in
+ let fmt = Format.formatter_of_out_channel chan in
+ Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
+ close_out chan
+
+let () = Db.Main.extend run
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index e2d476f9ae44f43b4c17f7d5099d33bb1fd0be9e..ef5703754dffb3181f8bcbe544a8f444c9094124 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -362,12 +362,39 @@ literate=%
{'c}{$\gamma$ }1%
{µ}{`{}}1%
{€}{\textbackslash}1%
+{Ã }{{\`a}}1%
+{é}{{\'e}}1%
+}
+\lstdefinestyle{ocaml-basic}{
+ language=Ocaml,
+ basicstyle=\lp@basic
+}
+
+\lstdefinelanguage{Dune}{%
+literate=%
+{Ã }{{\`a}}1%
+{é}{{\'e}}1%
+,
+ style=framac-code-style,%
+ morekeywords={
+ dune, flags, generate_opam_files, lang, libraries, name, optional, package,
+ plugin, public_name, site, using
+ },%
+ morekeywords=[2]{
+ :standard
+ },
+ morecomment=[l]{;},
+}
+\lstdefinestyle{dune-basic}{%
+ language=Dune,%
+ style=framac-code-style,%
+ basicstyle=\lp@inline,%
}
-\lstdefinestyle{ocaml-basic}%
-{language=Ocaml,basicstyle=\lp@basic}
\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
+\newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}}
+\lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{}
% --------------------------------------------------------------------------
\lstdefinelanguage{Why}{%
morekeywords={