Merge branch 'stable/iron'

.git-blame-ignore-revs

@@ -5,6 +5,7 @@
 1cec870fb83b726a1362a41ef8ebfa71423fc7d8
 2467fec178efe269231972f68e7f2c08fdec122c
 2f10c9d25fc4ca48edce8248a799d1e6164e8a69
+2f69c7d664a5f2069fbb56e392d5a6d4378b75af
 3b6d99bd1c08434fed8f4bb3d6d66a051785980d
 41c3d54cdbb85152a8192c396c7506cd078e3f2f
 4691c9c7b01d6985a36d23166145c137935f28b8

doc/developer/Makefile

@@ -27,7 +27,6 @@ SRC	= developer \
 	tutorial \
 	architecture \
 	advance \
-	refman \
 	changes
 SRC	:= $(addsuffix .tex, $(SRC))
 SRC	+= macros.sty

doc/developer/changes.tex

@@ -12,6 +12,9 @@ This chapter summarizes the major changes in this documentation between each
 
 \section*{26.0 Iron}
 \begin{itemize}
+\item \textbf{Makefiles/Dune}: Document the use of \texttt{dune} for compiling
+and testing plug-in, and describe transition from a \texttt{Makefile}-based to
+a \texttt{dune}-based setup.
 \item \textbf{Journalisation}: Journalisation has been removed.
 \end{itemize}
 

doc/developer/introduction.tex

-%; whizzy-master "developpeur.tex"
+% Local Variables:
+% TeX-master: "developer.tex"
+% End:
 
 \chapter{Introduction}
 
 \framac (Framework for Modular Analyses of \C) is a software platform which
-helps the development of static analysis tools for \C programs thanks to a
-plug-ins mechanism. 
+helps the development of static and dynamic analysis tools for \C programs
+thanks to a plug-in mechanism.
 
 This guide aims at helping developers program within the \framac platform,
 in particular for developing a new analysis or a new source-to-source
 transformation through a new plug-in. For this purpose, it provides a
 step-by-step tutorial, a general presentation of the \framac software
-architecture, a set of \framac-specific programming rules and an overview of the
+architecture and an overview of the
 API of the \framac kernel. However it does not provide a complete documentation
 of the \framac API and, in particular, it does not describe the API of 
-existing \framac plug-ins. This API is documented in the \html source code
-generated by \texttt{make doc} (see
-Section~\ref{doc:rules} for additional details about this
-documentation). 
+existing \framac plug-ins.
+%This API is documented in the \html source code
+%generated by \texttt{make doc} (see
+%Section~\ref{tut2:doc} for additional details about this
+%documentation).
 
-This guide introduces neither the use of \framac which is the purpose of the
+This guide introduces neither the use of \framac, which is the purpose of the
 user manual~\cite{userman} and of the reference articles~\cite{sefm12,fac15},
 nor the use of plug-ins which are documented in separated and dedicated
 manuals~\cite{slicing,wp,value,rte,aorai}.  We assume that the reader of this
 guide already read the \framac user manual and knows the main \framac concepts.
 
 The reader of this guide may be either a \framac beginner who just finished 
-reading the user manual and wishes to develop his/her own analysis with the help
+reading the user manual and wishes to develop their own analysis with the help
 of \framac, an intermediate-level plug-in developer who would like to have 
 a better understanding of one particular aspect of the framework, 
 or a \framac expert who wants to remember details about one specific point 
@@ -52,11 +55,6 @@ corresponding entries while other numbers (e.g. \textcolor{red}{1}) are
 less important references. 
 Furthermore, the name of each \caml value
 in the index corresponds to an actual \framac value.
-In the \framac source code, the
-\ocamldoc documentation of such a value contains the special tag
-\texttt{@plugin development guide} while, in the \html documentation of the
-\framac API, the note ``\textbf{Consult the Plugin Development Guide} for
-additional details'' is attached the value name.
 
 
 \begin{important}
@@ -72,7 +70,7 @@ additional details'' is attached the value name.
 
 \section{Outline}
 
-This guide is organised in four parts.
+This guide is organised in three parts.
 
 \begin{description}
 \item[Chapter~\ref{chap:tutorial}] is a step-by-step tutorial for developing a
@@ -83,12 +81,4 @@ This guide is organised in four parts.
   architecture. 
 \item[Chapter~\ref{chap:advance}] details how to use all the services provided
   by \framac in order to develop a fully integrated plug-in. 
-\item[Chapter~\ref{chap:refman}] is a reference manual with complete
-  documentation for some particular points of the \framac platform.
 \end{description}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Local Variables:
-%%% TeX-master: "main"
-%%% ispell-local-dictionary: "english"
-%%% End:

doc/developer/macros.sty

@@ -43,7 +43,7 @@
 \newcommand{\C}{\langage{C}}
 \newcommand{\caml}{\langage{OCaml}}
 \newcommand{\ocaml}{\langage{OCaml}}
-\newcommand{\lablgtk}{\langage{Lablgtk2}}
+\newcommand{\lablgtk}{\langage{Lablgtk3}}
 \newcommand{\gnomecanvas}{\langage{GnomeCanvas}}
 \newcommand{\lablgtksourceview}{\langage{Lablgtksourceview2}}
 \newcommand{\dottool}{\langage{DOT}}

doc/developer/tutorial.tex

