diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
index b6ef39a67856b8c00985e4a92dc62e4be686179c..57e8b4fe14a4610a0aa5d3f5ad4cee326b078220 100644
--- a/.git-blame-ignore-revs
+++ b/.git-blame-ignore-revs
@@ -5,6 +5,7 @@
1cec870fb83b726a1362a41ef8ebfa71423fc7d8
2467fec178efe269231972f68e7f2c08fdec122c
2f10c9d25fc4ca48edce8248a799d1e6164e8a69
+2f69c7d664a5f2069fbb56e392d5a6d4378b75af
3b6d99bd1c08434fed8f4bb3d6d66a051785980d
41c3d54cdbb85152a8192c396c7506cd078e3f2f
4691c9c7b01d6985a36d23166145c137935f28b8
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index 8718ee6e1cca36aba202a62c04e5927f5f810949..1b44d2ffa99a4c611c06d87038d5c555c8830d14 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -27,7 +27,6 @@ SRC = developer \
tutorial \
architecture \
advance \
- refman \
changes
SRC := $(addsuffix .tex, $(SRC))
SRC += macros.sty
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 6298b441abc8e3e4ca474f920061e1dd37532a6e..0f86ab39287fc15563f775da65f670496114a7de 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -36,9 +36,7 @@ Plug-in development also requires some familiarity with the Dune build system.
Note that the following subsections can be read in no particular
order: their contents are indeed quite independent from one another even if
-there are references from one chapter to another one. Pointers to
-reference manuals (Chapter~\ref{chap:refman}) are also provided for readers who
-want full details about specific parts.
+there are references from one section to another one.
\section{Plug-in dependencies}\label{adv:dependencies}
@@ -159,7 +157,7 @@ libraries:
(libraries frama-c.kernel frama-c-wp.core camlp-streams zarith)
\end{lstlisting}
-Its plug-in library name is \verb|frama-c-clang.core|. Its availability
+Its plug-in library name is \verb|frama-clang.core|. Its availability
must be displayed as the ``summary'' of the configuration, written as the first
line, with each dependency as a subitem:
@@ -168,7 +166,7 @@ line, with each dependency as a subitem:
(alias frama-c-configure)
(deps (universe))
(action (progn
- (echo "Clang:" %{lib-available:frama-c-clang.core} "\n")
+ (echo "Clang:" %{lib-available:frama-clang.core} "\n")
(echo " - zarith:" %{lib-available:zarith} "\n")
(echo " - camlp5:" %{lib-available:camlp5} "\n") ; for gen_ast
(echo " - camlp-streams:" %{lib-available:camlp-streams} "\n")
@@ -194,16 +192,34 @@ Note that \verb|camlp5| is not among the dependencies declared in
Since the adoption of Dune, \framac's \texttt{Makefile}s were largely
simplified. They are still used for some tasks, partially due to conciseness
(\verb|make| is shorter than \verb|dune build|), partially because some tasks
-are better suited for them.
+are better suited for them. Some standard targets are defined in various
+Makefiles that are installed in \framac's shared directory.
-Plug-in developers usually just need to copy and paste the existing Makefile
-template and rename the opam file name (\verb|frama-c-<plugin>.opam|).
+A minimal plugin's \verb|Makefile| can thus be the following:
+
+\listingname{Makefile}
+\makeinput{./tutorial/hello/src/Makefile}
+
+\texttt{Makefile.testing} introduces various targets related to \framac's
+testing infrastructure (see Section~\ref{adv:ptests}). This includes notably
+\texttt{tests} to run all the tests of the plugin, after having taken care of
+generating the corresponding \texttt{dune} files.
+
+\texttt{Makefile.installation} provides two targets, \texttt{install} and
+\texttt{uninstall}. By default, installation will occur in the current
+\texttt{opam} switch, but this can be modified by using the \texttt{PREFIX}
+variable (note that if you install your plugin in a non-default place, you will
+have to explicitly instruct \framac to load it through option
+\texttt{-load-plugin}.
+
+Other Makefiles include \texttt{Makefile.documentation}, providing the
+\texttt{doc} for generating the documentation (see Section~\ref{tut2:doc}),
+and \texttt{Makefile.linting} which is used
+by \framac itself to perform various syntactic checks through target
+\texttt{check-lint} and fix indentation issues through \texttt{lint}. If
+you want to use the same conventions as \framac itself, you'll need to
+have \texttt{ocp-indent} installed to launch these targets.
-This Makefile reuses code from other Makefiles, distributed in Frama-C's
-{\em share} directory, such as \verb|Makefile.testing|,
-\verb|Makefile.installation|, etc. Their names indicate the kinds of features
-they provide. Many are shortcuts for specific dune targets, but they also
-provide linting and copyright headers-related features.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -526,13 +542,11 @@ the test file name, plus a few other implicit options (\verb|-check|,
\verb|-no-autoload-plugins|, \verb|-load-module|, etc).
\end{example}
-Figure~\ref{fig:test-directives} shows all the directives that can be used in
+Table~\ref{fig:test-directives} shows all the directives that can be used in
the configuration header of a test (or a test suite). Those whose name are
underlined are the directives that {\em actually} create test cases; the others
modify or disable test cases.
-\begin{figure}[ht]
-\begin{center}
-\begin{tabular}{|l|p{9cm}|p{4cm}|}
+\begin{longtable}{|l|p{9cm}|p{4cm}|}
\hline
\textbf{Name} & \textbf{Specification} & \textbf{default}\\
\hline
@@ -630,12 +644,10 @@ and report a failure.
& \textit{None}
\\
\hline
-\end{tabular}
-\end{center}
\caption{Directives in configuration headers of test files.
Underlined directives are the only ones which actually generate test cases.
}\label{fig:test-directives}
-\end{figure}
+\end{longtable}
In the following, we detail some aspects of several directives.
@@ -665,7 +677,7 @@ In the following, we detail some aspects of several directives.
Note that \texttt{EXECNOW} directives can also be prefixed with
\texttt{LOG}s, but they are written in the same line, without the
separating colon (\texttt{:}).
-\item By default, the test command (usually, \texttt|frama-c|) is expected
+\item By default, the test command (usually, \texttt{frama-c}) is expected
to return successfully (i.e., with an exit status of 0).
If a test is supposed to lead to an error, an \texttt{EXIT} directive must be
used. It takes as argument an integer
@@ -804,6 +816,41 @@ itself, it needs to be doubled, {\it i.e.} \texttt{@@} will be translated as
produced file as a dependency.
\end{important}
+\subsection{Pre-defined macros for tests commands}\label{sec:ptests-macros}
+Table~\ref{tab:ptests-macros} gives the definition of the most important
+predefined macros that can be used in \ptests' directives.
+Refer to \texttt{frama-c-ptests --help} to have the full list.
+\begin{longtable}{|p{4.5cm}|p{10cm}|}
+\hline
+Name & Expansion \\
+\hline
+\verb|frama-c| & path to \framac executable \\
+\hline
+\verb|PTEST_CONFIG| & either the empty string or \verb|_| followed by the
+name of the current alternative configuration
+(see section~\ref{ptests:structure}). \\
+\hline
+\verb|PTEST_DIR| & current test suite directory \\
+\hline
+\verb|PTEST_FILE| & path to the current test file \\
+\hline
+\verb|PTEST_NAME| & basename of the current test file (without suffix) \\
+\hline
+\verb|PTEST_NUMBER| & rank of current test in the test file. There are in
+fact two independent numbering schemes: one for \verb|EXECNOW| commands and
+one for regular tests (if more than one \verb|OPT|).\\
+\hline
+\verb|PTEST_RESULT| & shorthand alias to \verb|@PTEST_DIR@/result@PTEST_CONFIG@|
+(the result directory dedicated to the tested configuration)\\
+\hline
+\verb|PTEST_ORACLE| & basename of the current oracle file (macro only usable in FILTER directives)\\
+\hline
+\verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-check| \verb|-no-autoload-plugins|\\
+\hline
+\caption{Predefined macros for ptests}\label{tab:ptests-macros}
+\end{longtable}
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Plug-in Migration from Makefile to Dune}\label{adv:dune-migration}
@@ -822,16 +869,28 @@ please contact us if you need some help for migrating it.
\subsection{Files organization changes}
+\begin{important}
+Due to the way \texttt{dune} operates, it is preferable to work on the migration
+starting from a ``clean'' directory, without compilation and tests
+(in \texttt{result} directory of the test suites) artifacts. Otherwise,
+\texttt{dune} will complain about conflicts between files being both present
+in the original source directory and the target of a compilation rule.
+\end{important}
+
Previously for a plug-in named \texttt{Plugin}, only the file
\texttt{Plugin.mli} was necessary to expose the signature of the plug-in. Now,
one has to also provide an implementation file \texttt{Plugin.ml}.
+On the other hand, it is not necessary that it begins with a capital letter
+anymore: you can have \texttt{plugin.ml} and \texttt{plugin.mli}. If these files
+are not present, all functions included in the modules constituting the
+plug-in will be exported.
For most plug-ins, the \texttt{autoconf} and \texttt{configure} will be useless.
In particular, \framac does not provide any \texttt{autoconf} and
\texttt{configure} features anymore. So for most plug-ins these files will be
entirely removed (see~\ref{adv:dune-migration:conf}). Thus, the
\texttt{Makefile.in} does not exist anymore. A \texttt{Makefile} may be useful
-to provide some shortcuts.
+to provide some shortcuts (see Section~\ref{adv:make}).
If a plugin has a graphical user-interface, it is recommended to put the related
files into a separate directory in the directory of the plug-in
@@ -912,7 +971,7 @@ The \texttt{libraries} should be now:
)
)
\end{lstlisting}
-For external binaries, the keywod is \texttt{bin-available}.
+For external binaries, the keyword is \texttt{bin-available}.
In the case some file must be generated at build time, it is recommended to use
a rule together with an action of generation. The executable itself can be
@@ -936,7 +995,7 @@ is now a \texttt{dune} file for the GUI, that depends on the core features of
the plug-in and the \framac GUI. This file is to put in the \texttt{gui}
subdirectory. Again, if there are additional dependencies, they must be
indicated in the \texttt{libraries} field:
-\begin{lstlisting}
+\begin{dunecode}
( library
(name myplugin_gui)
(public_name frama-c-myplugin.gui)
@@ -945,15 +1004,40 @@ indicated in the \texttt{libraries} field:
(libraries frama-c.kernel frama-c.gui frama-c-myplugin.core)
)
-(plugin (optional) (name myplugin-gui) (libraries frama-c-myplugin.gui) (site (frama-c plugins_gui)))
-\end{lstlisting}
+(plugin (optional)
+ (name myplugin-gui)
+ (libraries frama-c-myplugin.gui)
+ (site (frama-c plugins_gui)))
+\end{dunecode}
\subsection{Build and \texttt{Makefile.in}}
-
+\lstset{language=shell}
Provided that the \lstinline{dune} files are ready. The plug-in can now be
built using the command \texttt{dune build @install}. The file
\lstinline{Makefile.in} can now be removed.
+\subsection{Installing Additional Files}
+
+If your plug-in has additional files to install besides the compiled files,
+themselves (typically, files in \texttt{share}), you can use an
+\texttt{install} stanza in the \texttt{dune} file, as in:
+
+\begin{dunecode}
+(install
+ (package frama-c-myplugin)
+ (section (site (frama-c share)))
+ (files (share/myfile as frama-c-myplugin/myfile)))
+\end{dunecode}
+
+With the stanza above, the installation of package \texttt{frama-c-myplugin}
+will copy \texttt{myfile} from the \texttt{share} directory
+of the plug-in sources into the \texttt{frama-c-myplugin} directory inside
+the \texttt{share} directory of \framac's installation. Other target sections
+are available (e.g. \texttt{bin} for installing an additional executable), see
+the \texttt{dune}
+manual\footnote{\url{https://dune.readthedocs.io/en/stable/dune-files.html\#install-1}}
+for more information.
+
\subsection{Migrating tests}
In the \texttt{test\_config*} files, the \texttt{PLUGIN} field is now mandatory
@@ -977,7 +1061,7 @@ DEFAULT_SUITES=basic eva wp
\end{lstlisting}
For most plug-ins, these modifications should be enough so that:
-\begin{lstlisting}
+\begin{lstlisting}[language=shell]
dune exec -- frama-c-ptests
dune build @ptests
\end{lstlisting}
@@ -1296,6 +1380,7 @@ be changed by using the
\paragraph{Source Options.} By default, a message is not localized. You may
specify a source location, either specifically or by using the current
location of an \texttt{AST} visitor.
+\lstset{style=frama-c-style}
\begin{itemize}
\item[] \lstinline{~source:$s$} use the source location $s$ (see \texttt{Log.mli})
\item[] \lstinline{~current:true} use the current source location
@@ -1797,7 +1882,7 @@ types like list and function (respectively
\section{Plug-in Registration and Access}\label{adv:plugin-registration}
In this section, we present how to register plug-ins and how to access them.
-Actually there are three different ways, but the recommended one is through a
+Actually, there are three different ways, but the recommended one is through a
\texttt{.mli} file.
Section~\ref{adv:standard-registration} indicates how to register and access a
@@ -1811,70 +1896,18 @@ Section~\ref{adv:dynamic-registration} details how to register and access a
\begin{target}plug-in developers.\end{target}
\begin{prereq}
- Basic knowledge of \make.
+ Basic knowledge of \texttt{dune}.
\end{prereq}
-Each plug-in is compiled into a module of name indicated by the variable
-\texttt{PLUGIN\_NAME}\codeidx{PLUGIN\_NAME} of its \texttt{Makefile} (say
-\texttt{Plugin\_A}. Its developer has to provide a \texttt{.mli} for this
-plug-in (following the previous example, a file \texttt{Plugin\_A.mli}). This
-\texttt{.mli} file may thus contains the API of the plug-in.
-
-Another plug-in may then access to \texttt{Plugin\_A} as it accesses any
-other \caml module, but it has to declare in its \texttt{Makefile} that it
-depends on \texttt{Plugin\_A} through the special variable
-\texttt{PLUGIN\_DEPENDENCIES}.
-
-\begin{example}
-\texttt{Plugin\_A} declares and provides access to a function \texttt{compute}
-in the following way.
-
-\listingname{File plugin\_a/my\_analysis\_a.ml}
-\begin{ocamlcode}
-let compute () = ...
-\end{ocamlcode}
-
-\listingname{File plugin\_a/Plugin\_A.mli}
-\begin{ocamlcode}
-module My_analysis_a: sig val compute: unit -> unit
-\end{ocamlcode}
-
-\codeidx{PLUGIN\_NAME}
-\codeidx{PLUGIN\_CMO}
-\codeidx{Makefile.dynamic}
-\listingname{File plugin\_a/Makefile}
-\begin{makefilecode}
-PLUGIN_NAME:=Plugin_A
-PLUGIN_CMO:=... my_analysis_a ...
-...
-include Makefile.dynamic
-\end{makefilecode}
-
-Then, \texttt{Plugin\_B} may use this function \texttt{Compute} as follows.
-
-\listingname{File plugin\_b/my\_analysis\_b.ml}
-\begin{ocamlcode}
-let compute () = ... Plugin_A.My_analysis_a.compute () ...
-\end{ocamlcode}
-
-\codeidx{PLUGIN\_NAME}
-\codeidx{PLUGIN\_CMO}
-\codeidx{PLUGIN\_DEPENDENCIES}
-\codeidx{Makefile.dynamic}
-\listingname{File plugin\_b/Makefile}
-\begin{makefilecode}
-PLUGIN_NAME:=Plugin_B
-PLUGIN_CMO:=... my_analysis_b ...
-PLUGIN_DEPENDENCIES:=Plugin_A
-...
-include Makefile.dynamic
-\end{makefilecode}
-\end{example}
+From \texttt{dune} point of view, a plug-in is simply an \ocaml library.
+In order for plugin \texttt{B} to use a function which is declared in
+the interface of plugin \texttt{A}, the \texttt{dune} file of \texttt{B} must
+contain in its \texttt{libraries} clause \texttt{frama-c-a.core}
+(see Section~\ref{adv:dependencies}), or more generally the \texttt{public\_name}
+under which \texttt{A} is declared.
\subsection{Kernel-integrated Registration and Access}
\label{adv:static-registration}
-\index{Plug-in!Kernel-integrated!Registration}
-\index{Plug-in!Kernel-integrated!Access}
\begin{target}kernel-integrated plug-in developers.\end{target}
@@ -1884,6 +1917,12 @@ include Makefile.dynamic
Section~\ref{adv:dynamic-registration} for details).
\end{prereq}
+\begin{important}
+This registration method is deprecated and only kept here for historical purpose.
+No new entry point should be added in the \texttt{Db}, which will be removed in
+a future version of \framac.
+\end{important}
+
A database, called \texttt{Db}\codeidxdef{Db} (in directory
\texttt{src/kernel\_services/plugin\_entry\_points}), groups together
the API of all kernel-integrated
@@ -1928,9 +1967,6 @@ directory. The best way is to create a directory dedicated to types.
plug-in $p$.
\end{convention}
-If you add such a directory, you also have to modify \texttt{Makefile} by
-extending variable \texttt{FRAMAC\_SRC\_DIRS}\codeidx{FRAMAC\_SRC\_DIRS} (see
-Section~\ref{make:plugin}).
\begin{example}
Suppose you are writing a plug-in \texttt{p} which exports a specific type
\texttt{t} corresponding to the result of the plug-in analysis. The standard way
@@ -1949,12 +1985,6 @@ module P : sig
@return result of the analysis. *)
end
\end{ocamlcode}
-
-\listingname{share/Makefile.common}
-\begin{makefilecode}
-FRAMAC_SRC_DIRS= ... plugins/p_types
- # Extend this variable with the new directory
-\end{makefilecode}
\end{example}
This design choice has a side effect : it reveals exported types.
@@ -1966,17 +1996,17 @@ implementation. This code should be linked before \texttt{Db}
\codeidx{Db}\footnote{A direct consequence is that you cannot use the whole
\framac functionalities, such as module \texttt{Db}, inside this code.}.
-To this effect, the files containing the external plug-in code must be added to
-the \texttt{Makefile} variable
-\texttt{PLUGIN\_TYPES\_CMO}\codeidxdef{PLUGIN\_TYPES\_CMO} (see
-Section~\ref{make:plugin}).
-
\subsection{Dynamic Registration and Access}
\label{adv:dynamic-registration}
\index{Plug-in!Registration}\index{Plug-in!Access}\index{Plug-in!API}
\begin{target}standard plug-ins developers.\end{target}
+\begin{important}
+Dynamic registration is obsolete. Newer development should favor exporting
+a static API, as explained in Section~\ref{adv:standard-registration}.
+\end{important}
+
Registration of kernel-integrated plug-ins requires to modify module
\texttt{Db}\codeidx{Db} which belongs to the \framac kernel. Such a
modification is not possible for standard plug-ins which are fully independent
@@ -2299,7 +2329,7 @@ module State =
(struct
let size = 97
let name = "state"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
end)
let compute_info (kf,vi) = ...
let memoize = State.memo compute_info
@@ -2391,7 +2421,7 @@ module Tbl =
(struct
let name = "functionwise_from"
let size = 97
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
end)
let () =
(* performed at module initialization runtime. *)
@@ -2682,7 +2712,7 @@ consistently handle state dependencies\index{State!Dependency}.
\scodeidx{State\_selection}{with\_dependencies}
\sscodeidx{Db}{Value}{self}
\begin{ocamlcode}
-let selection = State_selection.with_dependencies Db.Value.self in
+let selection = State_selection.with_dependencies Eva.Analysis.self in
Project.clear ~selection ()
\end{ocamlcode}
The selection explicitly indicates that we also want to clear all the states
@@ -4045,13 +4075,7 @@ accesses to the main widgets of the \framac GUI and to several plug-in extension
points. The documentation of the class type
\texttt{Design.main\_window\_extension\_points}%
\scodeidxdef{Design}{main\_window\_extension\_points} is accessible through the
-source documentation (see Section~\ref{adv:documentation}).
-
-The GUI plug-in code has to be put in separate files into the plug-in
-directory\index{Plug-in!Directory}. Furthermore, in the
-\texttt{Makefile}\codeidx{Makefile}, the variable
-\texttt{PLUGIN\_GUI\_CMO}\codeidx{PLUGIN\_GUI\_CMO} has to be set in order to
-compile the GUI plug-in code (see Section~\ref{make:plugin}).
+source documentation (see Section~\ref{tut2:doc}).
Besides time-consuming computations have to call the function
\texttt{!Db.progress}\scodeidx{Db}{progress} from time to time in order to keep the GUI reactive.
@@ -4061,7 +4085,7 @@ The GUI implementation uses
\lablgtk~\cite{lablgtk}\index{Lablgtk}: you can use any \lablgtk-compatible
code in your gui extension. A complete example of a GUI extension may be found in
the plug-in \texttt{Occurrence}\index{Occurrence} (see file
-\texttt{src/plugins/occurrence/register\_gui.ml}).
+\texttt{src/plugins/occurrence/gui/register\_gui.ml}).
\begin{important}
\paragraph{Potential issues}
@@ -4075,87 +4099,141 @@ but it could be quite difficult to understand for an user.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Documentation}\label{adv:documentation}
-\index{Documentation|bfit}
-
-\begin{prereq}
- Knowledge of \ocamldoc.
-\end{prereq}
-
-Here we present some hints on the way to document your plug-in. First
-Section~\ref{doc:rules} introduces a quick general overview about the
-documentation process. Next Section~\ref{doc:plugin} focuses on the
-plug-in source documentation.
-
-\subsection{General Overview}\label{doc:rules}
-
-Command \texttt{make doc}\codeidx{Makefile} produces the whole \framac source
-documentation\index{Documentation!Source} in HTML format. The generated index
-file is \texttt{doc/code/html/index.html}. A more general purpose index is
-\texttt{doc/index.html}\codeidx{index.html} (from which the previous index is
-accessible).
-
-The previous command takes times. So command \texttt{make doc-kernel} only
-generates the kernel documentation\index{Documentation!Kernel} (\emph{i.e.}
-\framac without any plug-in) while \texttt{make \$(PLUGIN\_NAME)\_DOC} (by
-substituting the right value for
-\texttt{\$(PLUGIN\_NAME)})\codeidx{PLUGIN\_NAME} generates
-the documentation for a single plug-in\index{Plug-in!Documentation}%
-\index{Documentation!Plug-in|see{Plug-in Documentation}}.
-
-\subsection{Source Documentation}\label{doc:plugin}
-\index{Plug-in!Documentation|bfit}
-
-Each plug-in should be properly documented. \framac uses \ocamldoc and so you
-can write any valid \ocamldoc comments.
-
-\paragraph{\ocamldoc tags for \framac}\index{Documentation!Tags} The tag
-\texttt{@since version} should document any element introduced after the very
-first release, in order to easily know the required version of the \framac
-kernel or specific plug-ins. In the same way, the \framac documentation
-generator provides a custom tag \texttt{@modify version description} which
-should be used to document any element which semantics have changed since its
-introduction.
-
-Furthermore, the special tag \texttt{@plugin developer guide} must be attached
-to each function used in this document.
-
-\paragraph{Plug-in API}
-
-A plug-in should export functions in its plug-in interface or through modules
-\texttt{Db}\codeidx{Db} or \texttt{Dynamic}\codeidx{Dynamic} as explained in
-Section~\ref{adv:plugin-registration}.
-
-\begin{important}
-The interface name of a plug-in \texttt{plugin} must be \texttt{Plugin.mli}. Be
-careful to capitalization of the filename which is unusual in \caml but
-required here for compilation purposes.
-\end{important}
-
-\paragraph{Internal Documentation for Kernel Integrated Plug-ins}
-
-The \framac documentation generator also produces an internal plug-in
-documentation which may be useful for the plug-in developer itself. This
-internal documentation is available \emph{via} file
-\texttt{doc/code/$plugin$/index.html}\codeidx{index.html} for each plug-in
-$plugin$. You can add an introduction to this documentation into a file. This
-file has to be assigned into variable
-\texttt{PLUGIN\_INTRO}\codeidx{PLUGIN\_INTRO} of the
-\texttt{Makefile}\codeidx{Makefile} (see Section~\ref{make:plugin}).
-
-In order to ease access to this internal documentation, you have to
-manually edit the file \texttt{doc/index.html}\codeidx{index.html} in order to add
-an entry for your plug-in in the plug-in list.
-
-\paragraph{Internal Documentation for External Plug-ins}
-
-External plug-ins can be documented in the same way as plug-ins that are
-compiled together with \framac. However, in order to be able to compile the
-documentation with \texttt{make doc}, you must have generated the documentation
-of Frama-C's kernel (\texttt{make doc}, see above) and installed it with the
-\texttt{make install-doc-code}\codeidx{install-doc-code} command.
-
-% Local Variables:
-% ispell-local-dictionary: "english"
-% TeX-master: "main"
-% End:
+% \section{Documentation}\label{adv:documentation}
+% \index{Documentation|bfit}
+
+% \begin{prereq}
+% Knowledge of \odoc.
+% \end{prereq}
+
+% Here we present some hints on the way to document your plug-in. First
+% Section~\ref{doc:rules} introduces a quick general overview about the
+% documentation process. Next Section~\ref{doc:plugin} focuses on the
+% plug-in source documentation.
+
+% \subsection{General Overview}\label{doc:rules}
+
+% Command \texttt{make doc}\codeidx{Makefile} produces the whole \framac source
+% documentation\index{Documentation!Source} in HTML format. The generated index
+% file is \texttt{doc/code/html/index.html}. A more general purpose index is
+% \texttt{doc/index.html}\codeidx{index.html} (from which the previous index is
+% accessible).
+
+% The previous command takes times. So command \texttt{make doc-kernel} only
+% generates the kernel documentation\index{Documentation!Kernel} (\emph{i.e.}
+% \framac without any plug-in) while \texttt{make \$(PLUGIN\_NAME)\_DOC} (by
+% substituting the right value for
+% \texttt{\$(PLUGIN\_NAME)})\codeidx{PLUGIN\_NAME} generates
+% the documentation for a single plug-in\index{Plug-in!Documentation}%
+% \index{Documentation!Plug-in|see{Plug-in Documentation}}.
+
+% \subsection{Source Documentation}\label{doc:plugin}
+% \index{Plug-in!Documentation|bfit}
+
+% Each plug-in should be properly documented. \framac uses \ocamldoc and so you
+% can write any valid \ocamldoc comments.
+
+% \paragraph{\ocamldoc tags for \framac}\index{Documentation!Tags} The tag
+% \texttt{@since version} should document any element introduced after the very
+% first release, in order to easily know the required version of the \framac
+% kernel or specific plug-ins. In the same way, the \framac documentation
+% generator provides a custom tag \texttt{@modify version description} which
+% should be used to document any element which semantics have changed since its
+% introduction.
+
+% Furthermore, the special tag \texttt{@plugin developer guide} must be attached
+% to each function used in this document.
+
+% \paragraph{Plug-in API}
+
+% A plug-in should export functions in its plug-in interface or through modules
+% \texttt{Db}\codeidx{Db} or \texttt{Dynamic}\codeidx{Dynamic} as explained in
+% Section~\ref{adv:plugin-registration}.
+
+% \begin{important}
+% The interface name of a plug-in \texttt{plugin} must be \texttt{Plugin.mli}. Be
+% careful to capitalization of the filename which is unusual in \caml but
+% required here for compilation purposes.
+% \end{important}
+
+% \paragraph{Internal Documentation for Kernel Integrated Plug-ins}
+
+% The \framac documentation generator also produces an internal plug-in
+% documentation which may be useful for the plug-in developer itself.
+
+% \paragraph{Internal Documentation for External Plug-ins}
+
+% External plug-ins can be documented in the same way as plug-ins that are
+% compiled together with \framac. However, in order to be able to compile the
+% documentation with \texttt{make doc}, you must have generated the documentation
+% of Frama-C's kernel (\texttt{make doc}, see above) and installed it with the
+% \texttt{make install-doc-code}\codeidx{install-doc-code} command.
+
+\section{Packaging}
+\label{sec:dune-packaging}
+
+If you intend to release your plug-in, a possible way is to take advantage of
+the \texttt{opam} integration within
+\texttt{dune}\footnote{\url{https://dune.readthedocs.io/en/stable/opam.html}}.
+Basically, the \index{dune-project}\texttt{dune-project} file
+(see Section~\ref{tut2:hello}) should contain a stanza
+\texttt{(generate\_opam\_files true)}, as well as some meta-information
+(location of the sources, licence, author(s), etc.). It is also possible to
+provide this information in a file \texttt{my-plugin-package.opam.template},
+assuming \texttt{my-plugin-package} is the name of the package of the plug-in in
+the \texttt{dune-project} file. See the dune documentation for detailed information
+about the creation of the \texttt{opam} file.
+
+% \section{Profiling with Landmarks} \label{refman:landmarks}\codeidxdef{Landmarks}
+
+% {\em Landmarks}\footnote{\url{https://github.com/LexiFi/landmarks}} is a
+% library for ``quick and dirty'' profiling of OCaml programs. It allows the
+% insertion of annotations in the code to enable profiling of specific parts of
+% it, but also an automatic mode, in which every function call is instrumented.
+% The Frama-C \texttt{configure} file is setup to enable usage of this library
+% when it is available (the usual way to install it is via the \texttt{landmarks}
+% opam package).
+
+% For quick usage of the library:
+% \begin{itemize}
+% \item ensure that the \texttt{configure} script detected it
+% (there should be a line \texttt{checking for Landmarks... found});
+% \item enable instrumentation {\em when compiling Frama-C's files}, that is,
+% when running \texttt{make}, by setting the environment variable
+% \verb+OCAML_LANDMARKS+. For instance, to enable automatic instrumentation
+% of every Frama-C function (note: this increases compilation time of Frama-C),
+% run:
+
+% \begin{lstlisting}
+% OCAML_LANDMARKS=auto make
+% \end{lstlisting}
+
+% \item enable instrumentation {\em during execution} of Frama-C, again using
+% \verb+OCAML_LANDMARKS+. Note that the \texttt{auto} parameter here is
+% implicit if you enabled it on the previous step.
+% For instance, run:
+
+% \begin{lstlisting}
+% OCAML_LANDMARKS= bin/frama-c [files] [options]
+% \end{lstlisting}
+% \end{itemize}
+
+% Commonly used options include \verb+output=landmarks.log+ to output the result
+% to a file instead of \texttt{stderr}.
+
+% To instrument a single file: add \verb+[@@@landmark "auto"]+ at the beginning
+% of the file.
+
+% To instrument a single function: add \verb+[@landmark]+ after the \texttt{let},
+% e.g.:
+
+% \begin{lstlisting}
+% let[@landmark] add_visitor vis =
+% \end{lstlisting}
+
+% Check \url{https://github.com/LexiFi/landmarks} for its documentation.
+
+% \textbf{Note:} if you intend to use \texttt{ocamlprof} (via \texttt{ocamlcp} or
+% \texttt{ocamloptp}), which does not support ppx extensions, and you have
+% Landmarks installed, you need to explicitly disable Landmarks during Frama-C's
+% configure: \verb+./configure --disable-landmarks+.
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 0947f4a02893f3d200358f978ad273f39299668f..4e949abc3b74503bb9715505ec5d5ce087691834 100644
--- a/doc/developer/changes.tex
+++ b/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}
diff --git a/doc/developer/introduction.tex b/doc/developer/introduction.tex
index 1415aa6781a1eed48360e1aff10e8ffcfa96e370..54c1ae77b185aa607ac5a7c1815ecb8c02961f1a 100644
--- a/doc/developer/introduction.tex
+++ b/doc/developer/introduction.tex
@@ -1,31 +1,34 @@
-%; 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:
diff --git a/doc/developer/macros.sty b/doc/developer/macros.sty
index 4cba3d771a41dc20a45abb9d1a40bd0e15fb2f10..f53b62d4f33553a62518435393d6ce851be7c1da 100644
--- a/doc/developer/macros.sty
+++ b/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}}
diff --git a/doc/developer/refman.tex b/doc/developer/refman.tex
deleted file mode 100644
index 6bd6389dbb8792f57f4070ec4d9e450f1946fe07..0000000000000000000000000000000000000000
--- a/doc/developer/refman.tex
+++ /dev/null
@@ -1,895 +0,0 @@
-%; whizzy-master "developpeur.tex"
-
-\chapter{Reference Manual}\label{chap:refman}
-
-\begin{target}
-Developers who would like to have a deep understanding of \framac.
-\end{target}
-
-This chapter is a reference manual for \framac developers. It provides details
-completing the previous chapters.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\section{Makefiles}\label{refman:make}\codeidxdef{Makefile}
-
-In this section, we detail the organization of the different Makefiles existing
-in \framac. First Section~\ref{make:overview} presents a general overview. Next
-Section~\ref{make:sections} details the different sections of
-\texttt{Makefile.config.in}, \texttt{Makefile.common},
-\texttt{Makefile.generic}, \texttt{Makefile.generating} and
-\texttt{Makefile}. Next Section~\ref{make:plugin} introduces the variables
-customizing \texttt{Makefile.dynamic}. Finally
-Section~\ref{make:dynamic} shows specific details of \texttt{Makefile.dynamic}.
-
-\subsection{Overview}\label{make:overview}
-
-\framac uses different Makefiles (plus the plug-in specific ones). They are:
-\begin{itemize}
-\item \texttt{Makefile}\codeidxdef{Makefile}: the general Makefile of
- \framac;
-\item \texttt{Makefile.generating}\codeidxdef{Makefile.generating}:
- it contains the complex rules that generate files. It is not
- directly in the general Makefile in order to reduce the dependencies
- of these rules to \texttt{Makefile.generating};
-\item \texttt{Makefile.config.in}\codeidxdef{Makefile.config.in}: the Makefile
- configuring some general variables (especially the ones coming from
- \texttt{configure});
-\item \texttt{Makefile.common}\codeidxdef{Makefile.common}: the Makefile
- providing some other general variables;
-\item \texttt{Makefile.generic}\codeidxdef{Makefile.generic}: the Makefile
- providing generic rules for compiling source files
-\item
- \texttt{.Makefile.plugin.generated}\codeidxdef{.Makefile.plugin.generated}:
- the Makefile introducing specific stuff for plug-in compilation which is
- generated from
- \texttt{Makefile.plugin.template}\codeidxdef{Makefile.plugin.template};
-\item \texttt{Makefile.dynamic}\codeidxdef{Makefile.dynamic}: the Makefile
- usable by plug-in specific Makefiles.
-\item \texttt{Makefile.dynamic\_config}\codeidxdef{Makefile.dynamic\_config}:
- this Makefile is automatically generated either from
- \texttt{Makefile.dynamic\_config.internal}%
- \codeidxdef{Makefile.dynamic\_config.internal} or
- \texttt{Makefile.dynamic\_config.external}%
- \codeidxdef{Makefile.dynamic\_config.external}. It sets variables which
- automatically configure \texttt{Makefile.dynamic}.
-\item \texttt{Makefile.clean}\codeidxdef{Makefile.clean} contains specific
- targets for cleaning which are separated from \texttt{Makefile} for
- performance reasons.
-\item \texttt{.Makefile.user}\codeidxdef{.Makefile.user} is a per-user
- Makefile that can be used to override some variables. If it is not present,
- the default values of \texttt{Makefile} variables will be used.
-\end{itemize}
-\texttt{Makefile}\codeidxdef{Makefile} and
-\texttt{.Makefile.user}\codeidxdef{.Makefile.user} are part of the root
-directory of the \framac distribution while
-the other ones are part of directory \texttt{share}. Each Makefile either
-includes or is included into at least another one. Figure~\ref{fig:makefiles}
-shows these relationships.
-\begin{figure}[htbp]
-\codeidx{Makefile}
-\codeidx{Makefile.generating}
-\codeidx{Makefile.config.in}
-\codeidx{Makefile.plugin.generated}
-\codeidx{Makefile.dynamic}
-\begin{tikzpicture}[
-plugin/.style={fill=Orange,draw=Orange},
-generated/.style={fill=palered,draw=palered},
-kernel/.style={fill=darkgreen,draw=darkgreen},
-other/.style={fill=palered,draw=darkgreen},
-opt/.style={fill=palegreen,draw=palegreen},
-include/.style={-Latex,very thick,fill=none},
-generation/.style={-Latex,very thick,dashed,fill=none},
-]
-\begin{scope}[every node/.style={rounded corners,node font=\small}]
- {[start chain=going right, node distance=\bigpaddelta]
- \node[on chain,kernel,draw=black] (config)
- { Makefile.config.in };
- \node[on chain,kernel,draw=black] (dyn-internal)
- { Makefile.dynamic\_config.internal};
- \node[on chain,kernel,draw=black] (dyn-external)
- { Makefile.dynamic\_config.external};
- }
- \coordinate[yshift=-\largepadding]
- (common-basept) at ($(config.south west)!0.5!(dyn-internal.south east)$);
- {[start chain=kernel-chain going below, node distance=\bigpaddelta]
- \node[on chain,kernel,draw=black,anchor=north] at (common-basept)
- (common) {Makefile.common};
- \node[on chain,kernel,draw=black] (generic) {Makefile.generic};
- }
-
- \node[generated,draw=black,right=\largepadding]
- at ($(kernel-chain-begin.north east)!0.5!(kernel-chain-end.south east)$)
- (dyn) { Makefile.dynamic\_config };
-
- {[start chain=main going right,node distance=\padding]
- \node[on chain,kernel,draw=black,
- below left=\largepadding and \padding]
- at (kernel-chain-end.south west) (generating) { Makefile.generating };
- \node[on chain,kernel,draw=black] (makefile) { Makefile };
- \node[on chain] {\ldots};
- \node[on chain,generated,draw=black]
- (generated) {.Makefile.plugin.generated };
- \node[on chain,kernel,draw=black,node distance=\bigpadding]
- (dynamic) {Makefile.dynamic};
- }
- {[start chain=opt going left,node distance=\bigpaddelta]
- \node[on chain,kernel,draw=black,anchor=north east,yshift=-\bigpadding]
- at (generated.south east) (template) {Makefile.plugin.template};
- \node[on chain,opt,draw=black] (clean) {Makefile.clean};
- \node[on chain,opt,draw=black] (user) {.Makefile.user};
- }
- {[start chain=specific going right,node distance=\bigpaddelta]
- \node[on chain,plugin,draw=black,anchor=north east,xshift=-\largepadding,yshift=-\largepadding]
- at (opt-begin.south east) {Makefile for plug-in 1 };
- \node[on chain] {\ldots};
- \node[on chain,plugin,draw=black] {Makefile for plugin $n$};
- }
-\end{scope}
-\matrix[anchor=north east,yshift=-\bigpadding,matrix of nodes,
-every node/.style={node font=\small,right}] at (specific-end.south east) {
-\textbf{Caption:} \\
-\node at(0,0) (m1) {$m_1$};
-\node at (\largepadding,0) (m2) {$m_2$};
-\draw[include] (m1) -- (m2);
-&
-Makefile $m_1$ is included in Makefile $m_2$
-\\
-\node at(0,0) (gm1) {$m_1$};
-\node at (\largepadding,0) (gm2) {$m_2$};
-\draw[generation] (gm1) -- (gm2);
-&
- Makefile $m_2$ is generated from Makefile $m_1$ \\
-|[plugin,draw=none]| orange boxes & Plug-in Makefiles \\
-|[generated,draw=none]| red boxes & Generated Makefiles \\
-|[kernel,draw=none]| green boxes & Other kernel Makefiles \\
-|[opt,draw=none]| light green boxes & Optional kernel Makefiles \\
-};
-\draw[kernel,include] (config) -- (common);
-\draw[kernel,include] (dyn-internal) to[out=-60,in=20] (node cs:name=makefile,angle=60);
-\draw[generated,generation] (dyn-internal) -- (dyn);
-\draw [generated,generation] (dyn-external) -- (dyn);
-\draw[kernel,include] (common.west) to[out=200,in=135] (node cs:name=makefile,angle=170);
-\draw[kernel,include] (generic.west) to[out=200,in=120]
- (node cs:name=makefile,angle=130);
-\draw[kernel,include] (common) -- (node cs:name=dynamic,angle=50);
-\draw[kernel,include] (generic) -- (node cs:name=dynamic,angle=120);
-\draw[kernel,include] (dyn) -- (node cs:name=dynamic,angle=20);
-\draw[kernel,include] (generating) -- (makefile);
-\draw[plugin,include,bend left] (generated.south west) to (makefile.south east);
-\draw[plugin,include,bend right] (generated.north west) to (makefile.north east);
-\draw[generated,generation] (template) -- (generated);
-\draw[kernel,include] (generated) -- (dynamic);
-\draw[plugin,include,bend left] (dynamic) to (node cs:name=specific-begin,angle=10);
-\draw[plugin,include] (dynamic) -- (specific-end);
-\draw[opt,include] (user) -- (makefile);
-\draw[opt,include] (clean) -- (makefile);
-\end{tikzpicture}
-\caption{Relationship between the Makefiles}\label{fig:makefiles}
-\end{figure}
-\texttt{Makefile} and \texttt{Makefile.dynamic} are independent: the first one
-is used to compile the \framac kernel while the second one is used to compile
-the \framac plug-ins. Their common variables are defined in
-\texttt{Makefile.common} (which includes
-\texttt{Makefile.config.in}). They also include \texttt{Makefile.generic},
-that defines default compilation rules for various kinds of source files.
-\texttt{Makefile.plugin.template} defines generic rules
-and variables for compiling plug-ins. It is used to generate
-\texttt{.Makefile.plugin.generated} for each plugin.
-\texttt{.Makefile.plugin.generated} is included either
-by \texttt{Makefile} for
-kernel-specific plug-ins integrated in \framac Makefile and by
-\texttt{Makefile.dynamic} for plug-ins with their own Makefiles.
-\texttt{.Makefile.user}\codeidxdef{.Makefile.user} is included by
-\texttt{Makefile} when the former exists. It is only used when compiling
-\framac itself, and has no effect for external plugins.
-
-\subsection{Sections of \texttt{Makefile},
- \texttt{Makefile.generating},
- \texttt{Makefile.config.in},
- \texttt{Makefile.common}
- and \texttt{Makefile.generic}}
-\label{make:sections}
-\codeidxdef{Makefile}
-\codeidxdef{Makefile.generating}
-\codeidxdef{Makefile.config.in}
-\codeidxdef{Makefile.common}
-\codeidxdef{Makefile.generic}
-
-Figure~\ref{fig:make-sections} presents the different parts of
-\texttt{Makefile.config.in}, \texttt{Makefile.common},
-\texttt{Makefile.generic}, \texttt{Makefile.generating} and \texttt{Makefile} in
-the order that they are introduced in these files. The third row of the tabular
-says whether the given part may be modified by a kernel-integrated plug-in
-developer\index{Plug-in!Kernel-integrated}. More details are provided below.
-\begin{figure}[htbp]
-\begin{center}
-\begin{tabular}{|c|c|c|c|c|}
-\hline
-\textbf{Id} & \textbf{Name} & \textbf{File} & \textbf{Mod.} &
-\textbf{Reference} \\
-\hline \hline
-1 & Working directories & Makefile.config.in & no & \\
-2 & Installation paths & Makefile.config.in & no & \\
-3 & Ocaml stuff & Makefile.config.in & no & \\
-4 & Libraries & Makefile.config.in & no & \\
-5 & Miscellaneous commands & Makefile.config.in & no & \\
-6 & Miscellaneous variables & Makefile.config.in & no & \\
-7 & Variables for plug-ins & Makefile.config.in & no & \\
-\hline
-1 (bis) & Working directories & Makefile.common & no & \\
-8 & Flags & Makefile.common & no & \\
-9 & Verbosing & Makefile.common & no & \\
-10 & Shell commands & Makefile.common & no & \\
-11 & Command pretty printing & Makefile.common & no & \\
-12 & Tests & Makefile.common & no & \\
-\hline
-13 & Generic rules & Makefile.generic & no & \\
-\hline
-14 & Source files generation & Makefile.generating & no & \\
-\hline
-15 & Global plug-in variables & Makefile & no & \\
-16 & Additional global variables & Makefile & no & \\
-17 & Main targets & Makefile & no & \\
-18 & Coverage & Makefile & no & \\
-19 & Ocamlgraph & Makefile & no & \\
-20 & \framac Kernel & Makefile & no & \\
-21 & Plug-in sections & Makefile & \textbf{yes} & Section~\ref{adv:make} \\
-22 & Generic variables & Makefile & no & \\
-23 & Toplevel & Makefile & no & \\
-24 & GUI & Makefile & no & \\
-25 & Standalone obfuscator & Makefile & no & \\
-26 & Tests & Makefile & no & \\
-27 & Emacs tags & Makefile & no & \\
-28 & Documentation & Makefile & no & \\
-29 & Installation & Makefile & \textbf{yes} & \todoshort \\
-30 & File headers: license policy & Makefile & \textbf{yes}
- & % Section~\ref{adv:copyright}
-\\
-31 & Makefile rebuilding & Makefile & no & \\
-32 & Cleaning & Makefile & no & \\
-33 & Depend & Makefile & no & \\
-34 & \ptests & Makefile & no & \\
-35 & Source distribution & Makefile & no & \\
-\hline
-\end{tabular}
-\end{center}
-\caption{Sections of \texttt{Makefile.config.in}, \texttt{Makefile.common} and
- \texttt{Makefile}.}\label{fig:make-sections}
-\end{figure}
-\begin{enumerate}
-\item \textbf{Working directories} (split between
- \texttt{Makefile.config.in} and \texttt{Makefile.common} defines the main
- directories of \framac. In particular, it declares the variable
- \texttt{FRAMAC\_SRC\_DIRS}\codeidxdef{FRAMAC\_SRC\_DIRS} which should be extended
- by a plug-in developer if he uses files which do not belong to the plug-in
- directory (that is if variable
- \texttt{PLUGIN\_TYPES\_CMO}\codeidx{PLUGIN\_TYPES\_CMO} is set, see
- Section~\ref{make:plugin}).
-\item \textbf{Installation paths} defines where \framac has to be installed.
-\item \textbf{Ocaml stuff} defines the \ocaml compilers and specific related
- flags.
-\item \textbf{Libraries} defines variables for libraries required by \framac.
-\item \textbf{Miscellaneous commands} defines some additional commands.
-\item \textbf{Miscellaneous variables} defines some additional variables.
-\item \textbf{Variables for plug-ins} defines some variables used by plug-ins
- distributed within \framac (and using the \texttt{configure} of \framac).
-\item \textbf{Flags} defines some variables setting compilation flags.
-\item \textbf{Verbosing} sets how \texttt{make} prints the command. In
- particular, it defines the variable \texttt{VERBOSEMAKE}\codeidx{VERBOSEMAKE}
- which must be set \texttt{yes} in order to see the full make commands in the
- user console. The typical use is
-\begin{shell}
-$ make VERBOSEMAKE=yes
-\end{shell}
-\item \textbf{Shell commands} sets all the shell commands eventually executed
- while calling \texttt{make}.
-\item \textbf{Command pretty printing} sets all the commands to be used for
- pretty printing.
-\begin{example}
-Consider the following target \texttt{foo} in a plug-in specific Makefile.
-\codeidx{PRINT\_CP}\codeidx{CP}
-\begin{makefilecode}
-foo: bar
- $(PRINT_CP) $@
- $(CP) $< $@
-\end{makefilecode}
-Executing
-\begin{shell}
-$ make foo
-\end{shell}
-prints
-\begin{shell}
-Copying to foo
-\end{shell}
-while executing\codeidx{VERBOSEMAKE}
-\begin{shell}
-$ make foo VERBOSEMAKE=yes
-\end{shell}
-prints
-\begin{shell}
-cp -f bar foo
-\end{shell}
-If one of the two commands is missing for the target \texttt{foo}, either
-\texttt{make foo} or \texttt{make foo VERBOSEMAKE=yes} will not work as
-expected.
-\end{example}
-\item \textbf{Tests} defines a generic template for testing plug-ins.
-\item \textbf{Generic rules} contains rules in order to automatically produces
- different kinds of files (\emph{e.g.} \texttt{.cm[iox]} from \texttt{.ml} or
- \texttt{.mli} for \ocaml files)
-\item \textbf{Source files generation} contains rules for generating files
- that depend on the configuration and on which the main \texttt{Makefile}
- depends on. They are put in an auxiliary \texttt{Makefile.generating} to
- avoid unnecessary rebuilds.
-\item \textbf{Global plug-in variables} declares some plug-in specific variables
- used throughout the makefile.
-\item \textbf{Additional global variables} declares some other variables used
- throughout the makefile.
-\item \textbf{Main targets} provides the main rules of the makefile. The most
- important ones are \texttt{top}, \texttt{byte} and \texttt{opt} which
- respectively build the \framac interactive, bytecode and native toplevels.
-\item \textbf{Coverage} defines how compile the eponymous library.
-\item \textbf{Ocamlgraph} defines how compile the eponymous library.
-\item \textbf{\framac Kernel} provides variables and rules for the \framac
- kernel\index{Kernel}. Each part is described in specific sub-sections.
-\item ~\\[-6mm]
- \begin{important}
- After Section ``Kernel'', there are several sections corresponding to
- \textbf{plug-ins}\index{Plug-in!Compilation} (see
- Section~\ref{make:plugin}). This is the part that a plug-in developer has to
- modify in order to add compilation directives for its plug-in.
- \end{important}
-\item \textbf{Generic variables} provides variables containing files to be
- linked in different contexts.
-\item \textbf{Toplevel} provides rules for building the files of the form
- \texttt{bin/toplevel.*}.
-\item \textbf{GUI} provides rules for building the files of the form
- \texttt{bin/viewer.*}
-\item \textbf{Standalone obfuscator} provides rules for building the \framac
- obfuscator.
-\item\label{make:sec:tests}
- \textbf{Tests} provides rules to execute tests\index{Test}.
- \verb|make tests| takes care of generating the appropriate environment and
- launching \texttt{ptests} (see Section~\ref{adv:ptests}) for all
- test suites of the kernel and enabled plugins. It is possible
- to pass options to \texttt{ptests} through the
- \texttt{PTESTS\_OPTS}\codeidxdef{PTESTS\_OPTS} environment variable.
-\item \textbf{Emacs tags} provides rules which generate \emacs tags (useful for
- a quick search of \caml definitions).\index{Tags}
-\item \textbf{Documentation} provides rules generating \framac source
- documentation (see Section~\ref{adv:documentation}).\index{Documentation}
-\item \textbf{Installation} provides rules for installing different parts of
- \framac.
-\item \textbf{File headers: license policy} provides variables and rules to
- manage the \framac license policy.
- \index{Header}\index{License}
-\item \textbf{Makefile rebuilding} provides rules in order to automatically
- rebuild \texttt{Makefile} and \texttt{configure} when required.
-\item \textbf{Cleaning} provides rules in order to remove files generated by
- makefile rules.
-\item \textbf{Depend} provides rules which compute \framac source dependencies.
-\item \textbf{Ptests} provides rules in order to build \ptests (see
- Section~\ref{adv:ptests}).\index{Ptests}
-\item \textbf{Source distribution} provides rules usable for distributing
- \framac.
-\end{enumerate}
-
-\subsection{Variables of \texttt{Makefile.dynamic}}
-\label{make:plugin}
-\codeidxdef{Makefile.dynamic}
-
-Figures~\ref{fig:make-parameters} and~\ref{fig:special-parameters}
-presents all the variables that can be set before including
-\texttt{Makefile.dynamic} (see Section~\ref{adv:dynamic-make}).
-Details are provided below.
-\begin{figure}[htbp]
-\begin{center}
-\begin{tabularx}{\textwidth}{|c|c|X|}
-\hline
-\textbf{Kind} & \textbf{Name} & \textbf{Specification} \\
-\hline \multirow{5}{27mm}{\centering{Plug-in Declaration}}
-& \texttt{PLUGIN\_NAME} & Module name of the plug-in \\
-& \texttt{PLUGIN\_DIR} & Directory containing plug-in source files \\
-& \texttt{PLUGIN\_ENABLE} & Whether to compile the plug-in \\
-& \texttt{PLUGIN\_HAS\_META} & Provided \texttt{META} (default: \texttt{no})\\
-\hline \multirow{4}{27mm}{\centering{Packaging\\(for \texttt{META})}}
-& \texttt{PLUGIN\_DESCRIPTION} & Short description (defaults to name) \\
-& \texttt{PLUGIN\_VERSION} & Version number (defaults to \framac's) \\
-& \texttt{PLUGIN\_DEPENDENCIES} & Dependencies to other plug-ins\\
-& \texttt{PLUGIN\_REQUIRES} & Dependencies to \texttt{ocamlfind} packages\\
-\hline \multirow{4}{27mm}{\centering{Object Files}}
-& \texttt{PLUGIN\_CMO} & Object files (without \texttt{.cmo}) \\
-& \texttt{PLUGIN\_CMI} & Standalone interfaces (without \texttt{.cmi}) \\
-& \texttt{PLUGIN\_GUI\_CMO} & Additional objects files for the GUI \\
-& \texttt{PLUGIN\_TYPES\_CMO} & External \texttt{.cmo} files \\
-\hline \multirow{6}{27mm}{\centering{Compilation flags}}
-& \texttt{PLUGIN\_BFLAGS} & Plug-in specific flags for \texttt{ocamlc} \\
-& \texttt{PLUGIN\_OFLAGS} & Plug-in specific flags for \texttt{ocamlopt} \\
-& \texttt{PLUGIN\_EXTRA\_BYTE} & Additional bytecode files to link against \\
-& \texttt{PLUGIN\_EXTRA\_OPT} & Additional native files to link against \\
-& \texttt{PLUGIN\_EXTRA\_DIRS} & Additional directories containing source files, relative to the root directory of the plugin (i.e. \texttt{PLUGIN\_DIR}) \\
-& \texttt{PLUGIN\_LINK\_BFLAGS} & Plug-in specific flags for linking with
-\texttt{ocamlc} \\
-& \texttt{PLUGIN\_LINK\_OFLAGS} & Plug-in specific flags for linking with
-\texttt{ocamlopt} \\
-& \texttt{PLUGIN\_LINK\_GUI\_BFLAGS} & Plug-in specific flags for linking a GUI
-with \texttt{ocamlc} \\
-& \texttt{PLUGIN\_LINK\_GUI\_OFLAGS} & Plug-in specific flags for linking a GUI
-with \texttt{ocamlopt} \\
-\hline
-\end{tabularx}
-\end{center}
-\caption{Standard parameters of \texttt{Makefile.dynamic}.}\label{fig:make-parameters}
-\end{figure}
-\begin{itemize}
-\item Variable \texttt{PLUGIN\_NAME}\codeidxdef{PLUGIN\_NAME}
- is the module name of the plug-in.\index{Plug-in!Name}
-
- \begin{important}
- This name must be capitalized (as is each \caml module name). It
- must be distinct from all other visible modules in the plugin
- directory, or in the \framac kernel.
- \end{important}
-\item Variable \texttt{PLUGIN\_DIR}\codeidxdef{PLUGIN\_DIR}
- is the directory containing plug-in source files\index{Plug-in!Directory}. It
- is usually set to \texttt{src/plugins/$plugin$} where $plugin$ is the
- plug-in name.
-\item Variable
- \texttt{PLUGIN\_ENABLE}\codeidxdef{PLUGIN\_ENABLE} must be
- set to \yes if the plug-in has to be compiled. It is usually set to
- \texttt{@$plugin$\_ENABLE@} provided by \texttt{configure.in} where $plugin$
- is the plug-in name.
-\item Variable
- \texttt{PLUGIN\_HAS\_META}\codeidxdef{PLUGIN\_HAS\_META} must
- be set to \yes if plug-in $plugin$ gets a \texttt{META} file
- describing its packaging. Unless \texttt{PLUGIN\_HAS\_META} is \texttt{yes},
- the following variables are used to generate a suitable \texttt{META}:
- \begin{itemize}
- \item \texttt{PLUGIN\_VERSION}\codeidxdef{PLUGIN\_VERSION}
- short text with $plugin$ version number.
- Default value is \framac's version number.
- \item \texttt{PLUGIN\_REQUIRES}\codeidxdef{PLUGIN\_REQUIRES}
- packages that must be loaded before the $plugin$.
- By default, there is no such package.
- \item \texttt{PLUGIN\_DEPENDENCIES}\codeidxdef{PLUGIN\_DEPENDENCIES}
- other plug-ins that must be loaded before the $plugin$.
- By default, there is no dependency.
- \end{itemize}
- \textbf{Remark:} the $plugin$ package name is defined to be \texttt{frama-c-$plugin$} with
- lowercased plugin name. You can refer to it directly with \texttt{ocamlfind}.
-\item Variables \texttt{PLUGIN\_CMO}\codeidxdef{PLUGIN\_CMO}
- and \texttt{PLUGIN\_CMI}\codeidxdef{PLUGIN\_CMI} are
- respectively \texttt{.cmo} plug-in files and \texttt{.cmi} files without
- corresponding \texttt{.cmo} plug-in files. For each of them, do not write
- their file path nor their file extension: they are automatically added
- (\texttt{\$(PLUGIN\_DIR)/$f$.cm[io]} for a file $f$).
-\item Variable
- \texttt{PLUGIN\_TYPES\_CMO}\codeidxdef{PLUGIN\_TYPES\_CMO}
- is the \texttt{.cmo} plug-in files which do not belong to
- \texttt{\$(PLUGIN\_DIR)}. They usually belong to
- \texttt{src/plugins/$plugin$\_types} where $plugin$ is the plug-in name (see
- Section~\ref{adv:static-registration}). Do not
- write file extension (which is \texttt{.cmo}): it is automatically
- added.\index{Plug-in!Types}
-\item Variable
- \texttt{PLUGIN\_GUI\_CMO}\codeidxdef{PLUGIN\_GUI\_CMO} is
- the \texttt{.cmo} plug-in files which have to be linked with the GUI (see
- Section~\ref{adv:gui}). As for variable \texttt{PLUGIN\_CMO}, do not write
- their file path nor their file extension.\index{Plug-in!GUI}
-%
-\item Variables of the form \texttt{PLUGIN\_*\_FLAGS} are
- plug-in specific flags for \texttt{ocamlc}, \texttt{ocamlopt},
- \texttt{ocamldep} or \texttt{ocamldoc}.
- \codeidxdef{PLUGIN\_BFLAGS}
- \codeidxdef{PLUGIN\_OFLAGS}
- \codeidxdef{PLUGIN\_EXTRA\_BYTE}
- \codeidxdef{PLUGIN\_EXTRA\_OPT}
- \codeidxdef{PLUGIN\_EXTRA\_DIRS}
- \codeidxdef{PLUGIN\_LINK\_OFLAGS}
- \codeidxdef{PLUGIN\_LINK\_GUI\_BFLAGS}
- \codeidxdef{PLUGIN\_LINK\_GUI\_OFLAGS}
- \codeidxdef{PLUGIN\_DEPFLAGS}
- \codeidxdef{PLUGIN\_DOCFLAGS}
-\end{itemize}
-%%%%
-\begin{figure}[htbp]
-\begin{center}
-\begin{tabularx}{\textwidth}{|c|c|X|c|}
-\hline
-\textbf{Kind} & \textbf{Name} & \textbf{Specification} & \\
-\hline
-\hline \multirow{3}{27mm}{\centering{Dependencies}}
-& \texttt{PLUGIN\_DEPFLAGS} & Plug-in specific flags for \texttt{ocamldep} &\\
-& \texttt{PLUGIN\_GENERATED} & Plug-in files to be generated before running
-\texttt{ocamldep} &\\
-& \texttt{PLUGIN\_DEPENDS} & Other plug-ins to be compiled before the considered
-one & no \\
-\hline \multirow{5}{27mm}{\centering{Documentation}}
-& \texttt{PLUGIN\_DOCFLAGS} & Plug-in specific flags for \texttt{ocamldoc}& \\
-& \texttt{PLUGIN\_UNDOC} & Source files with no provided documentation &\\
-& \texttt{PLUGIN\_TYPES\_TODOC} & Additional source files to document &\\
-& \texttt{PLUGIN\_INTRO} & Text file to append to the plug-in introduction & \\
-& \texttt{PLUGIN\_HAS\_EXT\_DOC} & Whether the plug-in has an external
-pdf manual &\\
-\hline \multirow{7}{27mm}{\centering{Testing}}
-& \texttt{PLUGIN\_NO\_TESTS} & Whether there is no plug-in specific test
-directory & \\
-& \texttt{PLUGIN\_TESTS\_DIRS} & Directories containing tests &\\
-& \texttt{PLUGIN\_TESTS\_DIRS\_DEFAULT} & tests to be included in the default
-test suite (all directories by default) & no \\
-& \texttt{PLUGIN\_TESTS\_LIBS} & Specific \texttt{.ml} files used by plug-in
-tests &\\
-& \texttt{PLUGIN\_NO\_DEFAULT\_TEST} & Whether to include tests
-in default test suite. &\\
-& \texttt{PLUGIN\_INTERNAL\_TEST} & Whether the test suite of the
-plug-in is located in \framac's own tests directory &\\
-& \texttt{PLUGIN\_PTESTS\_OPTS} & Plug-in specific options to ptests &\\
-\hline \multirow{3}{25mm}{\centering{Distribution}}
-& \texttt{PLUGIN\_DISTRIBUTED\_BIN} & Whether to include the plug-in
-in binary distribution & no \\
-& \texttt{PLUGIN\_DISTRIBUTED} & Whether to include the plug-in in
-source distribution & no \\
-& \texttt{PLUGIN\_DISTRIB\_EXTERNAL} & Additional files to be included
-in the distribution & no \\
-\hline
-\end{tabularx}
-\end{center}
-\caption{Special parameters of \texttt{Makefile.dynamic}.}\label{fig:special-parameters}
-\end{figure}
-\begin{itemize}
-\item Variable
- \texttt{PLUGIN\_GENERATED}\codeidxdef{PLUGIN\_GENERATED} is
- files which must be generated before computing plug-in dependencies. In
- particular, this is where \texttt{.ml} files generated by \texttt{ocamlyacc}
- and \texttt{ocamllex} must be placed if needed.
-\item Variable
- \texttt{PLUGIN\_DEPENDS}\codeidxdef{PLUGIN\_DEPENDS} is the
- other plug-ins which must be compiled before the considered plug-in.
-
- \begin{important}
- Using this variable is deprecated: you should consider to use
- \texttt{PLUGIN\_DEPENDENCIES} instead.
- \end{important}
-%
-\item Variable
- \texttt{PLUGIN\_UNDOC}\codeidxdef{PLUGIN\_UNDOC} is the
- source files for which no documentation is provided. Do not write their file
- path which is automatically set to
- \texttt{\$(PLUGIN\_DIR)}.\index{Plug-in!Documentation}
-\item Variable \texttt{PLUGIN\_TYPES\_TODOC}%
- \codeidxdef{PLUGIN\_TYPES\_TODOC} is the additional source
- files to document with the plug-in. They usually belong to
- \texttt{src/plugins/$plugin$\_types} where $plugin$ is the plug-in name (see
- Section~\ref{adv:static-registration}).
- \index{Plug-in!Documentation}\index{Plug-in!Types}
-\item Variable
- \texttt{PLUGIN\_INTRO}\codeidxdef{PLUGIN\_INTRO} is the
- text file to append to the plug-in documentation introduction. Usually this
- file is \texttt{doc/code/intro\_$plugin$.txt} for a plug-in $plugin$. It can
- contain any text understood by \texttt{ocamldoc}.\index{Plug-in!Documentation}
-\item Variable
- \texttt{PLUGIN\_HAS\_EXT\_DOC}%
- \codeidxdef{PLUGIN\_HAS\_EXT\_DOC} is set to yes if
- the plug-in has its own reference manual. It is supposed to be a
- \texttt{pdf} file generated by \texttt{make} in directory
- \texttt{doc/\$(PLUGIN\_NAME)}\index{Plug-in!Documentation}
-%
-\item Variable
- \texttt{PLUGIN\_NO\_TEST}\codeidxdef{PLUGIN\_NO\_TEST} must
- be set to \yes if there is no specific test directory for the
- plug-in.\index{Plug-in!Test}
-\item Variable
- \texttt{PLUGIN\_TESTS\_DIRS}\codeidxdef{PLUGIN\_TESTS\_DIRS}
- is the directories containing plug-in tests. Its default value is
- \texttt{tests/\$(notdir \$(PLUGIN\_DIR))}).\index{Plug-in!Test}
-\item Variable
- \texttt{PLUGIN\_TESTS\_LIB}\codeidxdef{PLUGIN\_TESTS\_LIB}
- contains the \texttt{.ml} plug-in specific files used by plug-in
- tests.\index{Plug-in!Test} Note that if you wish to have these files
- compiled before launching the tests (as opposed to e.g. compile them via
- an \verb|EXECNOW| directive in a test file), you should add the
- corresponding \verb|.cmo| and \verb|.cmxs| files as pre-requisite
- of the \verb|$(PLUGIN_DIR)/tests/ptests_config| %$
- target.
-\item Variable
- \texttt{PLUGIN\_NO\_DEFAULT\_TEST}%
- \codeidxdef{PLUGIN\_NO\_DEFAULT\_TEST} indicates
- whether the test directory of the plug-in should be considered when
- running \framac default test suite. When set to a non-empty value,
- the plug-in tests are run only through \texttt{make
- \$(PLUGIN\_NAME)\_tests}.\index{Plug-in!Test}
-\item Variable
- \texttt{PLUGIN\_INTERNAL\_TEST}%
- \codeidxdef{PLUGIN\_INTERNAL\_TEST} indicates
- whether the tests of the plug-in are included in \framac's own tests
- directory. When set to a non-empty value, the tests are searched
- there. When unset, tests are assumed to be in the \texttt{tests}
- directory of the plugin main directory itself. Having the tests of a
- plugin inside \framac's own \texttt{tests} suite is
- deprecated. Plugins should be self-contained.
-\item Variable
- \texttt{PLUGIN\_PTESTS\_OPTS}%
- \codeidxdef{PLUGIN\_PTESTS\_OPTS} allows to give specific options to
- \texttt{ptests} when running the tests. It comes in addition to
- \texttt{PTESTS\_OPTS}
- (see~\ref{make:sections}\textsection\ref{make:sec:tests}).
- For instance,
- \verb|PLUGIN_PTESTS_OPTS:=-j 1| will deactivate parallelization of tests in case
- the plugin does not support concurrent runs.
-%
-\item Variable
-\texttt{PLUGIN\_DISTRIB\_BIN}%
-\codeidxdef{PLUGIN\_DISTRIB\_BIN}
-indicates whether the plug-in should be included in a binary distribution.%
-\index{Plug-in!Distribution}
-\item Variable
-\texttt{PLUGIN\_DISTRIBUTED}%
-\codeidxdef{PLUGIN\_DISTRIBUTED}
-indicates whether the plug-in should be included in a source distribution.%
-\index{Plug-in!Distribution}
-\item Variable
-\texttt{PLUGIN\_DISTRIB\_EXTERNAL}%
-\codeidxdef{PLUGIN\_DISTRIB\_EXTERNAL}
-is the list of files that should be included within the source
-distribution for this plug-in. They will be put at their proper place for a
-release.\index{Plug-in!Distribution}
-\end{itemize}
-As previously said, the above variables are set before including
-\texttt{Makefile.dynamic} in order to customize its behavior. They
-must not be use anywhere else in the Makefile. In order to deal with this
-issue, for each plug-in $p$, \texttt{Makefile.dynamic} provides some variables
-which may be used after its inclusion defining $p$. These variables are listed
-in Figure~\ref{fig:make-defvars}. For each variable of the form
-\texttt{$p$\_VAR}, its behavior is exactly equivalent to the value of the
-parameter \texttt{PLUGIN\_VAR} for the plug-in $p$\footnote{Variables of the
- form \texttt{$p$\_*CMX} have no \texttt{PLUGIN\_*CMX} counterpart but their
- meanings should be easy to understand.}.
-\begin{figure}[htbp]
-\begin{center}
-\begin{tabularx}{\textwidth}{|c|c|X|}
-\hline
-\textbf{Kind} & \textbf{Name}\footnotemark & \textbf{Remarks}\\
-\hline
-\hline \multirow{1}{35mm}{\centering{Usual information}}
-& \texttt{$plugin$\_DIR}\index{plugin\_DIR@\texttt{$plugin$\_DIR}|bfit} & \\
-\hline \multirow{5}{35mm}{\centering{Source files}}
-& \texttt{$plugin$\_CMO}\index{plugin\_CMO@\texttt{$plugin$\_CMO}|bfit} & \\
-& \texttt{$plugin$\_CMI}\index{plugin\_CMI@\texttt{$plugin$\_CMI}|bfit} & \\
-& \texttt{$plugin$\_CMX}\index{plugin\_CMI@\texttt{$plugin$\_CMI}|bfit} & \\
-& \texttt{$plugin$\_TYPES\_CMO}%
-\index{plugin\_TYPES\_CMO@\texttt{$plugin$\_TYPES\_CMO}|bfit} & \\
-& \texttt{$plugin$\_TYPES\_CMX}%
-\index{plugin\_TYPES\_CMX@\texttt{$plugin$\_TYPES\_CMX}|bfit} & \\
-\hline \multirow{10}{35mm}{\centering{Targets}}
-& \texttt{$plugin$\_TARGET\_CMO}%
-\index{plugin\_TARGET_CMO@\texttt{$plugin$\_TARGET\_CMO}|bfit} & \\
-& \texttt{$plugin$\_TARGET\_CMX}%
-\index{plugin\_TARGET\_CMX@\texttt{$plugin$\_TARGET\_CMX}|bfit} & \\
-& \texttt{$plugin$\_TARGET\_CMA}%
-\index{plugin\_TARGET\_CMA@\texttt{$plugin$\_TARGET\_CMA}|bfit}
-& Empty if plug-in does not have external dependencies
-\\
-& \texttt{$plugin$\_TARGET\_CMXA}%
-\index{plugin\_TARGET\_CMXA@\texttt{$plugin$\_TARGET\_CMXA}|bfit}
-& Empty if plug-in does not have external dependencies
-\\
-& \texttt{$plugin$\_TARGET\_CMXS}%
-\index{plugin\_TARGET\_CMXS@\texttt{$plugin$\_TARGET\_CMXS}|bfit}
-& Empty if plugin is not dynamic
-\\
-& \texttt{$plugin$\_TARGET\_GUI\_CMO}%
-\index{plugin\_TARGET\_GUI\_CMO@\texttt{$plugin$\_TARGET\_GUI\_CMO}|bfit}
-& \rdelim\}{5}{\hsize}[\parbox{\hsize-7mm}{Empty if there is no plugin-specific GUI code}]
-\\
-& \texttt{$plugin$\_TARGET\_GUI\_CMX}%
-\index{plugin\_TARGET\_GUI\_CMX@\texttt{$plugin$\_TARGET\_GUI\_CMX}|bfit}
-&
-\\
-& \texttt{$plugin$\_TARGET\_GUI\_CMA}%
-\index{plugin\_TARGET\_GUI\_CMA@\texttt{$plugin$\_TARGET\_GUI\_CMA}|bfit}
-& \\
-& \texttt{$plugin$\_TARGET\_GUI\_CMXA}%
-\index{plugin\_TARGET\_GUI\_CMXA@\texttt{$plugin$\_TARGET\_GUI\_CMXA}|bfit}
-& \\
-& \texttt{$plugin$\_TARGET\_GUI\_CMXS}%
-\index{plugin\_TARGET\_GUI\_CMXS@\texttt{$plugin$\_TARGET\_GUI\_CMXS}|bfit}
-& \\
-\hline \multirow{6}{35mm}{\centering{Compilation flags}}
-& \texttt{$plugin$\_BFLAGS}%
-\index{plugin\_BFLAGS@\texttt{$plugin$\_BFLAGS}|bfit} & \\
-& \texttt{$plugin$\_OFLAGS}%
-\index{plugin\_OFLAGS@\texttt{$plugin$\_OFLAGS}|bfit} & \\
-& \texttt{$plugin$\_LINK\_BFLAGS}%
-\index{plugin\_LINK\_BFLAGS@\texttt{$plugin$\_LINK\_BFLAGS}|bfit} & \\
-& \texttt{$plugin$\_LINK\_OFLAGS}%
-\index{plugin\_LINK\_OFLAGS@\texttt{$plugin$\_LINK\_OFLAGS}|bfit} & \\
-& \texttt{$plugin$\_LINK\_GUI\_BFLAGS}%
-\index{plugin\_LINK\_GUI\_BFLAGS@\texttt{$plugin$\_LINK\_GUI\_BFLAGS}|bfit} & \\
-& \texttt{$plugin$\_LINK\_GUI\_OFLAGS}%
-\index{plugin\_GUI\_OFLAGS@\texttt{$plugin$\_GUI\_OFLAGS}|bfit} & \\
-\hline \multirow{2}{35mm}{\centering{Dependencies}}
-& \texttt{$plugin$\_DEPFLAGS}%
-\index{plugin\_DEPFLAGS@\texttt{$plugin$\_DEPFLAGS}|bfit} & \\
-& \texttt{$plugin$\_GENERATED}%
-\index{plugin\_GENERATED@\texttt{$plugin$\_GENERATED}|bfit} & \\
-\hline \multirow{2}{35mm}{\centering{Documentation}}
-& \texttt{$plugin$\_DOCFLAGS}%
-\index{plugin\_DOCFLAGS@\texttt{$plugin$\_DOCFLAGS}|bfit} & \\
-& \texttt{$plugin$\_TYPES\_TODOC}%
-\index{plugin\_TYPES\_TODOC@\texttt{$plugin$\_TYPES\_TODOC}|bfit} & \\
-\hline \multirow{2}{35mm}{\centering{Testing}}
-& \texttt{$plugin$\_TESTS\_DIRS}%
-\index{plugin\_TESTS\_DIRS@\texttt{$plugin$\_TESTS\_DIRS}|bfit} & \\
-& \texttt{$plugin$\_TESTS\_LIB}%
-\index{plugin\_TESTS\_LIB@\texttt{$plugin$\_TESTS\_LIB}|bfit} & \\
-\hline
-\end{tabularx}
-\end{center}
-\caption{Variables defined by \texttt{Makefile.dynamic}.}\label{fig:make-defvars}
-\end{figure}
-\footnotetext{$plugin$ is the module name of the considered plug-in (\emph{i.e.}
- as set by
- \texttt{\$(PLUGIN\_NAME)})\codeidx{PLUGIN\_NAME}.}
-
-\subsection{\texttt{.Makefile.user}}
-\codeidx{.Makefile.user}
-
-The following variables can be set inside \texttt{.Makefile.user}:
-\begin{itemize}
-\item \texttt{FRAMAC\_PARALLEL}: the contents of this variable are passed
-to \texttt{ptests} when it is called by \framac's Makefile. This variable
-can be used to override the default value of 4.
-
-\emph{Example value:} \texttt{-j 6}
-
-\item \texttt{OCAML\_ANNOT\_OPTION}: this variable of the Makefile
-can be overridden in \texttt{.Makefile.user}.
-By default, it is set to \texttt{-annot -bin-annot}. Users of
-\textsf{Merlin}\index{Merlin} do not need \texttt{-annot}.
-
-\emph{Example value:} \texttt{-bin-annot}
-
-\item \texttt{FRAMAC\_USER\_FLAGS}: the contents of this variable are
-passed to \texttt{ocamlc} and \texttt{ocamlopt}, \emph{after} the standard
-configuration options coming from the Makefile. It can be used to tweak
-the warnings emitted by OCaml, and whether they are emitted as errors.
-
-\emph{Example value:} \texttt{-warn-error -26-27} (do not consider warnings
-26 and 27 as fatal errors)
-
-\item \texttt{FRAMAC\_USER\_MERLIN\_FLAGS}: the contents of this variable are
-passed to a directive \texttt{FLG}, inside the \texttt{.merlin} file generated
-for \framac. (Through the \texttt{merlin} target of the
-main \texttt{Makefile}.) It can be used to tailor \textsf{Merlin}\index{Merlin}
-to your needs. See \texttt{ocamlmerlin -help} for the list of flags.
-
-
-\end{itemize}
-
-\subsection{\texttt{Makefile.dynamic}}
-\label{make:dynamic}
-
-\todo
-
-\section{Ptests}\label{sec:ptests}
-\subsection{Pre-defined macros for tests commands}\label{sec:ptests-macros}
-Ptests pre-defines a certain number of macros for each test about to be run.
-Figure~\ref{fig:ptests-macros} gives their definition.
-\begin{longtable}{|p{4.5cm}|p{10cm}|}
-\hline
-Name & Expansion \\
-\hline
-\verb|frama-c| & path to \framac executable \\
-\hline
-\verb|PTEST_CONFIG| & either the empty string or \verb|_| followed by the
-name of the current alternative configuration
-(see section~\ref{ptests:alternative}). \\
-\hline
-\verb|PTEST_DIR| & current test suite directory \\
-\hline
-\verb|PTEST_RESULT| & current result directory \\
-\hline
-\verb|PTEST_FILE| & path to the current test file \\
-\hline
-\verb|PTEST_NAME| & basename of the current test file (without suffix) \\
-\hline
-\verb|PTEST_NUMBER| & rank of current test in the test file. There are in
-fact two independent numbering schemes: one for \verb|EXECNOW| commands and
-one for regular tests (if more than one \verb|OPT|).\\
-\hline
-\verb|PTEST_RESULT| & shorthand alias to \verb|@PTEST_DIR@/result@PTEST_CONFIG@|
-(the result directory dedicated to the tested configuration)\\
-\hline
-\verb|PTEST_ORACLE| & basename of the current oracle file (macro only usable in FILTER directives)\\
-\hline
-\verb|PTEST_MODULE| & current list of module defined by the \verb|MODULE| directive\\
-\hline
-\verb|PTEST_LIBS| & current list of module defined by the \verb|LIBS| directive\\
-\hline
-\verb|PTEST_PLUGIN| & current list of plugins defined by the \verb|PLUGIN| directive\\
-\hline
-\verb|PTEST_SCRIPT| & current list of plugins defined by the \verb|SCRIPT| directive\\
-\hline
-\verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-check| \verb|-no-autoload-plugins|\\
-\hline
-\verb|PTEST_LOAD_MODULE| & the \verb|-load-module| option related to the \verb|MODULE| directive\\
-\hline
-\verb|PTEST_LOAD_LIBS| & the \verb|-load-module| option related to the \verb|LIBS| directive\\
-\hline
-\verb|PTEST_LOAD_PLUGIN| & the \verb|-load-module| option related to the \verb|PLUGIN| directive\\
-\hline
-\verb|PTEST_LOAD_SCRIPT| & the \verb|-load-script| option related to the \verb|SCRIPT| directive\\
-\hline
-\verb|PTEST_LOAD_OPTIONS| & shorthand alias to \spverb|@PTEST_LOAD_PLUGIN@ @PTEST_LOAD_LIBS@ @PTEST_LOAD_MODULE@ @PTEST_LOAD_SCRIPT@|\\
-\hline
-\verb|PTEST_OPTIONS| & the current list of options related to \verb|OPT| and \verb|STDOPT| directives (for \verb|CMD| directives)\\
-\hline
-\verb|frama-c| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@|\\
-\hline
-\verb|frama-c-cmd| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@|\\
-\hline
-\verb|frama-c-exe| & set to the value of the \verb|TOPLEVEL_PATH| variable from \verb|./tests/ptests_config| file\\
-\hline
-\caption{Predefined macros for ptests}\label{fig:ptests-macros}
-\end{longtable}
-
-\section{Profiling with Landmarks} \label{refman:landmarks}\codeidxdef{Landmarks}
-
-{\em Landmarks}\footnote{\url{https://github.com/LexiFi/landmarks}} is a
-library for ``quick and dirty'' profiling of OCaml programs. It allows the
-insertion of annotations in the code to enable profiling of specific parts of
-it, but also an automatic mode, in which every function call is instrumented.
-The Frama-C \texttt{configure} file is setup to enable usage of this library
-when it is available (the usual way to install it is via the \texttt{landmarks}
-opam package).
-
-For quick usage of the library:
-\begin{itemize}
-\item ensure that the \texttt{configure} script detected it
- (there should be a line \texttt{checking for Landmarks... found});
-\item enable instrumentation {\em when compiling Frama-C's files}, that is,
- when running \texttt{make}, by setting the environment variable
- \verb+OCAML_LANDMARKS+. For instance, to enable automatic instrumentation
- of every Frama-C function (note: this increases compilation time of Frama-C),
- run:
-
-\begin{lstlisting}
- OCAML_LANDMARKS=auto make
-\end{lstlisting}
-
-\item enable instrumentation {\em during execution} of Frama-C, again using
- \verb+OCAML_LANDMARKS+. Note that the \texttt{auto} parameter here is
- implicit if you enabled it on the previous step.
- For instance, run:
-
- \begin{lstlisting}
- OCAML_LANDMARKS= bin/frama-c [files] [options]
- \end{lstlisting}
-\end{itemize}
-
-Commonly used options include \verb+output=landmarks.log+ to output the result
-to a file instead of \texttt{stderr}.
-
-To instrument a single file: add \verb+[@@@landmark "auto"]+ at the beginning
-of the file.
-
-To instrument a single function: add \verb+[@landmark]+ after the \texttt{let},
-e.g.:
-
-\begin{lstlisting}
- let[@landmark] add_visitor vis =
-\end{lstlisting}
-
-Check \url{https://github.com/LexiFi/landmarks} for its documentation.
-
-\textbf{Note:} if you intend to use \texttt{ocamlprof} (via \texttt{ocamlcp} or
-\texttt{ocamloptp}), which does not support ppx extensions, and you have
-Landmarks installed, you need to explicitly disable Landmarks during Frama-C's
-configure: \verb+./configure --disable-landmarks+.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Local Variables:
-%%% TeX-master: "developer.tex"
-%%% ispell-local-dictionary: "english"
-%%% End:
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 71ad53c24ebdbf84934ed30b7eaeb976be93f52b..076cf179d056e9744d2d08665863d6ae1ae6aff9 100644
--- a/doc/developer/tutorial.tex
+++ b/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:
diff --git a/doc/developer/tutorial/hello/src/Makefile b/doc/developer/tutorial/hello/src/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..bfdef3c8367de27c5ec3c892320c60444ead1574
--- /dev/null
+++ b/doc/developer/tutorial/hello/src/Makefile
@@ -0,0 +1,13 @@
+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
diff --git a/doc/developer/tutorial/hello/src/Makefile.multiple-files b/doc/developer/tutorial/hello/src/Makefile.multiple-files
deleted file mode 100644
index 0a63c0353f0e895d0bd27db61c9d2599f4e53dd8..0000000000000000000000000000000000000000
--- a/doc/developer/tutorial/hello/src/Makefile.multiple-files
+++ /dev/null
@@ -1,26 +0,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). #
-# #
-##########################################################################
-
-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
diff --git a/doc/developer/tutorial/hello/src/Makefile.single-file b/doc/developer/tutorial/hello/src/Makefile.single-file
deleted file mode 100644
index b99d50a1dce2c0cd3b11a5bb15f5b87821b6b52f..0000000000000000000000000000000000000000
--- a/doc/developer/tutorial/hello/src/Makefile.single-file
+++ /dev/null
@@ -1,26 +0,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). #
-# #
-##########################################################################
-
-FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-PLUGIN_NAME = Hello
-PLUGIN_CMO = hello_world
-include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/doc/developer/tutorial/hello/src/Makefile.test b/doc/developer/tutorial/hello/src/Makefile.test
deleted file mode 100644
index 7ff38b3f00bd36c277dd4f889afb323b8ceeec55..0000000000000000000000000000000000000000
--- a/doc/developer/tutorial/hello/src/Makefile.test
+++ /dev/null
@@ -1,27 +0,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). #
-# #
-##########################################################################
-
-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
diff --git a/doc/developer/tutorial/hello/src/Hello.ml b/doc/developer/tutorial/hello/src/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/src/Hello.ml
rename to doc/developer/tutorial/hello/src/hello.ml
diff --git a/doc/developer/tutorial/hello/v1-simple/Hello.ml b/doc/developer/tutorial/hello/v1-simple/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v1-simple/Hello.ml
rename to doc/developer/tutorial/hello/v1-simple/hello.ml
diff --git a/doc/developer/tutorial/hello/v2-register/Hello.ml b/doc/developer/tutorial/hello/v2-register/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v2-register/Hello.ml
rename to doc/developer/tutorial/hello/v2-register/hello.ml
diff --git a/doc/developer/tutorial/hello/v3-log/Hello.ml b/doc/developer/tutorial/hello/v3-log/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v3-log/Hello.ml
rename to doc/developer/tutorial/hello/v3-log/hello.ml
diff --git a/doc/developer/tutorial/hello/v4-options/Hello.ml b/doc/developer/tutorial/hello/v4-options/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v4-options/Hello.ml
rename to doc/developer/tutorial/hello/v4-options/hello.ml
diff --git a/doc/developer/tutorial/hello/v5-multiple/Hello.ml b/doc/developer/tutorial/hello/v5-multiple/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v5-multiple/Hello.ml
rename to doc/developer/tutorial/hello/v5-multiple/hello.ml
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/Hello.ml b/doc/developer/tutorial/hello/v6-test-with-bug/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v6-test-with-bug/Hello.ml
rename to doc/developer/tutorial/hello/v6-test-with-bug/hello.ml
diff --git a/doc/developer/tutorial/hello/v7-doc/Hello.ml b/doc/developer/tutorial/hello/v7-doc/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v7-doc/Hello.ml
rename to doc/developer/tutorial/hello/v7-doc/hello.ml
diff --git a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
index cff0f6c0b40a36ecdbbce989fc11c9fbdcb8c839..2177f32d1ed74cd30be3b4df901a47b3813953b9 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
@@ -1,8 +1,7 @@
method! vstmt_aux s =
let color =
if Eva.Analysis.is_computed () then
- let state = Db.Value.get_stmt_state s in
- let reachable = Db.Value.is_reachable state in
+ let reachable = Eva.Results.is_reachable s in
if reachable then "fillcolor=\"#ccffcc\" style=filled"
else "fillcolor=pink style=filled"
else ""
diff --git a/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml b/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml
index 93fa563539a71ddf353a23de59c08d7d300585c4..a40a522ff9f9b32cac9e08b8fefd8ad09dc60d90 100644
--- a/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml
+++ b/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml
@@ -3,6 +3,6 @@ module Cfg_graph_state = State_builder.Hashtbl
(Datatype.String)
(struct
let name = "Data_for_cfg.Cfg_graph_state"
- let dependencies = [ Ast.self; Db.Value.self ]
+ let dependencies = [ Ast.self; Eva.Analysis.self ]
let size = 17
end);;
diff --git a/doc/eva/gui.tex b/doc/eva/gui.tex
index 4a767a5126cf2aa4a28b7c02dec4c8388bd982d7..ce046238691930f1528a74c184e9721ee8f2ebab 100644
--- a/doc/eva/gui.tex
+++ b/doc/eva/gui.tex
@@ -10,6 +10,29 @@ presented in the blog.
% suite\footnote{The archive for version 0.3 is available at
% \href{http://loup-vaillant.fr/projects/monocypher/monocypher-0.3.tar.gz}.}.
+\begin{important}
+\textbf{Note:}
+This chapter describes the traditional, GTK-based graphical interface.
+Frama-C is switching to {\em Ivette}, a new GUI based on Electron.
+Ivette is currently under development, but it already offers most of the
+existing features for viewing \Eva{} results, and also includes some new
+features.
+
+To install Ivette, you simply need to run \texttt{\em ivette} once after
+installing Frama-C. This requires node v16 and yarn:
+\begin{itemize}
+ \item install NVM: \url{https://github.com/nvm-sh/nvm}
+ \item run \texttt{\em nvm use 16}
+ \item run \texttt{\em npm install --global yarn}
+\end{itemize}
+
+The following post from the Frama-C blog contains some useful information
+for installing \texttt{ivette} and using it to view \Eva{} results:
+\url{https://frama-c.com/2022/07/12/frama-c-25-ivette.html}
+
+The rest of this chapter concerns the ``old'' Frama-C graphical interface.
+
+\end{important}
\paragraph{A caveat.}
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 735243bcd4c2b4ad337132599d65dfb1300cb34a..803d05e89841dd02adabba3486be9e91a78385e4 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -78,7 +78,7 @@ This manual documents the \Eva{} (for \emph{Evolved Value Analysis}) plug-in of
\vspace{2cm}
The \Eva{} plug-in automatically computes sets of possible
-values for the variables of an analyzed program. \Eva{}
+values for the variables of an analyzed program. \Eva{}
warns about possible run-time errors in the analyzed program.
Lastly, synthetic information
about each analyzed function can be computed automatically from the
@@ -86,7 +86,7 @@ values provided by \Eva{}: these functionalities (input
variables, output variables, and information flow) are also documented
here. \bigskip
-The framework, the \Eva{} plug-in and the other plug-ins
+The framework, the \Eva{} plug-in and the other plug-ins
documented here are all Open Source software. They can be
downloaded from \url{http://frama-c.com/}.
\bigskip
@@ -103,18 +103,18 @@ The interactive graphical interface of Frama-C displays
a normalized version of the analyzed source code.
In this interface, the \Eva{} plug-in allows the user
to select an expression in the
-code and observe an over-approximation of the set of
-values this expression can take at run-time.
+code and observe an over-approximation of the set of
+values this expression can take at run-time.
Here is a simple C example:
\listinginputcaption{1}{\texttt{introduction.c}}{examples/introduction.c}
If either interface of Frama-C is launched with options
\lstinline|-eva introduction.c|,
-the \Eva{} plug-in is able to guarantee that at each passage through
-the \lstinline|return| statement of
+the \Eva{} plug-in is able to guarantee that at each passage through
+the \lstinline|return| statement of
function \lstinline|f|, the global variables \lstinline+y+ and
-\lstinline+z+ each contain either 1 or 3.
+\lstinline+z+ each contain either 1 or 3.
At the end of function \lstinline|main|,
it indicates that \lstinline|y|
necessarily contains 4, and the value of \lstinline|z| is again 1 or 3.
@@ -152,9 +152,9 @@ Frama-C emits warnings for constructs
that do not cause any run-time errors. These are called ``false alarms''.
On the other hand, the fact that \Eva{}
computes correct, over-approximated sets of possible values prevents it
-from remaining silent on a program that contains a run-time error. For
+from remaining silent on a program that contains a run-time error. For
instance, a particular division in the analyzed program
-is the object of a warning
+is the object of a warning
as soon as the set of possible values for the divisor
contains zero. Only
if the set of possible values computed by \Eva{}
@@ -192,7 +192,7 @@ Throughout this tutorial, we will see on a single example how to use
\begin{enumerate}
\item to get familiar with foreign code,
\item to produce documentation automatically,
-\item to search for bugs,
+\item to search for bugs,
\item to guarantee the absence of bugs.
\end{enumerate}
It is useful to stick to a single example in this tutorial, and
@@ -260,7 +260,7 @@ These proofs are made using a mathematical definition
of the function. Using static analysis for verifying that a piece
of code corresponds to the mathematical model
which was the object of the security proofs is an interesting
-topic but is outside the scope of this tutorial.
+topic but is outside the scope of this tutorial.
In this document, we will not be using \Eva{} for
verifying cryptographic properties.
@@ -271,7 +271,7 @@ compiler, to this effect. We will also use \Eva{} to look
for bugs in the implementation of Skein, and finally prove that the
functions that implement Skein may never cause a run-time error for a
general use pattern. Because of the numerous pitfalls of the C
-programming language, any amount of work at the
+programming language, any amount of work at the
mathematical level cannot exclude the possibility of problems
such as buffer overflows in the implementation.
It is a good thing to be able to rule these out with \Eva{}.
@@ -314,14 +314,14 @@ typedef struct /* 256-bit Skein hash context structure */
/* Skein APIs for (incremental) "straight hashing" */
int Skein_256_Init (Skein_256_Ctxt_t *ctx, size_t hashBitLen);
[...]
-int Skein_256_Update(Skein_256_Ctxt_t *ctx, const u08b_t *msg,
+int Skein_256_Update(Skein_256_Ctxt_t *ctx, const u08b_t *msg,
size_t msgByteCnt);
[...]
int Skein_256_Final (Skein_256_Ctxt_t *ctx, u08b_t * hashVal);
\end{listing-nonumber}
The impression we get at first glance is that the hash
-of an 80-char message containing
+of an 80-char message containing
the string ``People of Earth, your attention, please''
can be computed as simply as declaring a variable of
type \lstinline|Skein_256_Ctxt_t|, letting \lstinline|Skein_256_Init|
@@ -333,7 +333,7 @@ Let us write a C program that does just that:
In order to make the test useful, we have to print
the obtained hash value. Because the result we are interested in is
-an 8-byte number, represented as a char array of
+an 8-byte number, represented as a char array of
arbitrary characters (some of them non-printable), we cannot
use string-printing functions, hence the \lstinline|for| loop at lines 17-18.
\goodbreak
@@ -364,7 +364,7 @@ gcc *.c
\subsection{First try at an analysis using \Eva{}}
Let us now see how \Eva{} works on the same example.
-\Eva{} can be launched with the following command.
+\Eva{} can be launched with the following command.
The analysis should not take more than a few seconds:
\begin{listing-nonumber}
frama-c -eva main_1.c >log
@@ -374,7 +374,7 @@ Frama-C has its own model of the target platform (the default target is
a little-endian 64-bit platform). It also uses the host system's preprocessor.
If you want to do the analysis for a different platform than the host platform,
you need to provide Frama-C with a way to pre-process the files as they
-would be during an actual compilation.
+would be during an actual compilation.
There are analyses where the influence of host platform parameters
is not noticeable. The analysis we are embarking on is not one of them.
@@ -383,7 +383,7 @@ then analyze it with Frama-C targeting its default 64-bit platform,
the analysis will be meaningless and you won't be able to make sense of
this tutorial.
If you are using a 32-bit compiler, simply match
-Frama-C's target platform with your host header files by systematically adding
+Frama-C's target platform with your host header files by systematically adding
the option \verb|-machdep x86_32| to all commands in
this tutorial.
@@ -391,13 +391,13 @@ The ``\lstinline|>log|'' part of the command sends all
the messages emitted by Frama-C into a file named
``\lstinline|log|''. \Eva{} is verbose for a number of reasons that
will become clearer later in this tutorial.
-The best way to make sense of the information
+The best way to make sense of the information
produced by the analysis is
to send it to a log file.
-There is also a Graphical User Interface
+There is also a Graphical User Interface
for creating analysis projects and
-visualizing the results.
+visualizing the results.
Note that you cannot {\em edit} the source code in the GUI, only visualize it.
Most of the information present in the console is also available in the GUI,
but presented differently. Each interface (terminal or GUI) is better suited
@@ -425,7 +425,7 @@ lines of the log.
\subsection{Missing functions}
-Since we are trying out the library for the first time,
+Since we are trying out the library for the first time,
something else to look for in the log file is the list of functions for
which the source code is missing. \Eva{} requires
either a body or a specification for each function it analyzes.
@@ -439,7 +439,7 @@ This should match lines indicating functions that are both undefined
In our example, we obtain the following lines in the log:
\begin{logs}
-[kernel:annot:missing-spec] main_1.c:13: Warning:
+[kernel:annot:missing-spec] main_1.c:13: Warning:
Neither code nor specification for function Skein_256_Init,
generating default assigns from the prototype
[eva] using specification for function Skein_256_Init
@@ -754,7 +754,7 @@ but when it is almost done (after the analysis of function
\begin{logs}
...
[eva] using specification for function printf_va_1
-[eva:alarm] main_1.c:17: Warning:
+[eva:alarm] main_1.c:17: Warning:
accessing uninitialized left-value. assert \initialized(&hash[i]);
[eva] done for function main
...
@@ -856,7 +856,7 @@ since the beginning, and the test that we ran as our first
step failed to notice it.
The bug can be fixed by passing
-8*HASHLEN instead of HASHLEN as the second argument of
+8*HASHLEN instead of HASHLEN as the second argument of
\lstinline|Skein_256_Init|.
With this fix in place, the analysis
with \lstinline|-eva-precision 3| produces no alarms and gives the following
@@ -892,7 +892,7 @@ Meanwhile, compiling and executing the fixed test produces the result:
The analysis we have done so far is very satisfying because
it finds problems that are not detected by a C compiler or by testing.
-The results of this analysis only prove
+The results of this analysis only prove
the absence of run-time errors\footnote{and the absence
of conditions that
{\em should} be run-time errors -- like the uninitialized access already
@@ -919,7 +919,7 @@ of the call to builtin primitives such as \lstinline|Frama_C_interval|.
We therefore dispense with the final calls to \lstinline|printf|,
since \Eva{} offers simpler ways to observe intermediate
and final results. Note that we included \verb|__fc_builtin.h|, a file
-that comes from the Frama-C distribution and which
+that comes from the Frama-C distribution and which
defines \lstinline|Frama_C_interval|. Running Frama-C on this
file (without \verb|main_1.c| in the same directory, to avoid having two
definitions for \verb|main|):
@@ -946,11 +946,11 @@ input buffer \lstinline|msg| (all 80 bytes of it), and from nothing else.
During \Eva{}'s analysis, we have seen that all of the buffer \verb|hash|
was always modified in the conditions of the analysis: the reason is that
-this buffer was uninitialized before the sequence of calls,
+this buffer was uninitialized before the sequence of calls,
and guaranteed to be initialized after them.
We can get the complete list of locations that may be modified by each
-function by adding the option \verb|-out| to the other options we were
+function by adding the option \verb|-out| to the other options we were
already using. These locations are computed in a quick analysis that comes
after \Eva{}. In the results of this analysis, we find:
\begin{logs}
@@ -965,7 +965,7 @@ that we used in doing so; the output buffer for receiving the hash;
and Skein's internal state, that was indirectly modified by us when we called
the functions \lstinline|Init|, \lstinline|Update| and \lstinline|Final|.
-If we want the outputs of the sequence to appear more clearly, without the
+If we want the outputs of the sequence to appear more clearly, without the
variables we used for instrumenting, we can put it in its own function:
\begin{listing}{1}
@@ -973,7 +973,7 @@ u08b_t hash[HASHLEN];
void do_Skein_256(void)
{
- Skein_256_Ctxt_t skein_context;
+ Skein_256_Ctxt_t skein_context;
Skein_256_Init( &skein_context, HASHLEN * 8);
Skein_256_Update( &skein_context, msg, 80);
Skein_256_Final( &skein_context, hash);
@@ -989,7 +989,7 @@ void main(void)
}
\end{listing}
-Using option \verb|-out-external| in order to obtain lists of
+Using option \verb|-out-external| in order to obtain lists of
locations that exclude each function's local variables, we get:
\begin{logs}
[inout] Out (external) for function do_Skein_256:
@@ -1001,14 +1001,14 @@ mean that each of the cells of the array was overwritten: we have to
rely on the results of \Eva{} when \lstinline|hash| was a
local variable for that result. But it means that when used in
conformance with the pattern in this program, the functions do not
-accidentally modify a global variable. We can conclude from this
+accidentally modify a global variable. We can conclude from this
analysis that the functions are re-entrant as long as the concurrent
computations are being made with separate contexts and destination
buffers.
Keeping the convenient function \lstinline|do_Skein_256| for modeling the
sequence, let us now compute the functional dependencies of each function.
-Functional dependencies list, for each output location,
+Functional dependencies list, for each output location,
the input locations that influence the final contents of this output location:
\begin{shell}
frama-c -eva *.c -eva-precision 3 -deps
@@ -1035,12 +1035,12 @@ Function Skein_256_Update:
\result FROM \nothing
Function Skein_256_Final:
- hash[0..7] FROM msg[0..79]; skein_context; ctx;
+ hash[0..7] FROM msg[0..79]; skein_context; ctx;
hashVal; Skein_Swap64_ONE[bits 0 to 7] (and SELF)
skein_context.h.bCnt FROM skein_context.h.hashBitLen; ctx (and SELF)
.h.T[0] FROM skein_context.h{.hashBitLen; .bCnt; .T[0]; }; ctx
.h.T[1] FROM skein_context{.h.hashBitLen; .h.T[1]; }; ctx
- {.X[0..3]; .b[0..15]; } FROM msg[0..79]; skein_context;
+ {.X[0..3]; .b[0..15]; } FROM msg[0..79]; skein_context;
ctx; Skein_Swap64_ONE[bits 0 to 7] (and SELF)
.b[16..31] FROM skein_context.h.bCnt; ctx (and SELF)
\result FROM \nothing
@@ -1049,7 +1049,7 @@ The functional dependencies for the functions \lstinline|Init|,
\lstinline|Update| and \lstinline|Final| are quite cryptic. They refer
to fields of the struct \lstinline|skein_context|. We have not had
to look at this struct yet, but its type \lstinline|Skein_256_Ctxt_t|
-is declared in file \verb|skein.h|.
+is declared in file \verb|skein.h|.
In the results, the mention \verb|(and SELF)| means that parts of the output
location may keep their previous values. Conversely, absence of this
@@ -1062,8 +1062,8 @@ hand, the \verb|-deps| analysis does not guarantee that all cells of
\verb|hash| are over-written --- but we previously saw we
could deduce this information from \Eva{}'s results.
-Since we don't know how the functions are supposed to work,
-it is difficult to tell if these
+Since we don't know how the functions are supposed to work,
+it is difficult to tell if these
dependencies are normal or reveal a problem. Let us move on to the
functional dependencies of \lstinline|do_Skein_256|:
\begin{logs}
@@ -1080,23 +1080,23 @@ dynamically). Finding out about this variable is a good thing: it
shows that a possibility for a malicious programmer to corrupt the
implementation into hashing the same message to different digests
would be to try to change the value of \verb|Skein_Swap64_ONE| between
-computations. Checking the source code for mentions of variable
+computations. Checking the source code for mentions of variable
\lstinline|Skein_Swap64_ONE|, we can see it is used to
detect endianness and is declared \lstinline|const|. On an
MMU-equipped platform, there is little risk that this variable
-could be modified maliciously from the outside.
+could be modified maliciously from the outside.
However, this is a vivid example of how static
analysis, and especially correct analyses as provided in Frama-C, can
complement code reviews in improving trust in existing C code.
Assuming that variable \lstinline|Skein_Swap64_ONE| keeps its value, a same
-input message is guaranteed always to be hashed by this
+input message is guaranteed always to be hashed by this
sequence of calls to the same digest,
because option \verb|-deps| says that there is no other
memory location \lstinline|hash| is computed from, not even an
internal state.
-A stronger property to verify would be that the
+A stronger property to verify would be that the
sequence \lstinline|Init(...)|, \lstinline|Update(...,80)|,
\lstinline|Final(...)| computes the same hash as when the
same message is passed in two calls \lstinline|Update(...,40)|.
@@ -1113,7 +1113,7 @@ calling \lstinline|Update(...,80)| an arbitrary number of times
between \lstinline|Init| and \lstinline|Final|. The general strategy
is to modify the C analysis context we have already written in a way
such that it is evident that it captures all such sequences of calls,
-and also in a way that launched with adequate options,
+and also in a way that launched with adequate options,
\Eva{} does not emit any warning.
The latter condition is harder than the former.
@@ -1128,25 +1128,25 @@ at \url{https://frama-c.com/category/skein/}\footnote{Note that some
% This tutorial is TO BE CONTINUED.\\
% ~\\
% In the next episode, you will learn how to
-% verify the hashing of messages of all lengths, and how to use
-% other Frama-C analyses to
-% establish more interesting results about Skein-256.
-% One of the strong properties that we will verify is that
+% verify the hashing of messages of all lengths, and how to use
+% other Frama-C analyses to
+% establish more interesting results about Skein-256.
+% One of the strong properties that we will verify is that
% it is {\em platform-conforming}\footnote{The notion here is almost the same as
% that of {\em strictly conforming program} in the ``Conformance'' chapter of the
% C99 standard, but \Eva{} recognizes some widely-used constructs
-% that are not specified in the standard, as discussed in \ref{norme_pratique}}: for
+% that are not specified in the standard, as discussed in \ref{norme_pratique}}: for
% a given platform configuration,
% two sequences of calls to the Skein-256 functions, part of the same
% or of different programs, always compute the same hash for the same message.
-% If this seems unimpressive, then please consider the attacker's
-% point of view.
+% If this seems unimpressive, then please consider the attacker's
+% point of view.
% Assume for an instant that it is important for you to be able
% to make the Skein-256 functions, inserted in different contexts, compute
% different hashes for a message of your choice.
% Think of all the ways you would have, in C,
-% as a malicious developer of the library, to insert backdoors in
+% as a malicious developer of the library, to insert backdoors in
% its source code to make it fail this property.
% In the next episode, you will discover how your
% best try would have been to surreptitiously change the value of variable
@@ -1203,8 +1203,8 @@ unions or casts. A set of integers can be represented as:
represents the set that contains 2, 12, 22, 32, and 42.
\end{itemize}
-\subsubsection{A floating-point value or interval}
-A location in memory (typically a floating-point variable)
+\subsubsection{A floating-point value or interval}
+A location in memory (typically a floating-point variable)
may also contain a floating-point number
or an interval of floating-point numbers:
\begin{itemize}
@@ -1238,8 +1238,8 @@ operations over addresses, many of the variation domains provided by
the analysis may be imprecise sets of the form
$\mbox{\tt garbled mix of }\&\cbopen x_1;\ \ldots\ x_n \cbclose$.
This expression
- denotes an unknown value built from applying arithmetic operations
-to the addresses of variables $x_1$,\ldots,$x_n$ and to integers.
+ denotes an unknown value built from applying arithmetic operations
+to the addresses of variables $x_1$,\ldots,$x_n$ and to integers.
\subsubsection{Absolutely anything}
You should not observe it in practice, but sometimes the analyzer is
@@ -1263,7 +1263,7 @@ Most modern C compilation platforms unify integer values
and absolute addresses:
there is no difference between the encoding of the integer 256
and that of the address \lstinline|(char*)0x00000100|. Therefore, \Eva{}
-does not distinguish between these two values either. It is partly
+does not distinguish between these two values either. It is partly
for this reason that offsets $D$ are expressed
in bytes in domains of the form $\cbopen\cbopen \&x + D;\ \ldots\ \cbclose\cbclose$.
@@ -1356,7 +1356,7 @@ and that consequently the read memory access is not an out-of-bound access.
If it was, an alarm would be emitted, and the
analysis would go in a different direction.
-With the default target platform, the read access remains
+With the default target platform, the read access remains
within the bounds of array \lstinline|t|,
but due to the offset of six bytes,
the 32-bit word read is made of the last two bytes from \lstinline|t[0]|
@@ -1392,7 +1392,7 @@ The value returned by function \lstinline|main| is\\
\subsubsection{Well value}
When generating an initial state to start the analysis from
-(see section \ref{libentry} for details), the analyzer
+(see section \ref{libentry} for details), the analyzer
has to generate a set of
possible values for a variable with only its type for information.
Some recursive or deeply chained types may force the generated
@@ -1426,22 +1426,22 @@ the textual log. Within Frama-C's AST, they are also available ACSL predicates.
(Frama-C comes with a common specification language for all plug-ins,
called ACSL, described at \url{http://frama-c.com/acsl.html}.)
-When using the GUI version of Frama-C, proof obligations are
+When using the GUI version of Frama-C, proof obligations are
inserted in the normalized source code. With the batch version,
option \lstinline|-print| produces a version of the analyzed source code
-annotated with the proofs obligations. The companion option
-\lstinline|-ocode <file.c>| allows to specify a filename for the
+annotated with the proofs obligations. The companion option
+\lstinline|-ocode <file.c>| allows to specify a filename for the
annotated source code to be written to.
\subsubsection{Invalid memory accesses}
Whenever \Eva{} is not able to establish that
a dereferenced pointer is valid, it emits an alarm that expresses
that the pointer needs to be valid at that point. Likewise, direct
-array accesses that may be invalid are flagged.
+array accesses that may be invalid are flagged.
\listinginput{1}{examples/alarms/invalid.c}
In the above example, the analysis is not able to guarantee that
-the memory accesses \lstinline|t[i]| and \lstinline|*p| are valid,
+the memory accesses \lstinline|t[i]| and \lstinline|*p| are valid,
so it emits a proof obligation for each:
\begin{logs}
invalid.c:5: ... accessing out of bounds index. assert i < 10;
@@ -1451,14 +1451,14 @@ invalid.c:7: ... out of bounds write. assert \valid(p);
analysis is able to guarantee that this always holds.)
-The choice between these two kinds of alarms is influenced by
+The choice between these two kinds of alarms is influenced by
option \lstinline|-unsafe-arrays|, as described
page \pageref{unsafe-arrays}.
Note that line 6 or 8 in this example could be considered as
problematic in the strictest interpretation of the standard.
\Eva{} omits warnings for these two lines according
-to the attitude described in \ref{norme_pratique}. An option
+to the attitude described in \ref{norme_pratique}. An option
to warn about these lines could happen if there was demand for
this feature.
@@ -1519,10 +1519,10 @@ with option \lstinline|-warn-invalid-pointer|.
When dividing by an expression that the analysis
is not able to guarantee non-null, a proof
obligation is emitted. This obligation expresses that the divisor
-is different from zero at this point of the code.
+is different from zero at this point of the code.
In the particular case where zero is the only possible value
-for the divisor, the analysis stops the propagation of this
+for the divisor, the analysis stops the propagation of this
execution path.
If the divisor seems to be able to take non-null values,
the analyzer
@@ -1539,7 +1539,7 @@ div.c:5: ... division by zero. assert x != 0;
In the above example, there is no way for the analyzer
to guarantee that \lstinline|x*y| is not null, so it emits
an alarm at line 4. In theory, it could avoid emitting
-the alarm \lstinline|x != 0| at line 5
+the alarm \lstinline|x != 0| at line 5
because this property is a consequence of the property emitted
as an alarm at line 4. Redundant alarms happen -- even in cases
simpler than this one. Do not be surprised by them.
@@ -1547,7 +1547,7 @@ simpler than this one. Do not be surprised by them.
\subsubsection{Undefined logical shift}
Another arithmetic alarm is the alarm emitted for logical
shift operations on integers where the second operand may be
-larger than the size in bits of the first operand's type.
+larger than the size in bits of the first operand's type.
Such an operation is left undefined by the \isoc{} standard, and
indeed, processors are often built in a way that such an
operation does not produce the \lstinline|0| or \lstinline|-1|
@@ -1616,7 +1616,7 @@ range of the integer type it is converted to.
\listinginput{1}{examples/alarms/ov_float_int.c}
\begin{logs}
...
-[eva:alarm] ov_float_int.c:6: Warning: overflow in conversion from floating-point
+[eva:alarm] ov_float_int.c:6: Warning: overflow in conversion from floating-point
to integer. assert f < 2147483648;
[eva] Values at end of function main:
@@ -1679,8 +1679,8 @@ if it appears to manipulate the address of a local variable outside
of the scope of said variable. Both issues occur in the following
example:
\listinginput{1}{examples/alarms/uninitialized.c}
-\Eva{} emits alarms for lines 5
-(variable \lstinline|r| may be uninitialized)
+\Eva{} emits alarms for lines 5
+(variable \lstinline|r| may be uninitialized)
and 13 (a dangling pointer to local variable \lstinline|t| is used).
\begin{logs}
uninitialized.c:5: ... accessing uninitialized left-value. assert \initialized(&r);
@@ -1737,10 +1737,10 @@ on \texttt{\_Bool} trap representations, in which case they are handled as
correct \texttt{\_Bool} values.
\subsubsection{Undefined pointer comparison alarms}
-Proof obligations can also be emitted
+Proof obligations can also be emitted
for pointer comparisons whose results may vary
from one compilation to another, such as \lstinline|&a < &b|
-or \lstinline|&x+2 != NULL|.
+or \lstinline|&x+2 != NULL|.
These alarms do not necessarily
correspond to run-time errors, but relying on an undefined
behavior of the compiler is in general undesirable (although
@@ -1767,7 +1767,7 @@ unwanted error, and is excluded by the emission of an alarm.
The analyzer can be instructed to propagate past these undefined
pointer comparisons with
-option \lstinline|-eva-undefined-pointer-comparison-propagate-all|.
+option \lstinline|-eva-undefined-pointer-comparison-propagate-all|.
With this option, in the example program above,
the values \lstinline|0| and \lstinline|1| are considered as results
for the condition as soon as \lstinline|p| becomes an invalid address.
@@ -1784,7 +1784,7 @@ comparison have pointer type;
\item \lstinline|all|: emit an alarm in all cases, including when comparing
scalars that the analysis has inferred as possibly containing pointers.
\end{itemize}
-
+
\subsubsection{Undefined side-effects in expressions}
The C language allows compact notations for modifying a variable that
@@ -1804,9 +1804,9 @@ as long as \lstinline|*p| does not have any bits in common with
\begin{shell}
frama-c -eva se.c -unspecified-access
\end{shell}
-With option \verb|-unspecified-access|, three warnings are emitted during
+With option \verb|-unspecified-access|, three warnings are emitted during
parsing. Each of these only mean that an expression with side-effects
-will require checking after the Abstract Syntax Tree has been elaborated.
+will require checking after the Abstract Syntax Tree has been elaborated.
For instance, the first of these warnings is:
\begin{logs}
[kernel] se.c:5: Warning: Unspecified sequence with side effect:
@@ -1817,7 +1817,7 @@ For instance, the first of these warnings is:
/* y <- x tmp */
y = x + tmp;
\end{logs}
-
+
Then \Eva{} is run on the program.
In the example at hand, the analysis finds problems at lines 5 and 7.
\begin{logs}
@@ -1832,7 +1832,7 @@ For line 7, it is not able to guarantee that \lstinline|p| does not point to
\lstinline|x|, so it emits a proof obligation. Since it cannot guarantee
that \lstinline|p| always points to \lstinline|x| either, the analysis
continues. Finally, it does not warn
-for line 9, because it is able to determine that
+for line 9, because it is able to determine that
\lstinline|*q| is \lstinline|z| or \lstinline|t|,
and that the expression \lstinline|*q + x++| is well defined.
@@ -1843,8 +1843,8 @@ modifies global variables that are read by the other, different
results can be obtained depending on factors outside the programmer's
control. At this time, \Eva{} does not check if these
circumstances occur, and silently chooses an order for calling
-\lstinline|f| and \lstinline|g|. The statement
-\lstinline|y = f() + x++;|
+\lstinline|f| and \lstinline|g|. The statement
+\lstinline|y = f() + x++;|
does not emit any warning either, although it would be desirable
to do so if \lstinline|f| reads or writes into variable \lstinline|x|.
These limitations will be addressed in a future version.
@@ -1859,7 +1859,7 @@ Vaguely related to, but different from, undefined side-effects in expressions,
The programmer thought implementation-defined behavior was invoked
in the above program, using an union to type-pun between structs S and T.
Unfortunately, this program returns 1 when compiled
-with \lstinline|clang -m32|; it returns 2 when compiled
+with \lstinline|clang -m32|; it returns 2 when compiled
with \lstinline|clang -m32 -O2|,
and it returns 0 when compiled with \lstinline|gcc -m32|.
@@ -1870,13 +1870,13 @@ compiler, if we may ask such a rhetorical
question, is right? They all are, because the program is undefined.
When function \lstinline|copy()| is called from \lstinline|main()|,
the assignment \lstinline|*p = *q;| breaks
-\isoc{}'s 6.5.16.1:3 rule. This rule states that
+\isoc{}'s 6.5.16.1:3 rule. This rule states that
in an assignment from lvalue to lvalue,
the left and right lvalues must overlap either exactly or not at all.
The program breaking this rule means compilers neither have to emit
warnings (none of the above did) nor produce code that does what the
-programmer intended, whatever that was.
+programmer intended, whatever that was.
Launched on the above program, \Eva{} says:
\begin{logs}
partially overlapping lvalue assignment. assert p == q || \separated(p, q);
@@ -1893,14 +1893,14 @@ for a specific target platform and compiler.
\subsubsection{Invalid function pointer access}
When \Eva{} encounters a statement of the form \lstinline|(*e)(x);|
-and is unable to guarantee that expression \lstinline|e|
+and is unable to guarantee that expression \lstinline|e|
evaluates to a valid function address, an alarm is emitted. This includes
invalid pointers (such as \lstinline|NULL|), or pointers to a function
with an incompatible type. In the latter case, an alarm is emitted,
but \Eva{} may nevertheless proceed with the analysis
if it can give some meaning to the call. This is meant to account
for frequent misconceptions on type compatibility (e.g. \lstinline|void *|
-and \lstinline|int *| are \emph{not} compatible).
+and \lstinline|int *| are \emph{not} compatible).
\listinginput{1}{examples/alarms/valid_function.c}
@@ -1945,15 +1945,15 @@ hold whenever the end of this function is reached.
% snowball
Some messages warn that the analysis is making an operation likely
to cause loss of precision. Other messages warn the user that
-unusual circumstances have been encountered by \Eva{}.
+unusual circumstances have been encountered by \Eva{}.
In both these cases, the messages are not proof
-obligations and it is not mandatory for the user to act on them.
+obligations and it is not mandatory for the user to act on them.
They can be distinguished from proof obligations by the fact that
they do {\bf not} use the word ``assert''.
These messages
are intended to help the user trace the results of the analysis, and
-give as much information as possible in order to help
+give as much information as possible in order to help
them find when and why the analysis becomes imprecise.
These messages are only useful when it is important to analyze the application
with precision. \Eva{} remains correct even when it
@@ -2013,7 +2013,7 @@ It contains:
\begin{itemize}
\item semantic coverage metrics, with the number of functions and
- statements analyzed;
+ statements analyzed (see section \ref{coverage} for more details);
\item total number of errors and warnings, pointing out potential issues that
could jeopardize the correction of the analysis;
\item total number of alarms emitted by the analysis, grouped by kind;
@@ -2032,6 +2032,41 @@ by the Report plugin.
The summary display can be disabled by using option
\lstinline|-eva-msg-key=-summary|.
+\subsection{Analysis coverage} \label{coverage}
+
+In the \Eva{} summary, the coverage indicates the number of functions whose
+body has been \emph{analyzed} by \Eva{}, out of the total number of
+\emph{defined} functions in the files given to \FramaC.
+Declared functions with no definition are ignored, as well as functions from the
+C standard library.
+
+This differs from the semantics coverage computed by the \textsf{Metrics} plugin
+with the option \lstinline|-metrics-eva-cover| : \textsf{Metrics} counts all
+functions \emph{reached} by the \Eva{} analysis, out of the total number
+of functions (defined or not) syntactically reachable from the starting point
+of the analysis.
+Functions from the C standard library are also ignored, unless option
+\lstinline|-metrics-libc| is used.
+
+When the \Eva{} analysis reaches a function \lstinline|f|,
+its body is analyzed, unless:
+\begin{itemize}
+ \item the function specification is used instead, because:
+ \begin{itemize}
+ \item the function has no definition;
+ \item the option \lstinline|-eva-use-spec f| has been set.
+ \end{itemize}
+ \item a builtin is used: \Eva{} uses internal builtins to interpret calls to
+ some standard C library functions without analyzing their body.
+ The command \lstinline|frama-c -eva-builtins-list| prints the list of
+ available \Eva{} builtins.
+ See chapter \ref{primitives} for more details.
+\end{itemize}
+
+In these three cases, the function \lstinline|f| is reached by the analysis
+(and thus counted in the \textsf{Metrics} coverage), but not analyzed
+(and thus not counted in the \Eva{} coverage).
+
\subsection{Audit messages ({\em experimental})}
Using options \lstinline|-audit-prepare| and \lstinline|-audit-check|, the
@@ -2100,7 +2135,7 @@ sense. Consider the following code snippet:
// slice for the value of x here.
\end{listing}
-This piece of program is begging for its second line to be removed, but
+This piece of program is begging for its second line to be removed, but
if \lstinline|p| can be the \lstinline|NULL| pointer, the sliced
program behaves differently from the original: the original program
exits abruptly on most architectures, whereas the sliced version
@@ -2110,14 +2145,14 @@ It is fine to ignore alarms in this context,
but the user of a code comprehension plug-in based on \Eva{}
should study the categorization of alarms in section \ref{obligations}
with particular care.
-Because \Eva{} is more aggressive
+Because \Eva{} is more aggressive
in trying to extract precise information from the program than other
analyzers, the user is more likely to observe incorrect results if there
-is a misunderstanding between him and the tool about what assumptions
+is a misunderstanding between him and the tool about what assumptions
should be made.
Everybody agrees that accessing an invalid pointer is an unwanted behavior,
-but what about comparing two pointers with \lstinline|<=| in an undefined manner or
+but what about comparing two pointers with \lstinline|<=| in an undefined manner or
assuming that a signed overflow wraps around in 2's complement
representation? Function \lstinline|memmove|, for instance, typically does the
former when applied to two addresses with different bases.
@@ -2126,7 +2161,7 @@ Yet, currently, if there appears to be an undefined pointer comparison, \Eva{}
propagates a state that may contain only ``optimistic''
(assuming the undefined circumstances do not occur) results
for the comparison result and for the pointers.\footnote{As explained earlier, in this particular case, it is
-possible to get all possible behaviors using option
+possible to get all possible behaviors using option
\lstinline|-eva-undefined-pointer-comparison-propagate-all|.}
It is possible to take advantage of \Eva{}
@@ -2134,11 +2169,11 @@ for program comprehension, and all existing program comprehension
tools need to make assumptions about undefined behaviors. Most tools
do not tell whether they had to make assumptions or not.
\Eva{} does: each alarm, in general,
-is also an assumption. Still, as implementation progresses
+is also an assumption. Still, as implementation progresses
and \Eva{}
becomes able to extract more information from the alarms it emits,
one or several options
-to configure it either not to emit some alarms, or not
+to configure it either not to emit some alarms, or not
to make the corresponding
assumptions, will certainly become necessary. This is a consequence
of the nature of the C language, very partially defined by a standard
@@ -2149,44 +2184,65 @@ where strong hypotheses on the underlying architecture are needed.
\section{API}
-Both the user (through the GUI) or a Frama-C plug-in can
-request the evaluation,
-at a specific statement, of an lvalue (or an arbitrary expression).
-The variation domain thus obtained
-contains all the values that this lvalue or expression may
-have anytime an actual execution reaches the selected statement.
-
-In fact, from the point view of \Eva{}, the graphical interface
-that allows to observe the values of variables in the program is very much
-an ordinary Frama-C plug-in. It uses the same functions (registered
-in module \lstinline|Db.Value|) as other plug-ins that interface with
-\Eva{}.
-This API is not very well documented yet, but one early external
-plug-in author used the GUI to get a feeling of what \Eva{}
-could provide, and then used the OCaml source code of the GUI as
-a reference for obtaining this information programmatically.
-
-\subsection{\Eva{} API overview}
-
-The function \lstinline|!Db.Value.access| is one of the
-functions provided to custom plug-ins.
-It takes a program point (of type \lstinline|Cil_types.kinstr|),
-the representation of
-an lvalue (of type \lstinline|Cil_types.lval|) and returns a representation
-of the possible values for the lvalue at the program point.
-
-Another function, \lstinline|!Db.Value.lval_to_loc|, translates the
-representation of an
-lvalue into a location (of type \lstinline|Locations.location|), which
-is the analyzer's abstract representation for a place in memory.
-The location returned by this function is free of memory accesses
-or arithmetic. The provided
-program point is used for instantiating the values of variables
-that appear in expressions
-inside the lvalue (array indices, dereferenced expressions).
-Thanks to this and similar functions, a custom plug-in may
-reason entirely in terms of abstract locations, and completely
-avoid the problems of pointers and aliasing.
+After an analysis, most results inferred by \Eva{} can be examined in the
+\FramaC graphical interface (see chapter \ref{gui}), or programmatically
+accessed by another \FramaC plugin through the public \Eva{} API.
+
+For instance, both an user (through the GUI) or a developer (through the API)
+can request the evaluation of an arbitrary lvalue or expression at a given
+statement.
+The obtained result represents all the possible values that this lvalue or
+expression may have anytime an actual execution reaches the selected statement.
+
+\subsection{API overview}
+
+The \Eva{} public API is available in the file \texttt{src/plugins/eva/Eva.mli}.
+
+The function \lstinline|Analysis.compute| starts an analysis, and other
+functions of the \lstinline|Analysis| module inform about the status of the
+current analysis.
+
+The \lstinline|Results| module provides access to the analysis results.
+In particular, it allows the evaluation of the possible values of
+arbitrary lvalues or expressions at any program point.
+Such evaluation is decomposed in several steps:
+\begin{enumerate}
+\item first, a \lstinline|request| is built by stating where it should be
+ evaluated: before or after a statement, at the start of a function, etc.
+\item optionally, a request may by restricted to a given callstack;
+\item then, functions \lstinline|eval_*| evaluate a variable, an lvalue or an
+ expression;
+\item finally, functions \lstinline|as_*| convert the evaluation result to a
+ usable destination type.
+\end{enumerate}
+
+For instance, the code below evaluates the expression \lstinline|expr|
+before statement \lstinline|stmt| in callstack \lstinline|cs|. The possible
+values of \lstinline|expr| are expressed as an \emph{fval}, a representation
+of a floating-point interval. If the evaluation fails, or if the possible values
+of \lstinline|expr| cannot be represented by a floating-point interval,
+\lstinline|Fval.top| is used instead.
+\begin{ocamlcode}
+before stmt |> in_callstack cs |>
+eval_exp expr |> as_fval |> default Fval.top
+\end{ocamlcode}
+
+Other useful functions exported in the \lstinline|Results| module include:
+\begin{itemize}
+ \item \lstinline|callee|, which returns the list of functions that can be
+ called at a given call statement, which is very useful for calls through
+ function pointers.
+ \item \lstinline|callers|, which returns the list of functions from which the
+ given function can be called.
+ \item \lstinline |is_reachable|, which returns whether a given statement has
+ been reached by the analysis.
+ \item \lstinline|expr_deps|, which computes an over-approximation of the
+ memory zones that must be read to evaluate the given expression.
+\end{itemize}
+
+Other modules of the \Eva{} API allows to change some parameters of the
+analysis, to add local annotations guiding the analysis, or to register
+ocaml builtins to be used by the analysis to interpret some function calls.
The Frama-C Plug-in Development Guide contains more information about
developing a custom plug-in.
@@ -2254,14 +2310,14 @@ writable.
\subsection{Alignment of memory accesses}
-\Eva{} currently does not check that memory accesses are
+\Eva{} currently does not check that memory accesses are
properly aligned in memory. It assumes that non-aligned accesses have
only a small time penalty (instead of causing an exception) and that the
programmer is aware of this penalty and is accessing (or seems to be accessing)
memory in a misaligned way on purpose. %% A more restrictive option
%% would be quick to implement if someone needed it. Meanwhile,
%% instructions to explicitly check for the alignment of some accesses
-%% can be inserted in the code following the howto at
+%% can be inserted in the code following the howto at
%% \url{http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:explicit_alignment_howto}.
% Removed: not in open-source version
@@ -2273,7 +2329,7 @@ memory in a misaligned way on purpose. %% A more restrictive option
The analysis of a source program always takes a finite time.
The fact that the source code contains loops, and that some of these
loops do not terminate, can never induce the analyzer itself to loop forever.
-% \footnote{An exception to this rule is when one uses the most
+% \footnote{An exception to this rule is when one uses the most
% precise modeling of {\tt malloc} (details in section
% \ref{malloc}).}
In order to guarantee this property, the analyzer may need to
@@ -2286,7 +2342,7 @@ is unknown:
The \Eva{} plug-in could provide the best possible sets of values
if the user explicitly instructed it to study step by step each
-of the hundred loop iterations. Without any such instruction,
+of the hundred loop iterations. Without any such instruction,
it analyses the body of the loop much less than
one hundred times. It is able to provide the approximated, but correct,
information that after the loop, \lstinline|y| contains an even number
@@ -2431,7 +2487,7 @@ at the time of analyzing \lstinline|init2|, \Eva{} will have no reason
to believe that the global variable \lstinline|ok1| has not kept its initial value 0.
The analysis of \lstinline|init2| consists of determining
that the value of the \lstinline|if| condition is always false, and to ignore
-all the code that follows. Any possible run-time error in this function
+all the code that follows. Any possible run-time error in this function
will therefore be missed by the analyzer.
However, as long as the user is aware of these pitfalls, the analysis of
incomplete sources can provide useful results. In this example, one way
@@ -2439,7 +2495,7 @@ to analyze the function \lstinline|init2| is to use the
option \lstinline|-lib-entry| described in section \ref{libentry}.
It is also possible to use annotations to describe the state in which
-the analysis should be started as a precondition for the entry point
+the analysis should be started as a precondition for the entry point
function. The syntax and usage of preconditions is described in
section \ref{prepostasserts}. The user should pay attention to the
intrinsic limitations in the way \Eva{} interprets these
@@ -2464,13 +2520,13 @@ take into account
interrupts (auxiliary function that can be executed at any time
during the main computation). As things stand, the plug-in may give
answers that do not reflect reality if interrupts play a role
-in the behavior of the analyzed application.
+in the behavior of the analyzed application.
There is preliminary support for using \Eva{} in this
context in the form of support for \lstinline|volatile| variables.
Unlike normal variables, the analyzer does not assume that
the value read from a \lstinline|volatile|
-variable is identical to the last value written there. Instead,
+variable is identical to the last value written there. Instead,
a volatile variable in which only scalar values have been written
is assumed to contain \lstinline|[--..--]| when it is read from,
regardless of the precise value of the contents
@@ -2496,7 +2552,7 @@ on the size of the word and the endianness of the target architecture.
There exists constructs of the C language which the ISO standard does
not specify, but which are compiled in the same way by almost every compiler
-for almost every architecture. For some of these constructs, the \Eva{}
+for almost every architecture. For some of these constructs, the \Eva{}
plug-in assumes a reasonable compiler and
target architecture. This design choice makes it possible to obtain more
information about the behavior of the program than would be possible
@@ -2540,7 +2596,7 @@ between integers and pointers, pointer arithmetic, the representation
of \lstinline|enum| types and the relations between the addresses of the
fields of a same \lstinline|struct|. As a concrete example, \Eva{}
plug-in assumes two-complement representation,
-which the standard does not guarantee,
+which the standard does not guarantee,
and whose consequences can be seen when converting between
signed and unsigned types or with signed arithmetic overflows.
These parameters are all fixed with the \lstinline|-machdep| option
@@ -2680,8 +2736,8 @@ section~\ref{malloc}.
\subsubsection{Values that are valid even if something bad happens}
\Eva{} provides sets of possible values under the
assumption that the alarms emitted during the analysis have been
-verified by the user (if necessary, using other techniques).
-If during an actual execution of the application,
+verified by the user (if necessary, using other techniques).
+If during an actual execution of the application,
one of the assertions emitted by \Eva{} is violated,
values other than those predicted by \Eva{} may happen.
See also questions 2 and 3 in chapter \ref{faq}.
@@ -2703,15 +2759,15 @@ that every time execution reaches the end of \lstinline|main|, the value
of \lstinline|x| is $\geq 100$. This does
not mean that the function always terminates or even that it may
sometimes terminate (it does neither). When \Eva{}
-proposes an interval for \lstinline|x| at a point P,
-it should always be interpreted as meaning
-that {\em if P is reached, then at that time \lstinline|x| is in
+proposes an interval for \lstinline|x| at a point P,
+it should always be interpreted as meaning
+that {\em if P is reached, then at that time \lstinline|x| is in
the proposed interval}, and
not as implying that P is reached.
\subsubsection{Propagation of the displayed states}
The values available through the graphical and programmatic interfaces
-do not come from a single propagated state but from the union of
+do not come from a single propagated state but from the union of
several states that the analyzer may have propagated separately.
As a consequence, it should not be assumed that the ``state''
displayed at a particular program point has been propagated.
@@ -2728,14 +2784,14 @@ main(int c){
...
...
/* At this point Eva guarantees:
- x IN {0; 1}
+ x IN {0; 1}
y IN {0; 1}; */
z = 10 / (x - y);
}
\end{listing}
\goodbreak
-With the option \lstinline|-eva-slevel| described in section \ref{slevel},
+With the option \lstinline|-eva-slevel| described in section \ref{slevel},
the lines leading up to this situation may for instance have been:
\begin{listing}{3}
x = c ? 0 : 1;
@@ -2751,11 +2807,11 @@ propagated back to a particular call point. The only guarantee is
that the state that was propagated back to the call point is included
in the one displayed for the end of the function.
-The only way to be certain that \Eva{} has propagated
+The only way to be certain that \Eva{} has propagated
a specific state, and therefore guarantee the absence of run-time
errors under the assumptions encoded in that state, is to build
the intended state oneself, for instance with non-deterministic
-primitives (section \ref{nondeterminism}).
+primitives (section \ref{nondeterminism}).
However, the intermediate results displayed in
the GUI can and should be used for
cross-checking that the state actually built
@@ -2878,7 +2934,7 @@ including header directories.
In rare cases, you may need to use a different preprocessing command, via
option \lstinline|-cpp-command <cmd>|.
-If the patterns \lstinline|%1| and \lstinline|%2| do not appear
+If the patterns \lstinline|%1| and \lstinline|%2| do not appear
in the text of the
command, Frama-C invokes the preprocessor in the following way:
\begin{shell}
@@ -2886,7 +2942,7 @@ command, Frama-C invokes the preprocessor in the following way:
\end{shell}
In the cases where it is not possible to invoke the preprocessor with
-this syntax, it is possible to use the
+this syntax, it is possible to use the
patterns \lstinline|%1| and \lstinline|%2|
in the command's text as place-holders for the input file (respectively,
the output file). Here are some examples of use of this option:
@@ -2915,10 +2971,10 @@ parameterization.
\label{saving-result}
The option \lstinline|-save s|
-saves the state of the analyzer, after the requested
+saves the state of the analyzer, after the requested
computations have completed,
in a file named \lstinline|s|.
-The option \lstinline|-load s| loads the state saved in file \lstinline|s|
+The option \lstinline|-load s| loads the state saved in file \lstinline|s|
back into memory for visualization or further computations.
\medskip
@@ -2973,12 +3029,12 @@ as the entry point.
\label{complete}
By default (when the option \lstinline|-lib-entry| is {\em not} set),
-the analysis starts from a state
+the analysis starts from a state
in which initialized global variables
contain their initial values, and uninitialized ones contain zero.
This only makes sense if the entry point (see section \ref{entry}) is
-the actual starting point of this analyzed application.
-In the initial state, each formal argument of the entry point contains
+the actual starting point of this analyzed application.
+In the initial state, each formal argument of the entry point contains
a non-deterministic value that corresponds to its type. Representative
locations are generated for arguments with a pointer type,
and the value of the pointer argument is the union of the address
@@ -2989,7 +3045,7 @@ Example: for an application written for the POSIX interface, the
prototype of \lstinline|main| is:
\lstinputlisting[linerange={1-1}]
{examples/parametrizing/simple-main.c}
-The types of arguments \lstinline|argc| and \lstinline|argv|
+The types of arguments \lstinline|argc| and \lstinline|argv|
translate into the following initial values:
\lstinputlisting[linerange={10-16}]
{examples/parametrizing/simple-main.log}
@@ -3052,14 +3108,14 @@ can be used to tweak the generation of these values to some extent.
The option \lstinline|-lib-entry| specifies that the analyzer should not use
the initial values for globals (except for those qualified
with the keyword \lstinline|const|).
-With this option, the analysis starts with an initial state
+With this option, the analysis starts with an initial state
where the numerical components of
global variables (without the \lstinline|const| qualifier) and arguments
of the entry point are initialized with a non-deterministic value of their
respective type.
Global variables of pointer type contain the non-deterministic
-superposition of \lstinline|NULL| and of the addresses of
+superposition of \lstinline|NULL| and of the addresses of
locations allocated by the analyzer. The algorithm to generate
those is the same as for formal arguments of the entry point (see previous
section). The same options can be used to parameterize the generation of
@@ -3068,15 +3124,15 @@ the pointed locations (see next section).
\subsection{Tweaking the automatic generation of initial values}
\label{generation_initial}
-This sections describes the options that influence
+This sections describes the options that influence
the automatic generation of initial values
of variables. The concerned
-variables are the arguments of the entry point and,
+variables are the arguments of the entry point and,
in \lstinline|-lib-entry| mode, the non-const global variables.
\subsubsection{Width of the generated tree}
-For a variable of a pointer type, there is no way for the analyzer
+For a variable of a pointer type, there is no way for the analyzer
to guess whether the pointer should be assumed to be pointing to a single
element or to be pointing at the
beginning of an array --- or indeed, in the middle of an array, which
@@ -3101,30 +3157,30 @@ Example: with the default value \lstinline|2| for option
causes the following array to be allocated:
\lstinputlisting[linerange={10-15}]
{examples/parametrizing/context-width.log}
-
+
Note that for both arrays of pointers and pointers to pointers,
using option \lstinline|-eva-context-width 1| corresponds to a very strong
assumption on the contents of the initial state with respect to aliasing.
You should only use the argument \lstinline|1| for
-option \lstinline|-eva-context-width| in special cases, and use at least
+option \lstinline|-eva-context-width| in special cases, and use at least
\lstinline|2| for generic, relatively representative calling contexts.
\subsubsection{Depth of the generated tree}
For variables of a type pointer to pointers, the analyzer limits the depth up
-to which initial chained structures are generated.
+to which initial chained structures are generated.
This is necessary for recursive types such as follows.
\lstinputlisting[linerange={1-1}]
{examples/parametrizing/context-depth.c}
This limit may also be observed for non-recursive types if they are deep enough.
Option \lstinline|-eva-context-depth| allows to specify this limit.
-The default value is 2. This number is the depth at which
+The default value is 2. This number is the depth at which
additional variables named \lstinline|S_...| are allocated, so
two is plenty for most programs.
For instance, here is the initial state displayed by \Eva{}
-in \lstinline|-lib-entry| mode if a global variable \lstinline|s|
+in \lstinline|-lib-entry| mode if a global variable \lstinline|s|
has type \lstinline|struct S| defined above:
\lstinputlisting[linerange={6-13}]
{examples/parametrizing/context-depth.1.log}
@@ -3134,7 +3190,7 @@ has type \lstinline|struct S| defined above:
In this case, if variable \lstinline|s| is the only one which
is automatically allocated, it makes sense to set the option
\lstinline|-eva-context-width| to one. The value of the
-option \lstinline|-eva-context-depth| represents the length of the
+option \lstinline|-eva-context-depth| represents the length of the
linked list which is modeled with precision. After this depth,
an imprecise value (called a well) captures all the possible continuations
in a compact but imprecise form.
@@ -3145,7 +3201,7 @@ with options \lstinline|-eva-context-width 1|
\lstinputlisting[linerange={6-16}]
{examples/parametrizing/context-depth.2.log}
-
+
\subsubsection{The possibility of invalid pointers}
In all the examples above, \lstinline|NULL| was one of the
@@ -3166,7 +3222,7 @@ of those areas through user-provided assertions
The option \lstinline|-eva-context-valid-pointers| causes
those pointers to be assumed to be valid (and
-\lstinline|NULL| therefore to be omitted from the possible values)
+\lstinline|NULL| therefore to be omitted from the possible values)
at depths that are less than the context width.
It also causes the list to end with a
\lstinline|NULL| value instead of a well.
@@ -3243,9 +3299,9 @@ Currently, only programs of the first category can be soundly analyzed by
\subsubsection{Using one of the pre-configured target platforms}
-The option \lstinline|-machdep |{\it platform}
+The option \lstinline|-machdep |{\it platform}
sets a number of parameters for the low-level description of the
-target platform, including the
+target platform, including the
\emph{endianness} of the target and size of each C type.
The option \lstinline|-machdep help| provides a list of currently supported
platforms. The default is \lstinline|x86_64|, an AMD64-compatible processor with
@@ -3254,7 +3310,7 @@ what are roughly the default compilation choices of gcc.
\subsubsection{Targeting a different platform}
If your target platform is not listed,
-please contact the developers.
+please contact the developers.
An auto-detection program can be provided in order to check the hypotheses
mentioned in section~\ref{norme_pratique}, as well as to detect the
parameters of your platform.
@@ -3262,14 +3318,14 @@ It comes under the form of a C program of a few lines, which should ideally be
compiled with the same compiler as the one intended to compile the
analyzed application. If this is not possible, the analysis can also be
parameterized manually with the characteristics of the target
-architecture.
+architecture.
The Frama-C Plugin Development Guide~\cite{plugin-dev-guide} contains a
section about customizing the machine model.
\subsection{Parameterizing the modeling of the C language}
-The following options are more accurately described as
-pertaining to Frama-C's modeling of the C language
+The following options are more accurately described as
+pertaining to Frama-C's modeling of the C language
than as a description of the target platform, but of course
the distinction is not always clear-cut. The important thing to remember
is that these options, like the previous one, are dangerous options
@@ -3297,7 +3353,7 @@ in a future version.
\Eva{} assumes that when an array
access occurs in the analyzed program, the intention is that the
accessed address should be inside the array. If it can not determine that
-this is the case, it emits an \lstinline|out of bounds index|
+this is the case, it emits an \lstinline|out of bounds index|
alarm. This leads to an alarm on the following example:
\lstinputlisting[numbers=left]
{examples/parametrizing/out-of-bound.c}
@@ -3648,14 +3704,14 @@ The value proposed for the cells \lstinline|t[2][5]| and following
is imprecise but correct. The set \lstinline|{0; 1}| does
contain the actual value \lstinline|1| of the cells.
-The option \lstinline|-eva-slevel-function f:n| tells the analyzer to apply
+The option \lstinline|-eva-slevel-function f:n| tells the analyzer to apply
semantic unrolling level \lstinline|n| to function \lstinline|f|.
-This fine-tuning option allows to
+This fine-tuning option allows to
force the analyzer to invest time precisely analyzing functions that matter,
for instance \lstinline|-eva-slevel-function crucial_initialization:2000|.
-Oppositely, options \lstinline|-eva-slevel 100 -eva-slevel-function trifle:0|
-can be used together to avoid squandering resources over irrelevant parts of
-the analyzed application. The \lstinline|-eva-slevel-function| option can be used
+Oppositely, options \lstinline|-eva-slevel 100 -eva-slevel-function trifle:0|
+can be used together to avoid squandering resources over irrelevant parts of
+the analyzed application. The \lstinline|-eva-slevel-function| option can be used
several times to set the semantic unrolling level of several functions.
Overall, \lstinline|-eva-slevel| has the advantage of being quick to setup.
@@ -3820,21 +3876,21 @@ void main (int c)
In the example above, without a loop invariant, the pointer \lstinline+p+
is determined to be in the range \lstinline|&t + [4..60],0%4|. In C terms, this
% <<do not fix the above even if it is wrongly colorized by Emacs. It is right>>
-means that \lstinline+p+ points between \lstinline+&t[0]+
+means that \lstinline+p+ points between \lstinline+&t[0]+
and \lstinline+&t[15]+, inclusive. In particular, the analysis is not able
to prove that the access on line~9 is always valid.
-Thanks to the loop invariant \lstinline|p < &t[N-1]|, the variable
-\lstinline+p+ is
+Thanks to the loop invariant \lstinline|p < &t[N-1]|, the variable
+\lstinline+p+ is
instead widened to the range \lstinline+&t[0]..&t[N-2]+.
-This means that the access to \lstinline+t+
+This means that the access to \lstinline+t+
through \lstinline+p+ at line 7 occurs
within bounds\footnote{And more precisely between \lstinline+t[1]+ and
\lstinline+t[9]+, since \lstinline+p+
is incremented before the affectation to \lstinline+*p+.}.
Thus, this technique is complementary to the use of
\lstinline+WIDEN_HINTS+, which only accepts integers --- hence not
-\lstinline+&t[N-1]+. Compared to the use
+\lstinline+&t[N-1]+. Compared to the use
of \lstinline+-eva-slevel+ or \lstinline+-ulevel+,
the technique above does not unroll the loop; thus the overall results
are less precise, but the analysis can be faster.
@@ -4493,8 +4549,8 @@ int isTopBit(unsigned something)
//@ assert something >= 0x80000000 || something < 0x80000000;
unsigned topBitOnly = something & 0x80000000;
something ^= topBitOnly;
- if (something & 0x80000000) // More precision on this conditional { ... }
-}
+ if (something & 0x80000000) // More precision on this conditional { ... }
+}
\end{lstlisting}
The current analysis is fully inter-procedural. All variables (including
@@ -4533,7 +4589,7 @@ following restrictions apply to the current implementation:
number of tracked variables. Since relational domains are usually costly
(cubic complexity for octagons, exponential for polyhedra), this may result
in very long analyses and/or massive memory usage.
-
+
\end{itemize}
\subsection{Taint}
@@ -4675,8 +4731,8 @@ amount of warnings and is rarely needed in practice.
\chapter{Inputs, outputs and dependencies}\label{inoutdeps}
\vspace{2cm}
-{\em Frama-C can compute and display the inputs (memory locations read from),
-outputs (memory locations written to),
+{\em Frama-C can compute and display the inputs (memory locations read from),
+outputs (memory locations written to),
and precise dependencies between outputs and inputs,
for each function. These computations use \Eva{}
for resolving array indices and pointers.}
@@ -4811,20 +4867,20 @@ can be thus read in all terminating executions of the function,
and a superset of the locations thus read including non-terminating
executions.
-Operational inputs can for instance be used
+Operational inputs can for instance be used
to decide which variables to initialize in order to
be able to execute the function.
Both flavors of operational inputs are displayed with
the option \lstinline|-inout|, as well as a list of locations that
-are guaranteed to have been over-written when the function terminates;
+are guaranteed to have been over-written when the function terminates;
the latter is a by-product of the computation of operational
inputs that someone may find useful someday.
\listinginput{1}{examples/op_inputs.c}
This example, when analyzed with the options \lstinline|-inout -lib-entry -main op|,
-is found to have on termination the operational
-inputs \lstinline|b; c; p; S_p[0]| for function \lstinline|op|.
+is found to have on termination the operational
+inputs \lstinline|b; c; p; S_p[0]| for function \lstinline|op|.
Operational inputs for non-terminating executions add \lstinline|e|, which is
read inside an infinite loop, to this list.
@@ -4834,7 +4890,7 @@ inputs, although it is not a functional input, because it is read
The variable \lstinline|a| is not among the operational inputs because its value
has been overwritten before being read. This means that an actual
execution of the function \lstinline|op| requires to initialize \lstinline|p|
-(which influences the execution by causing, or not,
+(which influences the execution by causing, or not,
an illicit memory access), whereas on the other hand, the analyzer
guarantees that initializing \lstinline|a| is unnecessary.
@@ -4858,7 +4914,7 @@ and tips related to specific warnings, which might be useful.
\subsection{Truth value of a property}
-Each time it encounters a precondition, postcondition or user assertion,
+Each time it encounters a precondition, postcondition or user assertion,
the analyzer evaluates the truth value of the property
in the state it is propagating. The result of this evaluation can be:
\begin{itemize}
@@ -4945,7 +5001,7 @@ multiplies the number of states to propagate in the same way that
analyzing an \lstinline|if-then-else| construct does. Again, the
analyzer keeps the states separate only if the limit (the numerical
value passed to option \lstinline|-eva-slevel|) has not been reached yet
-in that point of the program.
+in that point of the program.
This treatment often improves the precision of the analysis. It can be used with tautological assertions
to provide hints to the analyzer, as shown in the following example.
@@ -4958,7 +5014,7 @@ frama-c -eva -eva-slevel 2 sq.c
The analysis finds the result
of this computation to be in \lstinline|[0..100]|. Without the
-option \lstinline|-eva-slevel 2|, or without the annotation on line 4,
+option \lstinline|-eva-slevel 2|, or without the annotation on line 4,
the result found
is \lstinline|[-100..100]|. Both are correct. The former is
optimal considering the available information and the representation
@@ -4969,8 +5025,8 @@ of large sets as intervals, whereas the latter is approximated.
Attention should be paid to the following two limitations:
\begin{itemize}
\item a precondition or assertion only adds constraints to the state, i.e. always
-makes it smaller, not larger. In particular in the case of a precondition for
-a function analyzed with option \lstinline|-lib-entry|, the precondition
+makes it smaller, not larger. In particular in the case of a precondition for
+a function analyzed with option \lstinline|-lib-entry|, the precondition
can only
reduce the generic state that the analyzer would have used had there
not been an annotation. It cannot make the state more general. For instance,
@@ -4982,7 +5038,7 @@ approximated. The state effectively used after taking the annotation
into account is a superset of
the state described by the user. In the worst case (for instance if
the formula is too complicated for the analyzer to exploit), this superset
-is the same as the original state. In this case,
+is the same as the original state. In this case,
it appears as if the annotation is
not taken into account at all.
\end{itemize}
@@ -4991,7 +5047,7 @@ not taken into account at all.
The two functions below illustrate both of these limitations:
\listinginput{1}{examples/annotations_2.c}
-If the analyzer is launched with
+If the analyzer is launched with
options \lstinline|-lib-entry -main generalization|,
the initial state generated for the analysis of function
\lstinline|generalization| contains a pointer for the variable \lstinline|a| in a separated memory region.\\
@@ -5000,10 +5056,10 @@ The precondition
expected by the user: the intention appears to be to generalize
the initial state, which is not possible.
-If the analyzer is launched with
+If the analyzer is launched with
options \lstinline|-main not_reduced|,
the result for variable \lstinline|d| is the same as if there was no
-precondition. The interval computed for the returned
+precondition. The interval computed for the returned
value, \lstinline|[--..--]|,
seems not to take the precondition into account because the analyzer
cannot represent the set of non-zero integers.
@@ -5026,7 +5082,7 @@ on all \lstinline|return| statements. Postconditions are evaluated in
succession. Given a postcondition $P$, the analyzer computes
the truth value $\mathcal{V}$ of $P$ in the state $A$. % , and
% notifies it to Frama-C's kernel, so that it may be recorded for
-% consolidation.
+% consolidation.
Then:
\begin{itemize}
\item If $\mathcal{V}$ is \lstinline|valid|, the analysis continues on
@@ -5171,15 +5227,15 @@ the real behaviors of the function.
\paragraph{Assigns clauses and derived analyses}
For the purposes of options \lstinline|-deps|, \lstinline|-input|,
-\lstinline|-out|, and \lstinline|-inout|, the \lstinline|assigns|
+\lstinline|-out|, and \lstinline|-inout|, the \lstinline|assigns|
clauses provided for
library functions are assumed to be accurate descriptions of what the
function does. For the latter three options, there is a
leap of faith in the reasoning: an \lstinline|assigns| clause only
-specifies {\em functional} outputs and inputs. As an example, the contract
+specifies {\em functional} outputs and inputs. As an example, the contract
\lstinline|assigns \nothing;| can be verified for a function that reads
global \lstinline|x| to compute a new value for global \lstinline|y|,
-before restoring \lstinline|y| to its initial value. Looking only at the
+before restoring \lstinline|y| to its initial value. Looking only at the
prototype and contract of such a function, one of the \lstinline|-input|,
\lstinline|-out|, or \lstinline|-inout| computation would mistakenly
assume that it has empty inputs and outputs.
@@ -5254,7 +5310,7 @@ int succ(int x);
it points to a constant address).
\begin{listing}{1}
- int y; int *p;
+ int y; int *p;
/*@ assigns p \from q;
ensures p == &y; */
void g(int *q);
@@ -5512,7 +5568,7 @@ int Frama_C_nondet(int a, int b);
void *Frama_C_nondet_ptr(void *a, void *b);
/* returns either a or b */
-int Frama_C_interval(int min, int max);
+int Frama_C_interval(int min, int max);
/* returns any value in the interval from min to max inclusive */
float Frama_C_float_interval(float min, float max);
@@ -5528,7 +5584,7 @@ of Frama-C, but their types and their behavior will stay the same.
Example of use of the functions introducing non-determinism:
\listinginput{1}{examples/nondet.c}
-With the command below, the obtained result for
+With the command below, the obtained result for
variable \lstinline|X| is \lstinline|[-45..150],0%3|.
\begin{shell}
frama-c -eva ex_nondet.c .../share/libc/__fc_builtin.c
@@ -5790,7 +5846,7 @@ multiple separate intervals, as if a disjunction had been written
first argument the expression on which to split, and as second
argument the maximum admissible cardinality of the result, i.e. the
maximum number of distinct abstract states that will be created.
-(See below.)
+(See below.)
\begin{table}[!ht]
\centering
\begin{tabular}{ccc}
@@ -5900,7 +5956,7 @@ For these reasons, \lstinline|-ulevel| is seldom used nowadays.
tool so that it detects those alarms?
}
-The answers to these questions are ``yes'' and ``yes''.
+The answers to these questions are ``yes'' and ``yes''.
Consider the following example:
\listinginput{1}{examples/vraie_al.c}
@@ -5928,11 +5984,11 @@ The answers to these questions are respectively ``yes'' and
automatically goes on. If the alarm is really a
false alarm, the result given in the rest of the analysis can be
considered with the same level of trust than if Frama-C had not
-displayed the false alarm. One should however keep in mind
+displayed the false alarm. One should however keep in mind
that this applies only in
the case of a false alarm. Deciding whether the first alarm is a true
or a false one is the responsibility of the user.
-This situation
+This situation
happens in the following example:
\listinginput{1}{examples/false_al.c}
@@ -5947,7 +6003,7 @@ the interval \lstinline|-100..100|, which is approximated but correct.
The alarm on line 7 is false, because the values that \lstinline|i| can
take at run-time lie in fact in the interval \lstinline|0..100|. As it
proceeds with the analysis, the plug-in detects that line 8 is safe, and
-that there is an alarm on line 9. These results must be interpreted
+that there is an alarm on line 9. These results must be interpreted
thus: assuming that the array access on line 7 was legitimate, then
line 8 is safe, and there is a threat on line 9. As a consequence, if
the user can convince themselves that the threat on line 7 is false,
@@ -5979,7 +6035,7 @@ about on line 8, but line 9 needs further investigation).
%% \end{shell}
%% \medskip
-%% Note that when using this option, the preprocessing is
+%% Note that when using this option, the preprocessing is
%% made in two passes (the first
%% pass operating on the code only, and the second operating on the
%% annotations only). For this reason, the options passed to
@@ -6006,10 +6062,10 @@ about on line 8, but line 9 needs further investigation).
Dillon Pariente has provided helpful suggestions on this document
since it was an early draft. We are especially thankful to him for
finding the courage to read it version after version.
-Patrick Baudin, Richard Bonichon,
+Patrick Baudin, Richard Bonichon,
Jochen Burghardt,
G\'eraud Canet, Lo\"\i c Correnson,
-David Delmas, Florent Kirchner, David Mentr\'e, Benjamin Monate, Anne Pacalet,
+David Delmas, Florent Kirchner, David Mentr\'e, Benjamin Monate, Anne Pacalet,
Julien Signoles provided useful comments in the process of
getting the text to where it is today.
@@ -6029,13 +6085,13 @@ getting the text to where it is today.
%\begin{tabular}{rl}
%Chapter \ref{introduction} &
% \url{http://www.flickr.com/photos/josago/2413612964/} \\
-%Chapter \ref{what} &
+%Chapter \ref{what} &
% \url{http://www.flickr.com/photos/markusschoepke/245292284/} \\
%Chapter \ref{limitations_specificities} &
% \url{http://www.flickr.com/photos/michaelclesle/79196008/} \\
%Chapter \ref{parameterizing} &
% \url{http://www.flickr.com/photos/rofi/2775145881/} \\
-%Chapter \ref{inoutdeps} &
+%Chapter \ref{inoutdeps} &
% \url{http://www.flickr.com/photos/jsome1/477100921/} \\
%Chapter \ref{annotations} &
% \url{http://www.flickr.com/photos/luchilu/459219845/} \\
@@ -6129,7 +6185,7 @@ for an example syntax when dealing with pointers to type \texttt{void}.
ACSL annotations are preprocessed by default. This means you can use
definitions such as \verb+INT_MAX+, \verb+EOF+, etc.
-For null pointers, the ACSL term \verb+\null+ can be used, notably if macro
+For null pointers, the ACSL term \verb+\null+ can be used, notably if macro
\verb+NULL+ is not available.
\section{Kinds of clauses}
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index cb6f16df585f0055b0b0148fd16f6fd2b68d9daa..879f10eef8a61904ae416523a777feb8899c448f 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -222,7 +222,6 @@ prefix=framacbook@,
stringstyle=\lp@string,%
emphstyle=\lp@ident\underbar,%
showstringspaces=false,%
- mathescape=true,%
numberstyle=\lp@number,%
xleftmargin=6ex,xrightmargin=2ex,%
framexleftmargin=1ex,%
@@ -235,7 +234,7 @@ prefix=framacbook@,
morecomment={[il]{//NOPP-LINE}},% invisible comment until end of line
morecomment={[is]{//NOPP-BEGIN}{NOPP-END\^^M}},% no space after NOPP-END
mathescape=true,
- escapechar=`
+ escapechar=`,
% breaklines is broken when using a inline and background
% breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
}
@@ -377,9 +376,12 @@ literate=%
,
style=framac-code-style,%
morekeywords={
- dune, flags, generate_opam_files, lang, libraries, name, optional, package,
- plugin, public_name, site, using
+ action, alias, as, deps, dune, executable, files, flags, from,
+ generate_opam_files, install, lang, libraries, library, name, optional,
+ package, plugin, progn, public_name, rule, section, select, site,
+ targets, using
},%
+ alsoletter=:,
morekeywords=[2]{
:standard
},
@@ -391,10 +393,18 @@ literate=%
basicstyle=\lp@inline,%
}
+\lstdefinestyle{make-basic}{%
+ language=Makefile,%
+ style=framac-code-style,%
+ basicstyle=\lp@inline,%
+}
+
\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}}{}
+\newcommand{\makeinput}[2][]{\lstinputlisting[style=make-basic,#1]{#2}}
+\lstnewenvironment{makecode}[1][]{\lstset{style=make-basic,#1}}{}
% --------------------------------------------------------------------------
\lstdefinelanguage{Why}{%
morekeywords={
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 1e16211ff66de3a704584024ed685609318314ec..a278ae6c20a0d2076a417cbbb8ff0e1e4e190e92 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -12,6 +12,8 @@ release. First we list changes of the last release.
\begin{itemize}
\item Removed Journalisation
\item \textbf{Preparing the Sources:} added option \texttt{-ast-diff}.
+\item \textbf{Setting Up Plug-ins:} removed options \texttt{-add-path} and
+ \texttt{-load-script}, and added option \texttt{-load-library}.
\end{itemize}
\section*{24.0 (Chromium)}
diff --git a/doc/userman/user-gui.tex b/doc/userman/user-gui.tex
index 14c71fe6874fc3f8ce723ea608aab81478bca714..eb00735d41fff071828ddc950aa1ca606cd75f47 100644
--- a/doc/userman/user-gui.tex
+++ b/doc/userman/user-gui.tex
@@ -142,7 +142,7 @@ The menu bar is organised as follows:
\item [The analyses menu] provides items for configuring and running plug-ins.
\begin{itemize}
-\item \texttt{Configure and run analyses}: opens the dialog box shown in
+\item \texttt{Analyses}: opens the dialog box shown in
Figure~\ref{fig:launcher}, that allows setting \FramaC parameters and
re-running analyses.
\begin{figure}[htbp!]
@@ -152,13 +152,8 @@ The menu bar is organised as follows:
\caption{The Analysis Configuration Window}
\label{fig:launcher}
\end{figure}
-\item \texttt{Compile and run an ocaml script}: allows you to run an \caml
- file as a plug-in (in a way similar to the
- option \optionuse{-}{load-script}, see Section~\ref{sec:use-plugins}).
-\item \texttt{Load and run an ocaml module}: allows you to run a
- pre-compiled \caml file as a plug-in (in a
- way similar to the option \optionuse{-}{load-module}, see
- Section~\ref{sec:use-plugins}).
+\item \texttt{Load and run an OCaml module}: allows you to load a compiled \caml
+ module as a plug-in (see Section~\ref{sec:use-plugins}).
\item Other items are plug-in specific.
\end{itemize}
diff --git a/doc/userman/user-plugins.tex b/doc/userman/user-plugins.tex
index ab30e14d280d23887b67e729811e7081ad96af2e..9332fb75b5356018dba70050719a5ad672ffda28 100644
--- a/doc/userman/user-plugins.tex
+++ b/doc/userman/user-plugins.tex
@@ -34,29 +34,23 @@ plug-in's documentation for installation instructions.
\section{Loading Plug-ins}\label{sec:use-plugins}
At launch, \FramaC loads all plug-ins in the
-directories indicated by \texttt{frama-c \optionuse{-}{print-plugin-path}} (see
-Section~\ref{sec:var-plugin}). \FramaC can locate plug-ins in additional
-directories by using the option \texttt{\optiondef{-}{add-path} <paths>}.
-To prevent this behavior, you can use option
-\optiondef{-}{no-autoload-plugins}.
+directories indicated by \texttt{frama-c \optionuse{-}{print-plugin-path}}.
+These directories contain \texttt{META} files which are used by Dune to
+automatically load these plug-ins.
-Another way to load a plug-in is to set the
-\texttt{\optiondef{-}{load-module} <files>} or
-\texttt{\optiondef{-}{load-script} <files>} options, using in both cases a
-comma-separated list of specifications, which may be one of the following:
-
-\begin{itemize}
-\item an OCaml source file (in which case it will be compiled);
-\item an OCaml object file (\texttt{.cmo} or \texttt{.cma} if running
- \FramaC in bytecode, or \texttt{.cmxs} if running \FramaC in native code);
-\item a Findlib package.
-\end{itemize}
-
-File extensions for source and object files may be omitted, e.g.
-\texttt{-load-script file} will search for \texttt{file.ml} and
-\texttt{file.cm*} (where \texttt{cm*} depends if \FramaC is running in
-bytecode or native code).
+Like other OCaml libraries, \FramaC plug-ins can be located via the environment
+variable \texttt{OCAMLPATH}\index{OCAMLPATH}. It does not need to be set by
+default, but if you install \FramaC in a non-standard directory
+(e.g. \texttt{<PREFIX>}), you may need to add directory \texttt{<PREFIX>/lib}
+to \texttt{OCAMLPATH}.
+To prevent \FramaC from automatically loading any plug-ins, you can use option
+\optiondef{-}{no-autoload-plugins}. Then the plugin to load can be selected
+using \texttt{\optiondef{-}{load-plugin} <plugin-name>} (e.g. \texttt{aorai}).
+Since \FramaC plugins are also OCaml libraries it is possible to use
+\texttt{\optiondef{-}{load-library} <library-name>}
+(e.g. \texttt{frama-c-aorai}).
+Both options accept comma-separated lists of names.
\begin{important}
In general, plug-ins must be compiled with the
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 17cad6c4aff8ab42da78674b21347c99e57cff9d..41b1326507db4fefa6c374df50ec722fcae0b611 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -195,7 +195,7 @@ export default function ASTview(): JSX.Element {
buffer.forEach((cm) => {
markers.forEach((marker) => {
const line = marker.find()?.from.line;
- if (line) cm.setGutterMarker(line, 'bullet', bullet);
+ if (line !== undefined) cm.setGutterMarker(line, 'bullet', bullet);
});
});
}
diff --git a/man/frama-c.1 b/man/frama-c.1
index 80b334ce8ed9c6a4e9899772ed0d8b77906b37bb..41610870edc30ca7238333fe02c19854a98295f0 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -1,4 +1,4 @@
-.\" Automatically generated by Pandoc 2.14.0.2
+.\" Automatically generated by Pandoc 2.14.0.3
.\"
.TH "FRAMA-C" "1" "" "2021-06-18" ""
.hy
@@ -110,10 +110,6 @@ are valid.
Bounds are parsed as OCaml integer constants.
By default, all numerical addresses are considered invalid.
.TP
--add-path \f[I]p1[,p2[\&...,pn]]\f[R]
-adds directories \f[I]p1\f[R] through \f[I]pn\f[R] to the list of
-directories in which plugins are searched.
-.TP
-add-symbolic-path \f[I]p1:n1[,p2:n2[\&...,pn:nn]]\f[R]
replaces each path \f[I]pi\f[R] with the name \f[I]ni\f[R] when
displaying file locations in messages.
@@ -136,6 +132,11 @@ This is the default.
Annotations are pre-processed by default.
Use -no-pp-annot if you don\[cq]t want to expand macros in annotations.
.TP
+[-no]-ast-diff
+computes AST differences between a loaded session (loaded with
+\f[B]-load\f[R]) and the current sources.
+These can then be used by plug-ins supporting incremental analyses.
+.TP
-autocomplete \f[I]p1,\&...,pn\f[R]
lists the options of plugins \f[I]p1,\&...,pn\f[R] in a format suitable
for autocompletion scripts.
@@ -237,7 +238,7 @@ See also \f[B]-pp-annot\f[R].
when on, load all the dynamic plugins found in the search path (see
\f[B]-print-plugin-path\f[R] for more information on the default search
path).
-Otherwise, only plugins requested by \f[B]-load-module\f[R] will be
+Otherwise, only plugins requested by \f[B]-load-plugin\f[R] will be
loaded.
Defaults to on.
.TP
@@ -360,15 +361,21 @@ starting point of the program and globals have their initial value.
-load \f[I]file\f[R]
loads the (previously saved) state contained in \f[I]file\f[R].
.TP
--load-module \f[I]SPEC\f[R]
-dynamically load OCaml plug-ins, modules and scripts.
-Each \f[I]SPEC\f[R] can be an OCaml source or object file, with or
-without extension, or a Findlib package.
-Loading order is preserved and additional dependencies can be listed in
-*\f[B].depend\f[R] files.
+-load-library \f[I]library_1,\&...,library_n\f[R]
+dynamically load libraries.
+Loading order is preserved.
+Libraries are loaded between plugins and modules.
+.TP
+-load-module \f[I]SPEC_1,\&...,SPEC_n\f[R]
+dynamically load modules.
+Each can be an object file, with or without extension, or a Findlib
+package.
+Loading order is preserved, but after plugins and libraries.
.TP
--load-script \f[I]SPEC\f[R]
-alias for option \f[B]-load-module\f[R].
+-load-plugin \f[I]plugin_1,\&...,plugin_n\f[R]
+dynamically load plugins.
+Loading order is preserved.
+Plugins are loaded before libraries and modules.
.TP
-machdep \f[I]machine\f[R]
uses \f[I]machine\f[R] as the current machine-dependent configuration
@@ -639,11 +646,6 @@ through the following variables.
FRAMAC_LIB
The directory where kernel\[cq]s compiled interfaces are installed.
.TP
-FRAMAC_PLUGIN
-The directory where Frama-C can find standard plugins.
-If you wish to have plugins in several places, use \f[B]-add-path\f[R]
-instead.
-.TP
FRAMAC_SHARE
The directory where Frama-C data (e.g.\ its version of the standard
library) is installed.
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 73b505a007498ebcd306bb1a5b051efec98349a6..f863e4bcfd64d0e0b6fa258dd0b46dfdfea32427 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -204,7 +204,7 @@ See also **-pp-annot**.
[-no]-autoload-plugins
: when on, load all the dynamic plugins found in the search path
(see **-print-plugin-path** for more information on the default search path).
-Otherwise, only plugins requested by **-load-module** will be loaded.
+Otherwise, only plugins requested by **-load-plugin** will be loaded.
Defaults to on.
-enums *repr*
@@ -308,14 +308,18 @@ the starting point of the program and globals have their initial value.
-load *file*
: loads the (previously saved) state contained in *file*.
--load-module *SPEC*
-: dynamically load OCaml plug-ins, modules and scripts. Each *SPEC* can be an
-OCaml source or object file, with or without extension, or a Findlib package.
-Loading order is preserved and additional dependencies can be listed in
-***.depend** files.
+-load-library *library_1,...,library_n*
+: dynamically load libraries. Loading order is preserved.
+ Libraries are loaded between plugins and modules.
--load-script *SPEC*
-: alias for option **-load-module**.
+-load-module *SPEC_1,...,SPEC_n*
+: dynamically load modules. Each <SPEC> can be an object file, with or without
+ extension, or a Findlib package.
+ Loading order is preserved, but after plugins and libraries.
+
+-load-plugin *plugin_1,...,plugin_n*
+: dynamically load plugins. Loading order is preserved.
+ Plugins are loaded before libraries and modules.
-machdep *machine*
: uses *machine* as the current machine-dependent configuration (size of the
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index c727f7c578c8468876beca8ae4492ef585e01a2e..0ca631c1f05375f17c32143745b609033e28194f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -799,8 +799,7 @@ let compFullName comp =
(if comp.cstruct then "struct " else "union ") ^ comp.cname
(** Different visiting actions. 'a will be instantiated with [exp], [instr],
- etc.
- @see Plugin Development Guide *)
+ etc. *)
type 'a visitAction =
SkipChildren (** Do not visit the children. Return
the node as it is. *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index a45fb58818fb1880d2fffdf7e4db4fe74d6b460c..74a8fc790377e2ebae41ab1784c9b897ea660c24 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -869,7 +869,7 @@ module LoadModule =
let module_name = "LoadModule"
let arg_name = "SPEC,..."
let help = "Dynamically load modules. \
- Each <SPEC> can be object file, with \
+ Each <SPEC> can be an object file, with \
or without extension, or a Findlib package. \
Loading order is preserved, but after plugins and libraries."
end)
@@ -882,9 +882,10 @@ module LoadLibrary =
(struct
let option_name = "-load-library"
let module_name = "LoadLibrary"
- let arg_name = "<libname,..."
+ let arg_name = "libname,..."
let help = "Dynamically load libraries. \
- Loading order is preserved, but the load is done between the plugins and the modules."
+ Loading order is preserved. Libraries are loaded between \
+ plugins and modules."
end)
let () = Parameter_customize.set_group saveload
@@ -895,9 +896,10 @@ module LoadPlugin =
(struct
let option_name = "-load-plugin"
let module_name = "LoadPlugin"
- let arg_name = "SPEC,..."
- let help = "Dynamically load plug-ins. \
- Loading order is preserved."
+ let arg_name = "plugin,..."
+ let help = "Dynamically load plugins. \
+ Loading order is preserved. Plugins are loaded before \
+ libraries and modules."
end)
let () = Parameter_customize.set_group saveload
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 4bd43c0d49b981add992c5ad131abea5a71eacf1..279fbc8ce84268630563632dd4c036b5ccaf4d49 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -330,6 +330,7 @@ let do_wpo_success ~shell ~cache goal success =
Wp_parameters.feedback ~ontty:`Silent
"[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
else
+ let gui = Frama_c_very_first.Gui_init.is_gui in
let smoke = Wpo.is_smoke_test goal in
let gstats = Stats.results ~smoke @@ Wpo.get_results goal in
let cstats = ProofEngine.consolidated goal in
@@ -338,7 +339,7 @@ let do_wpo_success ~shell ~cache goal success =
global_stats := Stats.add !global_stats gstats ;
if cstats.tactics > 0 then
script_stats := Stats.add !script_stats cstats ;
- if shell || not success then
+ if gui || shell || not success then
do_report_stats ~shell ~cache goal ~smoke cstats ;
if smoke then
begin