@@ -28,7 +28,7 @@ The last is probably the easiest to setup for a beginner in OCaml.
 
 Most modern IDEs support (directly or indirectly, via Merlin)
 OCaml-LSP\footnote{\url{https://github.com/ocaml/ocaml-lsp}},
-which is an implementation of LSP ({\em Language Server Protocol} for OCaml.
+which is an implementation of LSP ({\em Language Server Protocol}) for OCaml.
 
 Concerning code formatting, the \framac team currently uses the
 \texttt{ocp-indent} opam package for code indentation.
@@ -150,7 +150,7 @@ platform. This tutorial focuses on specific parts of this figure.
 \end{center}
 \scodeidx{Db}{Main}\codeidx{Dynamic}\codeidx{Plugin}
 \codeidx{Project}\codeidx{Type}
-\codeidx{Makefile.dynamic}\codeidx{Design}
+\codeidx{Design}
 \index{GUI}\index{Plug-in!GUI}
 \caption{Plug-in Integration Overview.}\label{fig:overview}
 \end{figure}
@@ -186,7 +186,7 @@ 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
+  \item a \texttt{<my\_plugin>.ml} file that defines the API of the plugin
     (which can be empty).
 \end{itemize}
 
@@ -195,10 +195,15 @@ For example, for the Hello plugin:
 \listingname{./dune-project}
 \duneinput{./tutorial/hello/v1-simple/dune-project}
 
+The \texttt{dune\_site} feature\footnote{\url{https://dune.readthedocs.io/en/stable/sites.html}}
+ mentioned in this file allows us to rely on
+\texttt{dune} to install the plug-in in a place where \framac will find it
+and load it at runtime.
+
 \listingname{./dune}
 \duneinput{./tutorial/hello/v1-simple/dune}
 
-\texttt{Hello.ml} is just an empty file.
+\texttt{hello.ml} is just an empty file.
 
 Then the plugin can be built using the following command:
 
@@ -219,16 +224,15 @@ Note that this behavior can be configured with Dune's option \verb|--display|.
 \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 library is \texttt{my\_plugin};
   \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 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}
@@ -354,7 +358,7 @@ Section~\ref{adv:log}.
 
 We now extend the \texttt{hello world} plug-in with new options.
 
-If the plug-in is installed (globally, with \verb|make install|, or locally,
+If the plug-in is installed (globally, with \verb|dune 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
@@ -402,26 +406,20 @@ These new options also appear in the inline help for the hello plug-in:
 \subsection{About the plug-in build process}
 
 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.
+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:
 
-\listingname{./Hello.ml}
-\ocamlinput{./tutorial/hello/v5-multiple/Hello.ml}
-
-\begin{important}
-  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}
+\listingname{./hello.ml}
+\ocamlinput{./tutorial/hello/v5-multiple/hello.ml}
 
 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
+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}).
 
-The module name chosen by a plug-in (here \texttt{Hello}) is used by Dune to
+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
@@ -432,7 +430,7 @@ packed module. It can be installed along with the other \framac plug-ins using
 \verb|dune install|.
 
 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
+\texttt{hello} plug-in will be automatically loaded. Check it with the command
 \verb|frama-c -hello-help|.
 
 You can uninstall it by running \verb|dune uninstall|.
@@ -533,7 +531,7 @@ Each test file should contain a
 \texttt{run.config}\index{Test!Configuration}\index{Test!Header}
 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}).
+control tests, as detailed in Section~\ref{ptests:structure}).
 
 For this tutorial, no actual C code is needed, so
 \texttt{./tests/hello/hello\_test.c} will only contain the run.config header:
@@ -696,7 +694,7 @@ 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}.
+Sections~\ref{adv:ptests}.
 
 \subsubsection{Summary of Testing Operations}
 
@@ -735,11 +733,11 @@ This relies on \odoc and requires the plug-in to be documented following the
 
 We show here how the Hello plug-in could be slightly documented and use
 \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
+\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}
+\listingname{./hello.ml}
+\ocamlinput{./tutorial/hello/v7-doc/hello.ml}
 
 Then, we add some documentation tags to our modules:
 

doc/developer/tutorial/hello/src/Makefile

+FRAMAC_SHARE:=$(shell frama-c-config -print-share-path)
+
+## Common definitions
+
+include ${FRAMAC_SHARE}/Makefile.common
+
+## Tests-related targets
+
+include ${FRAMAC_SHARE}/Makefile.testing
+
+## Installation-related targets
+
+include ${FRAMAC_SHARE}/Makefile.installation

doc/developer/tutorial/hello/src/Makefile.multiple-files

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-PLUGIN_NAME = Hello
-PLUGIN_CMO = hello_options hello_print hello_run
-include $(FRAMAC_SHARE)/Makefile.dynamic

doc/developer/tutorial/hello/src/Makefile.single-file

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-PLUGIN_NAME = Hello
-PLUGIN_CMO = hello_world
-include $(FRAMAC_SHARE)/Makefile.dynamic

doc/developer/tutorial/hello/src/Makefile.test

-##########################################################################
-#                                                                        #
-#  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).            #
-#                                                                        #
-##########################################################################
-
-FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-PLUGIN_NAME = Hello
-PLUGIN_CMO = hello_options hello_print hello_run
-PLUGIN_TESTS_DIRS := hello
-include $(FRAMAC_SHARE)/Makefile.dynamic