diff --git a/.gitignore b/.gitignore
index 3ac179231813314cf5e8107e28d6d911108d9e94..cbfdac60de1738556fd596f8fed579e441e561c6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,7 +34,6 @@
/autom4te.cache
/frama_Clang_config.ml
/*.d
-/doc
/frama-clang.tar.gz
/tests/*/result/*
/tests/basic/result/*
@@ -57,3 +56,4 @@ tempirgen
/frama-clang-*.tar.gz
_build
/tests/*/oracle/dune
+*.idx
diff --git a/doc/userman/anr-logo.png b/doc/userman/anr-logo.png
new file mode 100644
index 0000000000000000000000000000000000000000..ccdb43a8e595eff510c6d06b6ebe14aa54721efe
Binary files /dev/null and b/doc/userman/anr-logo.png differ
diff --git a/doc/userman/biblio.bib b/doc/userman/biblio.bib
index 2649298aaee526caecebd75a08b83015295ba7a0..299868e06cb7a365d0a3364d1080d36e7c991dda 100644
--- a/doc/userman/biblio.bib
+++ b/doc/userman/biblio.bib
@@ -158,3 +158,16 @@ Properties}},
author = {Kostyantyn Vorobyov and Julien Signoles and Nikolai Kosmatov},
note = {Submitted for publication},
}
+
+
+@article{baudinCACM21,
+ title = {The {Dogged} {Pursuit} of {Bug}-{Free} {C} {Programs}: {The} {Frama}-{C} {Software} {Analysis} {Platform}},
+ volume = {64},
+ url = {https://cacm.acm.org/magazines/2021/8},
+ number = {8},
+ journal = {Communications of the ACM},
+ author = {Baudin, Patrick and Bobot, François and Bühler, David and Correnson, Loïc and Kirchner, Florent and Kosmatov, Nikolai and Maroneze, André and Perrelle, Valentin and Prevosto, Virgile and Signoles, Julien and Williams, Nicky},
+ month = aug,
+ year = {2021},
+ pages = {56--68},
+}
diff --git a/doc/userman/cealistlogo.jpg b/doc/userman/cealistlogo.jpg
deleted file mode 100644
index 966be5a8ff6d50d9a7f50759633ca144c4c5db1c..0000000000000000000000000000000000000000
Binary files a/doc/userman/cealistlogo.jpg and /dev/null differ
diff --git a/doc/userman/changes.tex b/doc/userman/changes.tex
index 676ca640034597cfa7484170ddb7395a1461253e..e9631c5c10b1163b9378973729925eeb8695d317 100644
--- a/doc/userman/changes.tex
+++ b/doc/userman/changes.tex
@@ -1,11 +1,18 @@
\chapter{Changes}\label{chap:changes}
-This chapter summarizes the changes in \fclang and its documentation
+This chapter summarizes the changes in \framaclang and its documentation
between each release, with the most recent releases first.
+\section*{Version 0.0.14}
+\begin{itemize}
+\item Compatibility with \FramaC 27.x Cobalt.
+\item Compatibility with \clang 15.0 and 16.0. \clang 10.0 is not supported anymore.
+\item \framaclang has an official \opam package.
+\end{itemize}
+
\section*{Version 0.0.13}
\begin{itemize}
-\item Compatibility with \framac 25.0
+\item Compatibility with \FramaC 25.0
\item added \texttt{limits} and \texttt{ratio} headers (contributed by T-Gruber)
\end{itemize}
@@ -13,7 +20,7 @@ between each release, with the most recent releases first.
\begin{itemize}
\item compatibility with \clang 13.0 and \clang 14.0
\item \clang >= 10 is now required
-\item compatibility with \framac 24.0
+\item compatibility with \FramaC 24.0
\item support for C++14 generic lambdas (contributed by S. Gränitz)
\item option for printing reparseable code and using demangling also on non-C++ sources
\end{itemize}
@@ -21,7 +28,7 @@ between each release, with the most recent releases first.
\section*{Version 0.0.11}
\begin{itemize}
\item compatibility with \clang 12.0
-\item compatibility with \framac 23.0
+\item compatibility with \FramaC 23.0
\item Slightly improved ACSL++ parsing
\item Various bug fixes
\end{itemize}
@@ -29,7 +36,7 @@ between each release, with the most recent releases first.
\section*{Version 0.0.10}
\begin{itemize}
\item compatibility with \clang 11.x
-\item compatibility with \framac 22.x
+\item compatibility with \FramaC 22.x
\item don't generate code for implicit member functions and operators when
they're not used
\item don't generate code for templated member functions that are in fact never
@@ -39,14 +46,14 @@ between each release, with the most recent releases first.
\section*{Version 0.0.9}
\begin{itemize}
\item compatibility with \clang 10.0
-\item compatibility with \framac 21.x
+\item compatibility with \FramaC 21.x
\item support for implicit initialization of POD objects.
\end{itemize}
\section*{Version 0.0.8}
\begin{itemize}
\item compatibility with \clang 9.0
-\item compatibility with \framac 20.0
+\item compatibility with \FramaC 20.0
\item proper conversion of ghost statements
\item support for \acslpp \lstinline|\exit_status|
\item C++-part of the plug-in is now free from g++ warnings
diff --git a/doc/userman/description.tex b/doc/userman/description.tex
index baee6d463ff2f2fcef5c02eba13ec14a067c29f6..fc35459f8b0d2c85a1380298bd038183cf701d26 100644
--- a/doc/userman/description.tex
+++ b/doc/userman/description.tex
@@ -1,32 +1,34 @@
\chapter{Installation}
-\fclang is currently still experimental and not part of regular \framac releases. It must be built from source and added to a \framac installation.
-The instructions for doing so are provided at
-\url{https://frama-c.com/frama-clang.html}.
+\framaclang is currently still experimental and not part of regular \FramaC releases. It must be built from source and added to a \FramaC installation.
+If you're already using the \opam package manager to install \FramaC (see below),
+\framaclang can be installed directly with \lstinline|opam install frama-clang|.
-\fclang depends on two software packages:
+The remainder of this chapter gives the instructions for installing \framaclang manually.
+\framaclang depends on two software packages:
\begin{itemize}
-\item A current version of \framac itself. It is highly recommended to install \framac using \lstinline|opam|, as described in the installation procedures for \framac (\url{https://frama-c.com/download.html}).
-Version \fclangversion of \fclang is compatible with version \fcversion of \framac.
+\item A current version of \FramaC itself. It is highly recommended to install \FramaC using \lstinline|opam|, as described in the installation procedures for \FramaC (\url{https://frama-c.com/download.html}).
+Version \fclangversion of \framaclang is compatible with version \framacversion of \FramaC.
\item An installation of Clang, which is available as part of LLVM,
-which itself is available from \url{http://releases.llvm.org}.
-Version \fclangversion of \fclang is compatible with version \clangversion of \clang.
+which itself is available from \url{http://releases.llvm.org}. Note that you will need
+\clang's library and its headers, not just the compiler itself.
+Version \fclangversion of \framaclang is compatible with version \clangversion of \clang.
\end{itemize}
-In addition, a third package is needed for compiling \fclang,
+In addition, a third package is needed for compiling \framaclang,
\lstinline|camlp5| (\url{https://camlp5.github.io/}).
-Once \fclang has been installed, \lstinline|camlp5| is not required anymore.
+Once \framaclang has been installed, \lstinline|camlp5| is not required anymore.
Again, the easiest way to install
\lstinline|camlp5| itself is through \lstinline|opam|. Finally, newer versions
of OCaml have dropped the \lstinline|Genlex| and \lstinline|Streams| modules
from their standard library, so that another \lstinline|opam| package must be
-installed as well, namely \lstinline|camlp-streams|
+installed as well, namely \lstinline|camlp-streams|.
-Building and installing \fclang has three effects:
+Building and installing \framaclang has three effects:
\begin{itemize}
-\item The \fclang executable files are installed within
-the \framac installation.
-In particular, if \framac has been installed using \lstinline|opam|,
+\item The \framaclang executable files are installed within
+the \FramaC installation.
+In particular, if \FramaC has been installed using \lstinline|opam|,
then the principal executable \irg will be installed in the
\lstinline|opam| \lstinline|bin| directory.
You must be sure that this directory is on your \verb|$PATH|.
@@ -34,40 +36,40 @@ This is usually the default for standard \lstinline|opam| installations.
In doubt, you can try the command \lstinline|which framaCIRGen|
after installation to be sure that \irg will be correctly detected by your
shell.
-\item The \framac plug-in itself is copied into the standard \framac plug-in
+\item The \FramaC plug-in itself is copied into the standard \FramaC plug-in
directory (as given by \lstinline|frama-c-config -print-plugin-path|), so
-that it will be loaded automatically by the main \framac commands at each
+that it will be loaded automatically by the main \FramaC commands at each
execution.
-\item Include files containing \acslpp specifications of \cpp library functions
-are copied to
+\item Include files containing \acslpp specifications of \Cpp library functions
+are copied to directory
\verb|$FRAMAC_SHARE/frama-clang/libc++|, where \verb|$FRAMAC_SHARE| is the path
given by the command \lstinline|frama-c-config -print-share-path|.
\end{itemize}
These include files are replacements for (a subset of)
the standard system include files. They should have the same definitions of
-\C and \cpp functions and classes, but
+\C and \Cpp functions and classes, but
with \acslpp annotations giving their specifications. Note however that this is
still very much a work in progress, except for the headers that are imported
from the C standard library, which benefit from the specifications of the
-headers provided by \framac itself.
+headers provided by \FramaC itself.
The plugin can be built by hand from source using the following commands. Create a new directory to which you download and unpack the source distribution. Then \lstinline|cd| into the source directory itself (one level down) and execute:
\begin{listing-nonumber}
-./configure
make
make install
\end{listing-nonumber}
-By default, \fclang will install its files under the same root
-directory as \framac itself. In particular, if \framac has been
+By default, \framaclang will install its files under the same root
+directory as \FramaC itself. In particular, if \FramaC has been
installed from \lstinline|opam|, the installation will be done under
-\verb|$(opam var prefix)| directory. Standard \lstinline|autoconf|-based
-configure options for manipulating installation directories are available,
-notably \verb|--prefix|.
+\verb|$(opam var prefix)| directory. To install it in another directory,
+you can set the \lstinline|PREFIX| environment variable before executing
+\lstinline|make install|. Note that in that case, \FramaC may not be able
+to load the plug-in automatically.
%\section{Current status}
%
-%Currently on Ubuntu 17.10 and MacOSX (Sierra 10.12.6), \fclang builds in this configuration:
+%Currently on Ubuntu 17.10 and MacOSX (Sierra 10.12.6), \framaclang builds in this configuration:
%
%\begin{itemize}
%\item Install opam (>= 2.0)
@@ -85,17 +87,17 @@ notably \verb|--prefix|.
%
%
%\begin{itemize}
-%\item \fclang branch \lstinline|cok-new-parser|, framac commit \lstinline|stable/potassium|,why3 version 0.88.3, alt-ergo version 2.0.0, llvm/clang 6.0, ocaml version 4.05.0
+%\item \framaclang branch \lstinline|cok-new-parser|, framac commit \lstinline|stable/potassium|,why3 version 0.88.3, alt-ergo version 2.0.0, llvm/clang 6.0, ocaml version 4.05.0
%
-%\item \fclang branch \lstinline|cok-new-parser|, \framac branch master (commit 83b5e367ff), with why3 version 1.0
+%\item \framaclang branch \lstinline|cok-new-parser|, \FramaC branch master (commit 83b5e367ff), with why3 version 1.0
%\end{itemize}
\chapter{Running the plug-in}
-\section{\cpp files}
-Once installed the plugin is run automatically by \framac on any \cpp
-files listed on the command-line. \cpp files are identified by their
-filename suffixes. The default suffixes recognized as \cpp are these:
+\section{\Cpp files}
+Once installed the plugin is run automatically by \FramaC on any \Cpp
+files listed on the command-line. \Cpp files are identified by their
+filename suffixes. The default suffixes recognized as \Cpp are these:
\lstinline| .cpp, .C, .cxx, .ii, .ixx, .ipp, .i++, .inl, .h, .hh|
Currently this set of suffixes is compiled in the plugin (in file
@@ -104,8 +106,8 @@ recompiling and reinstalling the plugin.
\section{Frama-clang executable}
The plug-in operates by invoking the executable \irg (which must be on the system \verb|$PATH|)
-on each file identified as \cpp, in turn.
-For each file it produces a temporary output file containing an equivalent \C AST, which is then translated and passed on as input to \framac.
+on each file identified as \Cpp, in turn.
+For each file it produces a temporary output file containing an equivalent \C AST, which is then translated and passed on as input to \FramaC.
This executable is a single-file-at-a-time command-line executable only.
Various options control its behavior.
@@ -122,8 +124,8 @@ preprocessor (e.g. \lstinline|-D| macro definitions or \lstinline|-I|
search path directives). In case the project under analysis mixes C and
C++ files which
require distinct preprocessor directives, it is possible to use the
-\fclang-specific option \lstinline|-fclang-cpp-extra-args|.
-In that case, \fclang will not consider \lstinline|-cpp-extra-args| at all.
+\framaclang-specific option \lstinline|-fclang-cpp-extra-args|.
+In that case, \framaclang will not consider \lstinline|-cpp-extra-args| at all.
See section~\ref{sec:include-directories} for more information.
\item \lstinline|-machdep| which indicates the architecture on
which the program is supposed to run. See section~\ref{sec:bit} for more
@@ -131,58 +133,64 @@ information
\end{itemize}
Apart from \lstinline|-fclang-cpp-extra-args|, and
-\lstinline|-cxx-clang-command|, \fclang options governing the
+\lstinline|-cxx-clang-command|, \framaclang options governing the
parsing of C++ files are:
\begin{itemize}
-\item \lstinline|-cxx-c++stdlib-path|, the path where \fclang standard C++
+\item \lstinline|-cxx-c++stdlib-path|, the path where \framaclang standard C++
headers are located.
-\item \lstinline|-cxx-cstdlib-path|, the path where \framac standard C headers
+\item \lstinline|-cxx-cstdlib-path|, the path where \FramaC standard C headers
are located
-\item \lstinline|-cxx-nostdinc|, instructs \irg not to consider \fclang and
-\framac headers (i.e. fall back to system headers).
+\item \lstinline|-cxx-nostdinc|, instructs \irg not to consider \framaclang and
+\FramaC headers (i.e. fall back to system headers).
\end{itemize}
\section{Frama-clang options}
-The options controlling \fclang are of four sorts:
+The options controlling \framaclang are of four sorts:
\begin{itemize}
-\item options known to the \framac kernel
-\item options the \fclang plug-in has registered with the \framac kernel.
-These also are recognized by the \fc command-line.
-\item options known to \irg directly (and not to \fc), These must be
-included in the internal command that invokes \irg using the \option{-cpp-extra-args} option. These options are described in \S\ref{sec:standalone}.
-\item \clang options, which must also be supplied using the \option{-cpp-extra-args} option, and are passed through \irg to \cl. See \S\ref{sec:standalone}.
+\item options known to the \FramaC kernel
+\item options the \framaclang plug-in has registered with the \FramaC kernel.
+These also are recognized by the FramaCcommand-line.
+\item options known to \irg directly (and not to FramaC, These must be
+included in the internal command that invokes \irg using the \lstinline|-cpp-extra-args| option. These options are described in \S\ref{sec:standalone}.
+\item \clang options, which must also be supplied using the \lstinline|-cpp-extra-args| option, and are passed through \irg to \clang. See \S\ref{sec:standalone}.
\end{itemize}
-The options in the first two categories are processed by the \fc kernel when listed on the \fc command-line.
-The use of the \fc command-line is described in the core \fc
+The options in the first two categories are processed by the \FramaC kernel
+when listed on the \FramaC command-line.
+The use of the FramaCcommand-line is described in the core \FramaC
user guide.
-There are many kernel options that affect all plugins and many options specific to \fclang.
+There are many kernel options that affect all plugins and many options specific to \framaclang.
The command \\
\centerline{\lstinline|frama-c -kernel-h|} \\
shows all kernel options; the command\\
\centerline{\lstinline|frama-c -fclang-h|} \\
-shows all \fcl-specific options.
+shows all \framaclang specific options.
The most important of the options are these:
\begin{itemize}
-\item \option{--help} or \option{-h} -- introduction to \framac help
- \item \option{-kernel-h}, \option{-fclang-h} -- help information about \fc, the \fc kernel and the \fcl plug-in
- \item \option{-print} -- prints out the input file seen by \fc; when \fcl is being used this is the input file after pre-processing and translation from \cpp to \C. Thus this output can be useful to see (and debug) the results of \fcl's transformations.
- \item \option{-kernel-warn-key=annot-error=<val>} sets the behavior of \framac, including \fclang, when a parsing error is encountered. The default value (set by the kernel) is \texttt{abort}, which terminates processing upon the first error; a more useful alternative is \texttt{active}, which reports errors but continues processing further annotations.
- \item \option{-machdep <arg>} -- sets the target machine architecture, cf. \S\ref{sec:bit}
- \item \option{-kernel-msg-key <categories>} -- sets the amount of informational messages according to different categories of messages.
+\item \lstinline|--help| or \lstinline|-h| -- introduction to \FramaC help
+ \item \lstinline|-kernel-h|, \lstinline|-fclang-h| -- help information about FramaC the FramaCkernel and the \framaclang plug-in
+ \item \lstinline|-print| -- prints out the input file seen by FramaC when
+ \framaclang is being used this is the input file after pre-processing and
+ translation from \Cpp to \C. Thus this output can be useful to see (and debug)
+ the results of \framaclang's transformations.
+ \item \lstinline|-kernel-warn-key=annot-error=<val>| sets the behavior of \FramaC, including \framaclang, when a parsing error is encountered. The default value (set by the kernel) is \texttt{abort}, which terminates processing upon the first error; a more useful alternative is \texttt{active}, which reports errors but continues processing further annotations.
+ \item \lstinline|-machdep <arg>| -- sets the target machine architecture, cf. \S\ref{sec:bit}
+ \item \lstinline|-kernel-msg-key <categories>| -- sets the amount of informational messages according to different categories of messages.
See \lstinline|-kernel-msg-key help| for a list of informational categories.
- \item \option{-kernel-warn-key <categories>} -- sets the amount and behavior of warnings.\\ See \lstinline|-kernel-warn-key help| for a list of warning categories.
- \item \option{-fclang-msg-key <categories>} -- sets the amount of informational messages according to different categories of messages.
+ \item \lstinline|-kernel-warn-key <categories>| -- sets the amount and behavior of warnings.\\ See \lstinline|-kernel-warn-key help| for a list of warning categories.
+ \item \lstinline|-fclang-msg-key <categories>| -- sets the amount of informational messages according to different categories of messages.
See \lstinline|-fclang-msg-key help| for a list of informational categories.
- \item \option{-fclang-warn-key <categories>} -- sets the amount and behavior of warnings.\\ See \lstinline|-fclang-warn-key help| for a list of warning categories.
- \item \option{-fclang-verbose <n>} -- sets the amount of information from the \fclang plug-in
- \item \option{-fclang-debug <n>} -- sets the amount of debug information from the \fclang plug-in
- \item \option{-annot} -- enables processing \acslpp annotations (enabled by default)
- \item \option{-no-annot} -- disables processing \acslpp annotations
- \item \option{-cxx-unmangling <key>} indicates how mangled C++ symbols will be displayed
- by Frama-C pretty-printing. \texttt{key} can be one of:
+ \item \lstinline|-fclang-warn-key <categories>| -- sets the amount and behavior of warnings.\\ See \lstinline|-fclang-warn-key help| for a list of warning categories.
+ \item \lstinline|-fclang-verbose <n>| -- sets the amount of information
+ from the \framaclang plug-in
+ \item \lstinline|-fclang-debug <n>| -- sets the amount of debug
+ information from the \framaclang plug-in
+ \item \lstinline|-annot| -- enables processing \acslpp annotations (enabled by default)
+ \item \lstinline|-no-annot| -- disables processing \acslpp annotations
+ \item \lstinline|-cxx-unmangling <key>| indicates how mangled C++ symbols will be displayed
+ by \FramaC pretty-printing. \texttt{key} can be one of:
\begin{itemize}
\item \texttt{help}: outputs the list of existing \texttt{key} with a short description
\item \texttt{fully-qualified}: each symbol is displayed with its fully-qualified
@@ -192,26 +200,28 @@ See \lstinline|-fclang-msg-key help| for a list of informational categories.
\item \texttt{none}: no demangling is performed, symbols are displayed as seen in
the AST
\end{itemize}
- \item \option{-cxx-parseable-output} indicates that the pretty-printed code resulting
- from the translation should be able to be parsed again by Frama-C. This implies
+ \item \lstinline|-cxx-parseable-output| indicates that the pretty-printed code resulting
+ from the translation should be able to be parsed again by \FramaC. This implies
\lstinline|-cxx-unmangling none|.
\end{itemize}
-Note that the \framac option \verb|-no-pp-annot| is ignored by \fclang. Preprocessing is always performed on the source input (unless annotations are ignored entirely using \verb|-no-annot|).
+Note that the \FramaC option \verb|-no-pp-annot| is ignored by \framaclang. Preprocessing is always performed on the source input (unless annotations are ignored entirely using \verb|-no-annot|).
\section{Include directories}\label{sec:include-directories}
-By default \irg is given the paths to the two directories containing the \fcl and \fc header files, which include \acslpp specifications for the \cpp library functions. The default paths (\verb|$FRAMAC_SHARE/libc++| and
-\verb|$FRAMAC_SHARE/libc| respectively) to these directories
-can be overriden by the \fcl options \lstinline|-cxx-c++stdlib-path| and\\
+By default \irg is given the paths to the two directories containing the
+\framaclang and \FramaC header files, which include \acslpp specifications for the \Cpp library functions. The default paths (namely \verb|$FRAMAC_SHARE/libc++| and
+\verb|$FRAMAC_SHARE/libc|) to these directories
+can be overriden by the \framaclang options \lstinline|-cxx-c++stdlib-path| and
\lstinline|-cxx-cstdlib-path| options.
-Users typically have additional header files for their own projects. These are supplied to the \fcl preprocessor using the option \lstinline|-cpp-extra-args|.
+Users typically have additional header files for their own projects.
+These are supplied to the \framaclang preprocessor using the option \lstinline|-cpp-extra-args|.
You can use \lstinline|-fclang-cpp-extra-args| instead of \lstinline|cpp-extra-args|; multiple such options also have a cumulative effect.
-The \fcl option only affects the \fcl plugin, whereas
+The \framaclang option only affects the \framaclang plugin, whereas
\lstinline|-cpp-extra-args| may be seen by other plugins as well, if such plugins do their own preprocessing. Also note that the presence of any instance of \lstinline|-fclang-cpp-extra-args| will cause uses of \lstinline|-cpp-extra-args| to be ignored.
-The system header files supplied by \fcl does not include all \cpp system files. Omissions should be reported to the \fc team.
+The system header files supplied by \framaclang does not include all \Cpp system files. Omissions should be reported to the \FramaC team.
As an example, to perform \lstinline|wp| checking of files \lstinline|a.cpp| and \lstinline|inc/a.h|, one might use the command-line \\
\centerline{\texttt{frama-c -cpp-extra-args="-Iinc" -wp a.cpp}}
@@ -220,22 +230,26 @@ As an example, to perform \lstinline|wp| checking of files \lstinline|a.cpp| and
\label{sec:bit}
\acslpp is for the most part machine-independent.
-There are some features of \cpp that can be environment-dependent, such as the sizes of fundamental datatypes.
-Consequently, \framac has some options that allow the user to state what machine target is intended.
+There are some features of \Cpp that can be environment-dependent, such as the sizes of fundamental datatypes.
+Consequently, \FramaC has some options that allow the user to state what machine target is intended.
\begin{itemize}
-\item The \option{-machdep} option to \framac. See the allowed values using the command\\
+\item The \lstinline|-machdep| option to \FramaC. See the allowed values using the command\\
\centerline{ \lstinline|frama-c -machdep help|.}
- For example, with a value of \lstinline|x86_32|, \lstinline|sizeof(long)| has a value of 4, whereas with the option \option{-machdep x86\_64}, \lstinline|sizeof(long)| has a value of 8.
-%%\item Alternately, the value of \option{-machdep} can be set instead using an environment variable: \lstinline|__FC_MACHDEP|. The variable can be set either in the shell environment or on the command line with \lstinline|-D__FC_MACHDEP=...|
+ For example, with a value of \lstinline|x86_32|, \lstinline|sizeof(long)| has a value of 4, whereas with the option \lstinline|-machdep x86_64|, \lstinline|sizeof(long)| has a value of 8.
+%%\item Alternately, the value of \lstinline|-machdep| can be set instead using an environment variable: \lstinline|__FC_MACHDEP|. The variable can be set either in the shell environment or on the command line with \lstinline|-D__FC_MACHDEP=...|
\end{itemize}
\section{Warnings, errors, and informational output}
-Output messages arise from multiple places: from the \fcl plugin, from the \irg lexer and parser, from the \clang parser, and from the \framac kernel (as well as from any other plugins that may be invoked, such as the \texttt{wp} plug-in).
-They are controlled by a number of options within the \framac kernel and each plugin. Remember that \cl and \irg options must be put in the \lstinline|-cpp-extra-args| option.
+Output messages arise from multiple places: from the \framaclang plugin,
+from the \irg lexer and parser, from the \clang parser, and from the
+ \FramaC kernel (as well as from any other plugins that may be invoked, such as
+the \texttt{wp} plug-in).
+They are controlled by a number of options within the \FramaC kernel and each plugin.
+Remember that \clang and \irg options must be put in the \lstinline|-cpp-extra-args| option.
Output messages, including errors, are written to standard out, not to standard error.
@@ -245,50 +259,53 @@ Error messages are always output.
The key question is whether processing stops or continues upon encountering an error.
Continuing can result in a cascade of unhelpful error messages, but stopping immediately can hide errors that occur later in source files.
\begin{itemize}
-\item \lstinline|--stop-annot-error| is a \irg option that causes prompt termination on annotations errors (the \irg default is to continue); this does not respond to errors in C++ code
-\item \lstinline|-kernel-warn-key=annot-error=abort| is a \fcl plug-in option that will invoke \irg with \lstinline|--stop-annot-error|. \lstinline|error| and \lstinline|error_once| (instead of \lstinline|abort|) have the same effect; other values for the key will allow continuing after errors. The default is \texttt{abort}.
+\item \lstinline|--stop-annot-error| is a \irg option that causes prompt termination on annotations errors (the \irg default is to continue); this does not respond to errors in \Cpp code
+\item \lstinline|-kernel-warn-key=annot-error=abort| is a \framaclang plug-in option that will invoke \irg with \lstinline|--stop-annot-error|. \lstinline|error| and \lstinline|error_once| (instead of \lstinline|abort|) have the same effect; other values for the key will allow continuing after errors. The default is \texttt{abort}.
\end{itemize}
\subsection{Warnings}
-%The various categories of warnings from \fcl can be seen with the command \\ \centerline{\lstinline|frama-c -fclang-warn-key help|}
+%The various categories of warnings from \framaclang can be seen with the
+%command \\ \centerline{\lstinline|frama-c -fclang-warn-key help|}
%Warning messages are emitted by default.
Warning messages from \irg can be controlled with the \lstinline|-warn| option of \irg.
% Note in the current version
-%, or, equivalently, the \lstinline|-fclang-warn-key=parse| option of \fc.
+%, or, equivalently, the \lstinline|-fclang-warn-key=parse| option of FramaC
\begin{itemize}
\item \lstinline|-Werror| is a clang and \irg option that causes any parser warnings to be treated as errors
\item \lstinline|-w| is a clang and \irg option that causes any parser warnings to be ignored
\end{itemize}
-\textit{The \clang options are not currently integrated with the \fc warning and error key system.}
+\textit{The \clang options are not currently integrated with the \FramaC
+ warning and error key system.}
\subsection{Informational output}
\textit{This section is not yet written}
-\textit{The clang informational output is not currently integrated with the \fc warning and error key system.}
+\textit{The \clang informational output is not currently integrated with the
+ \FramaC warning and error key system.}
-\chapter{Running the \fclang front-end standalone}
+\chapter{Running the \framaclang front-end standalone}
\label{sec:standalone}
-In normal use within \framac, the \irg executable is
+In normal use within \FramaC, the \irg executable is
invoked automatically. However, it can also be run standalone.
In this mode it accepts command-line options and a single input file;
-it produces a C AST representing the translated \cpp, in a text format similar to Cabs.
+it produces a C AST representing the translated \Cpp, in a text format similar to Cabs.
The exit code from \irg is
\begin{itemize}
\item 0 if processing is successful, including if only warnings or informational messages are emitted
-\item 0 if there are some non-fatal errors but \option{--no-exit-code} is enabled (the default)
-\item 1 if there are some non-fatal errors but \option{--exit-code} is enabled, or if there are warnings and \lstinline|-Werror| is enabled, but \lstinline|-w| is not.
+\item 0 if there are some non-fatal errors but \lstinline|--no-exit-code| is enabled (the default)
+\item 1 if there are some non-fatal errors but \lstinline|--exit-code| is enabled, or if there are warnings and \lstinline|-Werror| is enabled, but \lstinline|-w| is not.
\item 2 if there are fatal errors
\end{itemize}
Fatal errors are those resulting from misconfiguration of the system; non-fatal errors are the result of errors in the user input (e.g. parsing errors).
-The \option{-Werror} option causes warnings to be treated as errors.
+The \lstinline|-Werror| option causes warnings to be treated as errors.
All output is sent to the standard output.\footnote{Currently clang output goes to std err.}
@@ -297,62 +314,63 @@ All output is sent to the standard output.\footnote{Currently clang output goes
These options are specific to \irg.
\begin{itemize}
- \item \option{-h} -- print help information
- \item \option{-help} -- print more help information
- \item \option{-{-}version} -- print version information
- \item \option{-o <file>} -- specifies the name and location of the output file (that is, the file to contain the generated AST). The output path may be absolute or relative to the current working directory. \textit{This option is required.}
- \item \option{-v} -- verbose output
- \item \option{-{-}stop-annot-error} -- if set, then parsing stops on the first error; default is off
+ \item \lstinline|-h| -- print help information
+ \item \lstinline|-help| -- print more help information
+ \item \lstinline|-{-}version| -- print version information
+ \item \lstinline|-o <file>| -- specifies the name and location of the output file (that is, the file to contain the generated AST). The output path may be absolute or relative to the current working directory. \textit{This option is required.}
+ \item \lstinline|-v| -- verbose output
+ \item \lstinline|-{-}stop-annot-error| -- if set, then parsing stops on the first error; default is off
\end{itemize}
\section{Clang options}
-Frama-Clang is built on the \clang \cpp parser.
+Frama-Clang is built on the \clang \Cpp parser.
As such, the \irg executable accepts the clang
compiler options and passes them on to clang. There are many of these.
-Many of these are irrelevant to \fcl as they relate to
-code generation, whereas \fcl only uses \clang for parsing, name
+Many of these are irrelevant to \framaclang as they relate to
+code generation, whereas \framaclang only uses \clang for parsing, name
and type resolution, and producing the AST.
You can see a list of options by running
\lstinline|framaCIRGen -help|
-The most significant \cl options are these:
+The most significant \clang options are these:
\begin{itemize}
- \item \option{-I <dir>} -- adds a directory to the include file search path. Using absolute paths is recommended; relative paths are relative to the current working directory.
- \item \option{-w} -- suppress clang warnings
- \item \option{-Werror} -- treat warnings as errors
+ \item \lstinline|-I <dir>| -- adds a directory to the include file search path. Using absolute paths is recommended; relative paths are relative to the current working directory.
+ \item \lstinline|-w| -- suppress clang warnings
+ \item \lstinline|-Werror| -- treat warnings as errors
\end{itemize}
-Although \clang can process languages other than \cpp, \cpp is the only one usable with \fclang.
+Although \clang can process languages other than \Cpp, \Cpp is the only one usable with \framaclang.
\section{Default command-line}
-The launching of \irg by \framac includes the following options by default. The \fc option \lstinline|-fclang-msg-key=clang| will show (among other information) the internal command-line being invoked.
+The launching of \irg by \FramaC includes the following options by default. The FramaCoption \lstinline|-fclang-msg-key=clang| will show (among other information) the internal command-line being invoked.
\begin{itemize}
\item \verb|-target <target>| with the target being set according to
the \lstinline|-machdep| and \lstinline|-target| options given to
- \framac (cf. \S\ref{sec:bit})
+ \FramaC (cf. \S\ref{sec:bit})
\item \verb|-D__FC_MACHDEP_86_32| -- also set according to the chosen
architecture. The corresponding \verb|__FC_MACHDEP_*| macro is used in
- \framac- and \fcl- provided standard headers for architecture-specific
+ \FramaC- and \framaclang provided standard headers for architecture-specific
features.
\item \verb|-std=c++11| -- target C++11 features
-\item \verb|-nostdinc| -- use \fcl and \framac system header files, and not the compiler's own header files
-\item \verb|-I$FRAMAC_SHARE/frama-clangs/libc++ -I$FRAMAC_SHARE/libc| -- include the \fclang and \framac header files, which contain system library definitions with \acslpp annotations (the paths used are controlled by the \fc options \lstinline|-cxx-c++stdlib-path| and \lstinline|-cxx-cstdlib-path|).
-\item \verb|--annot| or \verb|--no-annot| according to the \verb|-annot| or \verb|-no-annot| \framac kernel option
-\item \verb|-stop-annot-error| if the corresponding option (\lstinline|-fclang-warn-key=annot-error=abort|) is given to \framac
-\item options to set the level of info messages and warning messages, based on options on the \fc command-line
+\item \verb|-nostdinc| -- use \framaclang and \FramaC system header files, and not the compiler's own header files
+\item \verb|-I$FRAMAC_SHARE/frama-clangs/libc++ -I$FRAMAC_SHARE/libc| -- include the \framaclang and \FramaC header files, which contain system library definitions with \acslpp annotations (the paths used are controlled by the FramaCoptions \lstinline|-cxx-c++stdlib-path| and \lstinline|-cxx-cstdlib-path|).
+\item \verb|--annot| or \verb|--no-annot| according to the \verb|-annot| or \verb|-no-annot| \FramaC kernel option
+\item \verb|-stop-annot-error| if the corresponding option (\lstinline|-fclang-warn-key=annot-error=abort|) is given to \FramaC
+\item options to set the level of info messages and warning messages,
+ based on options on the \FramaC command-line
\end{itemize}
%\section{Custom ASTs}
%\lstset{keepspaces=true}
-%In standard mode, \framac invokes \irg on a file, producing an AST in intermediate format, and the reads that intermediate file into \framac to complete the processing.
+%In standard mode, \FramaC invokes \irg on a file, producing an AST in intermediate format, and the reads that intermediate file into \FramaC to complete the processing.
%If some manipulation of the AST intermediate is needed, those two steps can be performed separately as follows:
%\begin{itemize}
%\item Produce an intermediate AST \lstinline|f.ast| for a given input file \lstinline|f.cpp| using the command \\
%\centerline{\lstinline|framaCIRGen <options> -o f.ast f.cpp|}
%\item Manipulate \lstinline|f.ast| as desired.
-%\item Run \framac on the AST using the command \\
+%\item Run \FramaC on the AST using the command \\
%\centerline{\lstinline|frama-c <options> -cpp-command "cat f.ast" f.cpp|}
%\end{itemize}
%
diff --git a/doc/userman/eu-flag.jpg b/doc/userman/eu-flag.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..d59420b9cdcd1ff44ef33c9860fb93f068e5ebd5
Binary files /dev/null and b/doc/userman/eu-flag.jpg differ
diff --git a/doc/userman/fclangversion.tex b/doc/userman/fclangversion.tex
index 60e61946457d91aa96686f6b83856a7860dc269e..4bb60c8ac12f96cdfe3730f6714ccc1147372b9a 100644
--- a/doc/userman/fclangversion.tex
+++ b/doc/userman/fclangversion.tex
@@ -1,4 +1,4 @@
-\newcommand{\version}{0.0.13\xspace}
-\newcommand{\fclangversion}{0.0.13\xspace}
-\newcommand{\fcversion}{25.0~Manganese\xspace}
-\newcommand{\clangversion}{10.0-14.0\xspace}
+\newcommand{\version}{0.0.14\xspace}
+\newcommand{\fclangversion}{0.0.14\xspace}
+\newcommand{\framacversion}{27.x~Cobalt\xspace}
+\newcommand{\clangversion}{11.0-16.0\xspace}
diff --git a/doc/userman/frama-c-book.cls b/doc/userman/frama-c-book.cls
index e2d476f9ae44f43b4c17f7d5099d33bb1fd0be9e..305ef01afb2165e01d1a5edfcd57dc28a998c22d 100644
--- a/doc/userman/frama-c-book.cls
+++ b/doc/userman/frama-c-book.cls
@@ -1,135 +1,289 @@
-% --------------------------------------------------------------------------
-% --- LaTeX Class for Frama-C Books ---
-% --------------------------------------------------------------------------
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
-\newif\ifusecc
-\usecctrue
-% --------------------------------------------------------------------------
-% --- Base Class management ---
-% --------------------------------------------------------------------------
-\makeatletter
+\ProvidesClass{frama-c-book}
+\LoadClass[a4paper]{report}
+
\RequirePackage{kvoptions}
\SetupKeyvalOptions{
-family=framacbook,
-prefix=framacbook@,
+ family=framacbook,
+ prefix=framacbook@,
}
-\RequirePackage{ifthen}
-\DeclareVoidOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
-\DeclareVoidOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
-\DeclareStringOption[{type=CC,version=4.0,modifier=by-sa}]{license}
\DeclareStringOption[english]{lang}
-\DeclareDefaultOption{\PassOptionsToClass{\CurrentOption}{report}}
-\PassOptionsToClass{a4paper,11pt,twoside,openright}{report}
-
\ProcessKeyvalOptions*
-\LoadClass{report}
-
\PassOptionsToPackage{\framacbook@lang}{babel}
-\ifthenelse{\equal{\framacbook@license}{no}}{\useccfalse}{}
-\ifusecc
- \PassOptionsToPackage{\framacbook@license}{doclicense}
-\fi
\RequirePackage{babel}
-\RequirePackage{fullpage}
+
+\RequirePackage[
+ left=.125\paperwidth,
+ right=.125\paperwidth,
+ top=.125\paperheight,
+ bottom=.125\paperheight
+]{geometry}
+\RequirePackage[dvipsnames,table]{xcolor}
+\RequirePackage{graphicx}
+\RequirePackage{xspace}
+\RequirePackage{anyfontsize}
+\RequirePackage{titletoc}
+\RequirePackage{titlesec}
+\RequirePackage[shortlabels]{enumitem}
+\RequirePackage{fancyhdr}
\RequirePackage{lmodern}
+\RequirePackage{microtype}
+\RequirePackage{etoolbox}
+
+\RequirePackage{tikz}
+\usetikzlibrary{fadings}
+
+% Do I keep it there:
+
\RequirePackage[T1]{fontenc}
\RequirePackage[utf8]{inputenc}
\RequirePackage{amssymb}
-\RequirePackage[table]{xcolor}
-\RequirePackage[pdftex]{graphicx}
-\RequirePackage{ifthen}
-\RequirePackage{xspace}
-\RequirePackage{makeidx}
-\RequirePackage[leftbars]{changebar}
-\RequirePackage{fancyhdr}
-\RequirePackage{titlesec}
-\RequirePackage{upquote}
-\RequirePackage[pdftex,pdfstartview=FitH]{hyperref}
-\ifusecc\RequirePackage{doclicense}\else\fi
-% --------------------------------------------------------------------------
-% --- Page Layout ---
-% --------------------------------------------------------------------------
-\setlength{\voffset}{-6mm}
-\setlength{\headsep}{8mm}
-\setlength{\footskip}{21mm}
-\setlength{\textheight}{238mm}
-\setlength{\topmargin}{0mm}
-\setlength{\textwidth}{155mm}
-\setlength{\oddsidemargin}{2mm}
-\setlength{\evensidemargin}{-2mm}
-\setlength{\changebarsep}{0.5cm}
-\setlength{\headheight}{13.6pt}
-\def\put@bg(#1,#2,#3)#4{\setlength\unitlength{1cm}%
- \begin{picture}(0,0)(#1,#2)
- \put(0,0){\includegraphics[width=#3cm]{#4}}
- \end{picture}}
-\fancypagestyle{plain}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
- \fancyhead[CE]{\scriptsize\textsf{\leftmark}}
- \fancyhead[CO]{\scriptsize\textsf{\rightmark}}
- \fancyfoot[C]{\small\textsf{\thepage}}
- \renewcommand{\headrulewidth}{0pt}
- \renewcommand{\footrulewidth}{0pt}
-}
-\fancypagestyle{blank}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
-}
-%% Redefinition of cleardoublepage for empty page being blank
-\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
-\hbox{}
-\thispagestyle{#1}
-\newpage
-\fi\fi}
-\def\cleardoublepage{\cleardoublepagewith{blank}}
-\pagestyle{plain}
-
-% --------------------------------------------------------------------------
-% --- Cover Page ---
-% --------------------------------------------------------------------------
-\newcommand{\coverpage}[1]{%
-\thispagestyle{empty}
-\setlength\unitlength{1cm}
-\begin{picture}(0,0)(3.27,26.75)
-\put(0.58,0.70){\includegraphics[width=20.9cm]{frama-c-cover.pdf}}
-\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
-\end{picture}
-}
-
-% --------------------------------------------------------------------------
-% --- Title Page ---
-% --------------------------------------------------------------------------
-\renewenvironment{titlepage}%
-{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
-{\end{center}}
-\renewcommand{\title}[2]{
-\vspace{20mm}
-{\Huge\bfseries #1}
-
-\bigskip
-
-{\LARGE #2}
-\vspace{20mm}
-}
-\renewcommand{\author}[1]{
-\vspace{20mm}
-
-{#1}
-
-\medskip
-\ifusecc\doclicenseThis\else\fi
+\RequirePackage{comment}
+
+
+\definecolor{frama-c-orange}{HTML}{F36521}
+\definecolor{frama-c-dark-orange}{HTML}{D04604}
+\definecolor{frama-c-dark-red}{HTML}{D00404}
+\definecolor{frama-c-bronze}{HTML}{F39D21}
+\definecolor{frama-c-green}{HTML}{16A371}
+\definecolor{frama-c-dark-green}{HTML}{0E6647}
+
+\RequirePackage[
+ pdftex,pdfstartview=FitH,
+ bookmarks=true,
+ hyperindex=true,
+ bookmarksopen=true,
+ bookmarksnumbered=true,
+ colorlinks=true,
+ allcolors={frama-c-dark-orange}
+]{hyperref}
+
+% --------------------------------------------------------------------------
+% CEA commands
+% --------------------------------------------------------------------------
+
+\newcommand{\cealist}{CEA-List}
+\newcommand
+ {\fcaffiliationen}
+ {\cealist, Université Paris-Saclay\\ Software Safety and Security Lab\xspace}
+\newcommand
+ {\fcaffiliationfr}
+ {\cealist, Université Paris-Saclay\\ Laboratoire de Sûreté et Sécurité des Logiciels\xspace}
+
+\newcommand{\cealogo}{logos/cea_tech_list.png}
+
+% --------------------------------------------------------------------------
+% LICENSE commands
+% --------------------------------------------------------------------------
+
+\def\@licence{}
+\def\@licencelogo{}
+\def\@licencelink{}
+\newcommand{\licence}[3]{
+ \def\@licence{#1}
+ \def\@licencelogo{#2}
+ \def\@licencelink{#3}
+}
+\newcommand{\cclicence}[1]{
+ \licence
+ {Creative Commons \uppercase{#1}}
+ {logos/#1.png}
+ {\url{https://creativecommons.org/licenses/#1/4.0/}}
+}
+
+% --------------------------------------------------------------------------
+% Copyright commands
+% --------------------------------------------------------------------------
+
+\def\@copyrightfrom{}
+\newcommand{\copyrightstarts}[1]{
+ \def\@copyrightfrom{#1}
+}
+
+\newcommand{\addcopyrightowner}[1]{
+ \listadd{\@copyrightowner}{#1}
+}
+\addcopyrightowner{cealist} % add it by default
+
+\newcommand{\insertcopyrightowners}{{
+ \def\listsep{\def\listsep{, }}%
+ \renewcommand{\do}[1]{\listsep##1}%
+ \dolistloop\@copyrightowner
+}}
+
+\newcommand{\insertcopyright}{
+ \textcopyright\xspace \@copyrightfrom-\the\year{} \insertcopyrightowners
+}
+
+% --------------------------------------------------------------------------
+% Logos
+% --------------------------------------------------------------------------
+
+\def\@logos{}
+\newcommand{\addlogo}[1]{
+ \listadd{\@logos}{#1}
+}
+\addlogo{\cealogo} % add it by default
+
+\newcommand{\insertlogos}{{
+ \def\listsep{\def\listsep{\hspace{2em}}}%
+ \renewcommand{\do}[1]{\listsep\includegraphics[height=7em]{##1}}%
+ \dolistloop\@logos
+}}
+
+% --------------------------------------------------------------------------
+% Subtitle
+% --------------------------------------------------------------------------
+
+\def\@subtitle{}
+
+\newcommand{\subtitle}[1]{
+ \def\@subtitle{#1}
+}
+
+% --------------------------------------------------------------------------
+% Frama-C commands
+% --------------------------------------------------------------------------
+
+\def\@fcversion{}
+\newcommand{\fcversion}[1]{
+ \subtitle{For Frama-C #1}
+}
+
+\def\fchrulefill{\leavevmode\leaders\hrule height 1.25pt\hfill\kern\z@}
+
+
+% --------------------------------------------------------------------------
+% Title page
+% --------------------------------------------------------------------------
+
+\renewcommand{\maketitle}{%
+ \newgeometry{top=1cm, bottom=1cm, right=1cm,left=1cm}
+ \thispagestyle{empty}
+ \noindent\includegraphics{logos/frama-c.png}
+
+ \tikzfading[name=fade right,left color=transparent!0, right color=transparent!80]
+ \tikz[remember picture,overlay]{
+ \node[inner sep=0pt,anchor=south,yshift=35mm] (named) at (current page.south){
+ \includegraphics[width=\paperwidth]{logos/frama-c-guy}
+ };
+ \fill[white,path fading=fade right]
+ (named.south west) rectangle (named.north east);
+ }
+
+ \vspace{12em}
+ \begin{center}
+ \textbf{\Huge\@title}
+
+ \medskip
+ \ifx\@subtitle\empty\else{
+ \Large \@subtitle
+ }\fi
+ \end{center}
+
+ \vspace{-1em}
+ {\noindent\color{frama-c-orange}\fchrulefill}
+
+ \begin{center}
+ \begin{minipage}{.8\textwidth}
+ \centering
+ \large\@author
+ \end{minipage}
+ \end{center}
+
+ \bigskip
+
+ \begin{center}
+ \insertlogos
+ \end{center}
+
+ \vfill
+
+ \noindent
+ \ifx\@licencelogo\empty
+ \else{
+ \begin{minipage}{.14\textwidth}
+ \includegraphics[height=25pt]{\@licencelogo}
+ \end{minipage}
+ \hfill
+ }
+ \fi
+ \begin{minipage}{.84\textwidth}
+ \vspace{.2em}
+ \ifx\@licence\empty
+ \else{\large Work licensed under \@licence\xspace licence}\fi\\
+ \ifx\@licencelink\empty
+ \else{\large\@licencelink}\fi
+ \end{minipage}
+ \medskip
+
+ \noindent\insertcopyright
+
+ \restoregeometry%
+
+ \cleardoublepage
+}
+
+% --------------------------------------------------------------------------
+% Table of contents
+% --------------------------------------------------------------------------
+
+\newcommand\tocdotfill{{\normalfont\normalsize \TOCLineLeaderFill}}
+
+\titlecontents{chapter}
+ [0em]
+ {\bigskip}
+ {\makebox[2em][l]{\thecontentslabel}\bfseries}
+ {\hspace*{2em}\bfseries}
+ {\space\hfill\makebox[1.5em]{\contentspage}}[]
+
+\titlecontents{section}
+ [2em]
+ {\medskip}
+ {\makebox[3em][l]{\thecontentslabel}}
+ {\hspace*{3em}}
+ {\space\tocdotfill\makebox[1.5em]{\contentspage}}[]
+
+\titlecontents{subsection}
+ [5em]
+ {\smallskip}
+ {\makebox[4.5em][l]{\thecontentslabel}}
+ {\hspace*{4.5em}}
+ {\space\tocdotfill\makebox[1.5em]{\contentspage}}[]
+
+% --------------------------------------------------------------------------
+% Acknoledgements
+% --------------------------------------------------------------------------
+
+\def\@people{}
+\newcommand{\acknowledge}[1]{
+ \listadd{\@people}{#1}
}
+\newcommand{\commaorandlist}[1]{%
+ \count255=0
+ \def\do##1{\advance\count255 1 \chardef\finalitem=\count255 }%
+ \dolistloop{#1}%
+ \count255=0
+ \def\do##1{\advance\count255 1
+ \ifnum\count255=\finalitem
+ \space and\space
+ \else
+ \ifnum\count255=1\else,\space\fi
+ \fi##1}
+ \dolistloop{#1}}
+
+\newcommand{\insertpeople}{{
+ \ifx\@people\empty\else
+ {We gratefully thank all the people who contributed to this document: \commaorandlist\@people.}
+ \fi
+}}
+
+
% \acknowledge{<flag image file>}{<text inside box>}
-\newcommand{\acknowledge}[2]{
+\newcommand{\acknowledgeprogram}[2]{
\fbox{
\begin{minipage}{0.97\textwidth}
\begin{minipage}{1.2cm}
@@ -142,233 +296,435 @@ prefix=framacbook@,
}
}
-\newcommand{\acknowledgeANR}{
- \acknowledge{anr-logo.png}{the French ANR projects
- CAT~(ANR-05-RNTL-00301) and U3CAT~(08-SEGI-021-01)
- }
+\newcommand{\acknowledgeANR}[1]{
+ \acknowledgeprogram{anr-logo.png}{#1}
}
-\newcommand{\acknowledgeEU}{
- \acknowledge{eu-flag.jpg}{the
- European Union's Seventh Framework Programme (FP7/2007-2013)
- under grant agreement N$^\circ$\,317753 (\mbox{STANCE}).\\
- It has also received funding from the Horizon 2020 research
- and innovation programme, under grant agreements
- N$^\circ$\,731453~(\mbox{VESSEDIA}),
- N$^\circ$\,824231~(\mbox{DECODER}),
- N$^\circ$\,830892~(\mbox{SPARTA}),
- and N$^\circ$\,883242~(\mbox{ENSURESEC})
- }
+\newcommand{\acknowledgeEU}[1]{
+ \acknowledgeprogram{eu-flag.jpg}{#1}
}
% --------------------------------------------------------------------------
-% --- Sectionning ---
+% Header
+% --------------------------------------------------------------------------
+
+\pagestyle{fancy}
+\fancyhf{}
+\fancyhead[L]{\vspace{1.25em}\raggedleft\rightmark\vspace{-1.25em}}
+\fancyfoot[C]{\thepage}
+\renewcommand{\headrulewidth}{0pt}
+\setlength{\headheight}{24pt}
+
+% --------------------------------------------------------------------------
+% Chapters
+% --------------------------------------------------------------------------
+
+\titleformat{\chapter}[display]
+ {\sc\huge}
+ {\filleft\fontsize{50}{0}\selectfont\thechapter}
+ {-1.1em}
+ {\filright}
+ [\normalsize\vspace{-.5em}\color{frama-c-orange}\fchrulefill]
+
+\titleformat{\section}[hang]
+ {\Large\bfseries}
+ {\thesection}
+ {1em}
+ {}
+ [\vspace{-10pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}]
+
+\titlespacing*{\section}{0pt}{20pt}{20pt}
+
+% --------------------------------------------------------------------------
+% Itemize style
+% --------------------------------------------------------------------------
+
+\renewcommand\labelitemi{--}
+\setitemize{noitemsep,topsep=5pt,parsep=0pt,partopsep=0pt}
+\setenumerate{noitemsep,topsep=5pt,parsep=0pt,partopsep=0pt}
+
+% --------------------------------------------------------------------------
+% Footnote style
% --------------------------------------------------------------------------
-\titleformat{\chapter}[display]{\Huge\raggedleft}%
-{\huge\chaptertitlename\,\thechapter}{0.5em}{}
-\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
-[\vspace{-14pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}]
-\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
-[\vspace{-8pt}]
+
+\renewcommand\footnoterule{%
+ \kern-3\p@%
+ {\color{frama-c-orange}\hrule\@width\columnwidth}%
+ \kern2.6\p@%
+}
+
+\renewcommand{\@makefntext}[1]{
+ \setlength{\parindent}{0pt}
+ \begin{list}{}{\setlength{\labelwidth}{1.5em}
+ \setlength{\leftmargin}{\labelwidth}
+ \setlength{\labelsep}{3pt}
+ \setlength{\itemsep}{0pt}
+ \setlength{\parsep}{0pt}
+ \setlength{\topsep}{3pt}
+ \footnotesize}
+ \item[\@makefnmark\hfil]#1
+ \end{list}
+}
% --------------------------------------------------------------------------
-% --- Main Text Style ---
+% Warning & information style
% --------------------------------------------------------------------------
-%\raggedright
-\setlength\parindent{0pt}
-\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
-\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
-\def\FramaC{\textsf{Frama-C}\xspace}
+
+\newsavebox{\fcsavebox}
+\newenvironment{colbox}[1]{%
+ \newcommand\colboxcolor{#1}%
+ \begin{lrbox}{\fcsavebox}%
+ \begin{minipage}{\dimexpr\linewidth-2\fboxsep\relax}
+ \itshape
+}{%
+ \end{minipage}\end{lrbox}%
+ \begin{center}
+ \colorbox{\colboxcolor}{\usebox{\fcsavebox}}
+ \end{center}
+}
+
+\newenvironment{important}{\begin{colbox}{frama-c-dark-orange!30}}{\end{colbox}}
+\newenvironment{information}{\begin{colbox}{frama-c-green!30}}{\end{colbox}}
+
% --------------------------------------------------------------------------
-% --- Listings ---
+% Code
% --------------------------------------------------------------------------
+
+\RequirePackage{scrhack} % avoids warning about \float@addtolists related to lstlisting
\RequirePackage{listings}
+\RequirePackage{caption}
+\RequirePackage{accsupp}
-\lstdefinelanguage{ACSL}{%
- morekeywords={allocates,assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
- boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
- exit_behavior,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
- model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
- union,variant},
- keywordsprefix={\\},
- alsoletter={\\},
- morecomment=[l]{//}
+\newcommand{\noncopynumber}[1]{%
+ \BeginAccSupp{method=escape,ActualText={}}%
+ #1%
+ \EndAccSupp{}%
}
-\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
-\definecolor{lstbg}{gray}{0.98}
-\definecolor{lstfg}{gray}{0.10}
-\definecolor{lstrule}{gray}{0.6}
-\definecolor{lstnum}{gray}{0.4}
+\renewcommand{\ttdefault}{pcr} % so that keywords can be bold
+
+% CAPTION
+
+\DeclareCaptionFormat{listing}{
+ \raggedright\textbf{#1 #2} #3
+ \vspace{-2mm}
+ {\color{gray}\rule{\textwidth}{0.1pt}}
+}
+\DeclareCaptionLabelSeparator{listing}{--}
+\captionsetup[lstlisting]{format=listing,labelsep=listing}
+
+% Basic style
+% --------------------------------------------------------------------------
+
+\definecolor{lstnum}{gray}{0.3}
\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
-\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
+\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}
\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
\definecolor{lstfile}{gray}{0.85}
+\definecolor{lstcomments}{rgb}{0.35,0.35,0.35}
+
\newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
+
\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\small\else\normalfont\ttfamily\mdseries\small\fi}
-\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
+\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\normalsize\fi}
\def\lp@keyword{}
-\def\lp@special{\color{lstfg}}
-\def\lp@comment{\normalfont\ttfamily\mdseries}
-\def\lp@string{\color{lstfg}} \def\lp@ident{}
-\def\lp@number{\rmfamily\tiny\color{lstnum}}
-\lstdefinestyle{frama-c-style}{%
+\def\lp@special{\color{frama-c-dark-orange}}
+\def\lp@comment{\normalfont\ttfamily\mdseries\color{lstcomments}}
+\def\lp@string{\color{frama-c-dark-green}}
+\def\lp@ident{}
+\def\lp@number{\rmfamily\tiny\color{lstnum}\noncopynumber}
+
+\lstdefinestyle{frama-c-basic-style}{%
+ captionpos=b,%
columns=flexible,%
basicstyle=\lp@inline,%
identifierstyle=\lp@ident,%
commentstyle=\lp@comment,%
- keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
- keywordstyle=[2]\lp@special,%
+ keywordstyle={\bfseries\ifmmode\mathsf\else\ttfamily\fi\color{blue}},%
+ keywordstyle=[2]\bfseries\lp@special,%
stringstyle=\lp@string,%
emphstyle=\lp@ident\underbar,%
showstringspaces=false,%
- mathescape=true,%
numberstyle=\lp@number,%
- xleftmargin=6ex,xrightmargin=2ex,%
+ xleftmargin=1.82em,%
framexleftmargin=1ex,%
frame=l,%
framerule=1pt,%
- rulecolor=\color{lstrule},%
- backgroundcolor=\color{lstbg},%
+ rulecolor=\color{frama-c-orange!60},%
+ backgroundcolor=\color{frama-c-bronze!10},%
+ literate={\ }{\ }1,
+ % ^~~~~ Without this, spaces starting a line does not have the right size ...
+}
+
+\lstdefinestyle{frama-c-style}{%
+ style=frama-c-basic-style,%
moredelim={*[s]{/*@}{*/}},%
moredelim={*[l]{//@}},%
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=`
-% breaklines is broken when using a inline and background
-% breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
}
+% Code styles
+% --------------------------------------------------------------------------
+
+\lstdefinestyle{frama-c-shell-style}{%
+ mathescape=false,%
+ basicstyle=\lp@basic,%
+ keywordstyle=\sffamily\bfseries,%
+ keywordstyle=[1]\sffamily\color{lstmodule},%
+ keywordstyle=[2]\sffamily\color{lstspecial},%
+ keywordstyle=[3]\sffamily\bfseries,%
+ identifierstyle=\ttfamily,%
+ stringstyle=\ttfamily\color{frama-c-orange},%
+ commentstyle=\rmfamily\bfseries\color{lsttxt},%
+ literate={\\\$}{\$}1%
+ {€}{\textbackslash}1%
+,%
+}
+
+% ACSL + C
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{ACSL}{%
+ escapechar={},
+ literate=,
+ breaklines=false,
+ classoffset=1,
+ morekeywords={admit,allocates,assert,assigns,assumes,axiom,axiomatic,behavior,
+ behaviors,boolean,breaks,calls,check,complete,continues,data,decreases,disjoint,
+ ensures,exits,frees,ghost,global,import,inductive,integer,invariant,lemma,
+ logic,loop,model,module,predicate,reads,real,requires,sizeof,strong,struct,
+ terminates,returns,type,union,variant,
+ dynamic_split,merge,pragma,slevel,split,taints,taint,unroll,widen_hints,
+ \\tainted,
+ Here,LoopCurrent,LoopEntry,Pre,Post,Old,
+ \\Cons,\\Down,\\NearestAway,\\NearestEven,\\Nil,\\ToZero,\\Up,
+ \\at,\\allocable,\\allocation,\\automatic,\\base_addr,\\block_length,\\dangling,
+ \\dynamic,\\exists,\\exit_status,\\false,\\forall,\\freeable,\\fresh,\\from,
+ \\in,\\initialized,\\lambda,\\let,\\list,\\match,\\nothing,\\null,\\numof,
+ \\object_pointer,\\offset,\\old,\\register,\\result,\\separated,\\static,
+ \\sum,\\true,\\unallocated,\\valid,\\valid_function,\\valid_read,\\with},
+ classoffset=0,
+ alsoletter={\\},
+ morecomment=[l]{//}
+}
+
+\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
+
\lstdefinestyle{c}%
{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
\lstdefinestyle{c-basic}%
{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
-
-% --- C/ACSL Stuff ---------------------------------------------------------
-% Make 'c' the default style
-\lstset{style=c}
-
\newcommand{\listinginput}[3][1]%
{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}
-
\newcommand{\listinginputcaption}[4][1]%
-{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,title=#3]{#4}}
+{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,caption={#3}]{#4}}
\lstnewenvironment{listing}[2][1]%
{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
-
\lstnewenvironment{listing-nonumber}%
{\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}
-% --- Verbatim Stuff -------------------------------------------------------
-\lstdefinelanguage{Shell}[]{csh}%
-{escapechar=@
- identifierstyle=\lp@basic,
- mathescape=false,
- backgroundcolor=,
- literate={\\\$}{\$}1
-}
+% Commands used mainly by Eva manual
-\lstnewenvironment{shell}[1][]
-{\lstset{language=Shell,basicstyle=\lp@basic,#1}}
-{}
+\newcommand{\logwithrange}[2]%
+{\lstinputlisting[breaklines=true,basicstyle=\ttfamily\small,linerange=#1]{#2}}
-% ---- Stdout Stuff --------------------------------------------------------
-\lstdefinelanguage{Logs}[]{csh}%
-{identifierstyle=\lp@basic,backgroundcolor=}
-\lstnewenvironment{logs}[1][]{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
-\newcommand{\logsinput}[1]%
-{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
+\newcommand{\cwithrange}[2]%
+{\lstinputlisting[style=c-basic,numbers=left,linerange=#1]{#2}}
+
+\newcommand{\csource}[1]%
+{\lstinputlisting[style=c-basic,numbers=left]{#1}}
+
+\lstnewenvironment{listing-log}%
+{\lstset{numbers=none,basicstyle=\lp@basic}}{}
+
+% ACSL + C (developers)
% --------------------------------------------------------------------------
-% --- Developer Code Stuff ---
-% --------------------------------------------------------------------------
-
-\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
-
-% --- Style ----------------------------------------------------------------
-\lstdefinestyle{framac-code-style}{%
-basicstyle=\lp@inline,%
-numberstyle=\lp@number,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\rmfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-}
-\lstdefinestyle{framac-shell-style}{%
-mathescape=false,%
-basicstyle=\lp@basic,%
-numberstyle=\lp@number,%
-keywordstyle=\sffamily\bfseries,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\ttfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-literate={\\\$}{\$}1%
-{€}{\textbackslash}1%
-,%
+
+\lstdefinestyle{framac-code}%
+{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
+
+\newcommand{\cinput}[2][]%
+{\lstinputlisting[
+ language={[ANSI]C},
+ alsolanguage=ACSL,
+ style=frama-c-style,#1]{#2}
}
-% --- Configure ------------------------------------------------------------
+\newcommand{\cinline}[1]%
+{\lstinline[style=framac-code]{#1}}
+
+\lstnewenvironment{ccode}[1][]%
+{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic,#1}}{}
+
+% Configure
+% --------------------------------------------------------------------------
+
\lstdefinelanguage{Configure}[]{csh}{%
-style=framac-shell-style,%
-morekeywords={fi},%
+ style=frama-c-shell-style,%
+ morekeywords={fi},%
}
+
+\newcommand{\configureinput}[1]%
+{\lstinputlisting[language=Configure]{#1}}
+
\lstnewenvironment{configurecode}[1][]%
{\lstset{language=Configure,#1}}{}
-\newcommand{\configureinput}[1]{\lstinputlisting[language=Configure]{#1}}
-% --- Makefile ------------------------------------------------------------
+
+% Commands
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{frama-c-commands}[]{}{%
+ mathescape=false,%
+ alsoletter=-.,%
+ keywordstyle=\color{frama-c-green}\bfseries,%
+ keywordstyle=[2]\color{frama-c-dark-red}\bfseries,%
+ classoffset=0,%
+ keywords={e-acsl-gcc.sh,frama-c,frama-c-gui,frama-c-script},%
+ classoffset=1,%
+ morekeywords={-load,-then,-then-last,-then-on,-then-replace,-save},%
+ classoffset=0,%
+ morestring=[b]{'},
+ morestring=[b]{"},
+ literate={\\\$}{\$}1%
+}
+
+\lstnewenvironment{frama-c-commands}[1][]
+{\lstset{style=frama-c-basic-style,language=frama-c-commands,#1}}{}
+
+% Dune
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{Dune}{%
+ literate=%
+ {Ã }{{\`a}}1%
+ {é}{{\'e}}1%
+ ,
+ style=frama-c-style,%
+ alsoletter=:-,%
+ keywords={%
+ action,alias,as,backend,context,default,deps,dune,executable,%
+ env,env-vars,files,flags,from,generate_opam_files,install,%
+ instrument_with,instrumentation,lang,libraries,library,name,optional,%
+ package,plugin,profile,progn,public_name,rule,section,select,site,%
+ targets,using%
+ },%
+ morekeywords=[2]{%
+ :standard%
+ },%
+ morecomment=[l]{;},%
+}
+
+\lstdefinestyle{dune-basic}{%
+ language=Dune,%
+ style=frama-c-basic-style,%
+ basicstyle=\lp@inline,%
+}
+
+\newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}}
+
+\lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{}
+
+% Logs
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{Logs}[]{}{%
+ style=frama-c-basic-style,
+ mathescape=false,
+ backgroundcolor=,
+ literate={\\\$}{\$}1
+}
+
+\newcommand{\logsinput}[1]%
+{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
+
+\lstnewenvironment{logs}[1][]%
+{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
+
+% Makefile
+% --------------------------------------------------------------------------
+
\lstdefinelanguage{Makefile}[]{make}{%
-style=framac-shell-style,%
-morekeywords={include},%
+ style=frama-c-shell-style,%
+ morekeywords={include},%
}
+
+\lstdefinestyle{make-basic}{%
+ language=Makefile,%
+ style=frama-c-basic-style,%
+ basicstyle=\lp@inline,%
+}
+
+\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
+\newcommand{\makeinput}[2][]{\lstinputlisting[style=make-basic,#1]{#2}}
+
\lstnewenvironment{makefilecode}[1][]%
{\lstset{language=Makefile,#1}}{}
-\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
-% --- C- for Developer ----------------------------------------------------
-\lstdefinestyle{framac-code}%
- {language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
-\lstnewenvironment{ccode}[1][]%
-{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
-\newcommand{\cinput}[1]%
-{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic]{#1}}
-\newcommand{\cinline}[1]%
-{\lstinline[style=framac-code]{#1}}
-% --- Ocaml ----------------------------------------------------------------
+
+\lstnewenvironment{makecode}[1][]%
+{\lstset{style=make-basic,#1}}{}
+
+% OCaml
+% --------------------------------------------------------------------------
+
\lstdefinelanguage{Ocaml}[Objective]{Caml}{%
-style=framac-code-style,%
-deletekeywords={when,module,struct,sig,begin,end},%
-morekeywords=[2]{failwith,raise,when},%
-morekeywords=[3]{module,struct,sig,begin,end},%
-literate=%
-{~}{${\scriptstyle\thicksim}$}1%
-{<}{$<$ }1%
-{>}{$>$ }1%
-{->}{$\rightarrow$ }1%
-{<-}{$\leftarrow$ }1%
-{:=}{$\leftarrow$ }1%
-{<=}{$\leq$ }1%
-{>=}{$\geq$ }1%
-{==}{$\equiv$ }1%
-{!=}{$\not\equiv$ }1%
-{<>}{$\neq$ }1%
-{'a}{$\alpha$ }1%
-{'b}{$\beta$ }1%
-{'c}{$\gamma$ }1%
-{µ}{`{}}1%
-{€}{\textbackslash}1%
-}
-
-\lstdefinestyle{ocaml-basic}%
-{language=Ocaml,basicstyle=\lp@basic}
+ style=frama-c-basic-style,%
+ deletekeywords={when,module,struct,sig,begin,end},%
+ morekeywords=[2]{failwith,raise,when},%
+ morekeywords=[3]{module,struct,sig,begin,end},%
+ literate=%
+ {~}{${\scriptstyle\thicksim}$}1%
+ {<}{$<$ }1%
+ {>}{$>$ }1%
+ {->}{$\rightarrow$ }1%
+ {<-}{$\leftarrow$ }1%
+ {:=}{$\leftarrow$ }1%
+ {<=}{$\leq$ }1%
+ {>=}{$\geq$ }1%
+ {==}{$\equiv$ }1%
+ {!=}{$\not\equiv$ }1%
+ {<>}{$\neq$ }1%
+ {'a}{$\alpha$ }1%
+ {'b}{$\beta$ }1%
+ {'c}{$\gamma$ }1%
+ {µ}{`{}}1%
+ {€}{\textbackslash}1%
+ {Ã }{{\`a}}1%
+ {é}{{\'e}}1%
+}
+
+\lstdefinestyle{ocaml-basic}{
+ language=Ocaml,
+ basicstyle=\lp@basic
+}
+
\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
+
\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
+
+% Shell
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{Shell}[]{csh}{%
+ escapechar=@
+ identifierstyle=\lp@basic,
+ mathescape=false,
+ backgroundcolor=,
+ literate={\\\$}{\$}1
+}
+
+\newcommand{\listingname}[1]%
+{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
+
+\lstnewenvironment{shell}[1][]
+{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{}
+
+% Why
% --------------------------------------------------------------------------
+
\lstdefinelanguage{Why}{%
morekeywords={
type, logic, axiom, predicate, goal,
@@ -382,22 +738,22 @@ literate=%
{not}{$\neg$}1%
{<>}{$\neq$}1%
{...}{$\dots$}1%
- %{_}{\_}1%
- %{_}{{\rule[0pt]{1ex}{.2pt}}}1%
- }
+}
\lstdefinestyle{why-style}{%
-language=Why,%
-style=framac-code-style,%
-basicstyle=\lp@inline,%
+ language=Why,%
+ style=frama-c-basic-style,%
+ basicstyle=\lp@inline,%
}
-\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
\newcommand{\whyinput}[1]%
{\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}}
\newcommand{\whyinline}[1]%
{\lstinline[style=why-style]{#1}}
-\makeatother
-% --------------------------------------------------------------------------
-% --- End. ---
+
+\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
+
+% Default style is empty
% --------------------------------------------------------------------------
+
+\lstset{style=frama-c-style}
diff --git a/doc/userman/frama-c-cover.pdf b/doc/userman/frama-c-cover.pdf
deleted file mode 100644
index 4e14243c8064ca92d696fd354476dcdb31092895..0000000000000000000000000000000000000000
Binary files a/doc/userman/frama-c-cover.pdf and /dev/null differ
diff --git a/doc/userman/frama-c-left.pdf b/doc/userman/frama-c-left.pdf
deleted file mode 100644
index ddf8888d292539177ab81c1b33d6411edf51c820..0000000000000000000000000000000000000000
Binary files a/doc/userman/frama-c-left.pdf and /dev/null differ
diff --git a/doc/userman/frama-c-right.pdf b/doc/userman/frama-c-right.pdf
deleted file mode 100644
index db9b236dfdb19d9a6631ec55eee63f431f8d6f0d..0000000000000000000000000000000000000000
Binary files a/doc/userman/frama-c-right.pdf and /dev/null differ
diff --git a/doc/userman/grammar.tex b/doc/userman/grammar.tex
index 2515986a8b42964329b2a4bcf6b44cfc6baea327..7ea2ba62386c990a406972e32ee51c17a03efe99 100644
--- a/doc/userman/grammar.tex
+++ b/doc/userman/grammar.tex
@@ -1,11 +1,10 @@
-\newcommand{\lang}{C++\xspace}
\chapter{Grammar and parser for \acslpp}
\label{sec:grammar}
-This section summarizes some of the technical implementation considerations in writing a parser for \acslpp within \fclang.
-This material may be useful for developers and maintainers of \fclang; it is not needed by users of \fclang.
+This section summarizes some of the technical implementation considerations in writing a parser for \acslpp within \framaclang.
+This material may be useful for developers and maintainers of \framaclang; it is not needed by users of \framaclang
-Recall that \fclang uses clang to parse \lang and a custom parser to parse \acslpp annotations, jointly producing a representation of the \lang and \acslpp source input in the Frama-C intermediate language.
+Recall that \framaclang uses clang to parse \Cpp and a custom parser to parse \acslpp annotations, jointly producing a representation of the \Cpp and \acslpp source input in the Frama-C intermediate language.
The first version of the \acslpp custom parser, written during the STANCE project, used a hand-written bison-like parser, but with function pointers to record state and actions rather than using a tool-generated table to drive the parsing.
This design proved to be too brittle and difficult to efficiently evolve as new features were added to \acslpp.
Consequently during the VESSEDIA project, the scanner and parser were completely rewritten, largely retaining the previous design's connections to clang, token definitions, name lookup and type resolution, and AST generation.
@@ -18,7 +17,7 @@ The bulleted paragraphs below describe the problematic aspects of \acslpp and ho
The principal goal of an LL(k) formulation of a grammar is to be able to predict which grammar production is being seen in the input stream from a small amount of look-ahead.
Most \acslpp constructs start with a unique keyword (e.g., clauses begin with \lstinline|requires|, \lstinline|ensures| etc.) which serves this purpopse.
-But the constructs inherited from \lang pose some challenges.
+But the constructs inherited from \Cpp pose some challenges.
\begin{itemize}
\item \textbf{Left recursion}. Expression grammars are typically left recursive, which is problematic for recursive descent parsers.
@@ -41,15 +40,26 @@ Many operations on a data type are also simply element-by-element operations on
Also, errors found during type-checking can be associated with more readable error messages than those found during parsing.
\item \textbf{cast vs. parenthesized expression} To determine whether an input like \lstinline|(T)-x| is (a) the difference of the parenthesized expression \lstinline|(T)| and \lstinline|x| or (b) a cast of \lstinline|-x| to the type \lstinline|T|, one must know whether \lstinline|T| is a variable or type.
-This is a classic problem in parsing \lang; it requires that identifiers be known to be either type names or variable names in the scanner.
+This is a classic problem in parsing \Cpp; it requires that identifiers be known to be either type names or variable names in the scanner.
In addition, \lstinline|T| here can be an arbitrary type expression.
-For example, in \lang, a type expression can contain pointer operators that can look, at least initially like multiplications and they can contain template instantiations that look initially like comparisons.
-\fclang handles this situation by allowing a backtrackable parse.
+For example, in \Cpp, a type expression can contain pointer operators that can look, at least initially like multiplications and they can contain template instantiations that look initially like comparisons.
+\framaclang handles this situation by allowing a backtrackable parse.
When a left parenthesis is parsed in an expression context, the parser proceeds by attempting a parse of a cast expression. If the contents of the parenthesis pair is successfully parsed as a type expression, it is assumed to be a cast expression.
If such a parse fails, no error messages are emitted; rather the parse is rewound and proceeds again assuming the token sequence to be a parenthesized expression.
-\item \textbf{set comprehension}. The syntax of the set comprehension expression follows traditional mathematics: \lstinline: { $expr$ | $binders$ ; $predicate$ }:. This structure poses two difficulties for parsers. First, the expression $expr$ may contain bitwise-or operators, so it is not known to the parser whether an occurence of \verb:|: is the beginning of the binders or is just a bitwise-or operator. Second, the expression will use the variables declared in the binders section. However, the binders are not seen until after the expression is scanned. Note that these problems are not unique to a recursive descent design; they would challenge a LR parser just as much. \textit{This particular feature is not yet implemented in \fclang, nor in Frama-C and so is not yet resolved in the parser implementation.}
+\item \textbf{set comprehension}. The syntax of the set comprehension expression
+ follows traditional mathematics:
+ \lstinline:{ $expr$ | $binders$ ; $predicate$}:.
+ This structure poses two difficulties for parsers. First, the expression
+ $expr$ may contain bitwise-or operators, so it is not known to the parser
+ whether an occurence of \verb:|: is the beginning of the binders or is just a
+ bitwise-or operator. Second, the expression will use the variables declared in
+ the binders section. However, the binders are not seen until after the
+ expression is scanned. Note that these problems are not unique to a recursive
+ descent design; they would challenge a LR parser just as much.
+ \textit{This particular feature is not yet implemented in \framaclang,
+ nor in \FramaC and so is not yet resolved in the parser implementation.}
\item \textbf{labeled expressions}. \acslpp allows expressions to have labels, designated by a \lstinline|id : | prefix.
So the parser cannot know whether an initial \lstinline|id| is a variable or just a label until the colon is parsed.
@@ -59,7 +69,7 @@ Ambiguity arises with the use of a colon for the else part of a conditional expr
So in an expression such as
\lstinline| a ? b ? c : d : e : f|, it is ambiguous whether \lstinline|c| or \lstinline|d| or \lstinline|e| is a label.
Parenthesizing must be used to solve this problem.
-\fcl presumes that if the \textit{then} part of a conditional expression is being parsed, a following colon is always the colon introducing the \textit{else} part. That is, the binding to a conditional expression has tighter precedence than to a naming expression.
+\framaclang presumes that if the \textit{then} part of a conditional expression is being parsed, a following colon is always the colon introducing the \textit{else} part. That is, the binding to a conditional expression has tighter precedence than to a naming expression.
\end{itemize}
diff --git a/doc/userman/introduction.tex b/doc/userman/introduction.tex
index 153ccad068151e00262bae8359f32567131f8dc3..59baba0c2255b99598a03063ed85d1725e7e183e 100644
--- a/doc/userman/introduction.tex
+++ b/doc/userman/introduction.tex
@@ -1,21 +1,21 @@
\chapter{Introduction}
-\framac~\cite{userman,fac15} is a modular analysis framework for the \C
+\FramaC~\cite{userman,baudinCACM21} is a modular analysis framework for the \C
programming language that supports the \acsl specification
-language~\cite{acsl}. This manual documents the \fclang plug-in of \framac,
+language~\cite{acsl}. This manual documents the \framaclang plug-in of \FramaC,
version \fclangversion.
-The \fclang plug-in supports the \acslpp extension of \acsl for \cpp programs and specifications;
+The \framaclang plug-in supports the \acslpp extension of \acsl for \Cpp programs and specifications;
it is built on the \clang\footnote{https://clang.llvm.org/} compiler infrastructure and uses \clang for
-parsing C++. The plug-in extends \clang to parse \acslpp, translating source files containing \cpp and \acslpp into \framac's intermediate language for \C and \acsl.
+parsing C++. The plug-in extends \clang to parse \acslpp, translating source files containing \Cpp and \acslpp into \FramaC's intermediate language for \C and \acsl.
-The \fclang plug-in intends to provide a full translation of \cpp and \acslpp into the \framac internal representation, and from there to allow \cpp programs and \acslpp specifications to be analyzed by other \framac plug-ins.
+The \framaclang plug-in intends to provide a full translation of \Cpp and \acslpp into the \FramaC internal representation, and from there to allow \Cpp programs and \acslpp specifications to be analyzed by other \FramaC plug-ins.
\textit{This is a work in progress.}
The following sections describe the current status and limitations of the current implementation.
\begin{itemize}
- \item The plug-in aims for the C++11 version of \cpp
- \item \acslpp is described in the companion \acslpp reference manual \cite{acslpp}, also a part of the \framac release.
+ \item The plug-in aims for the C++11 version of \Cpp
+ \item \acslpp is described in the companion \acslpp reference manual \cite{acslpp}, also a part of the \FramaC release.
\item The plug-in is compatible with version \clangversion of \clang.
- This version of \clang supports \cpp versions through C++17
+ This version of \clang supports \Cpp versions through C++17
(cf. \url{https://clang.llvm.prg/cxx_status.html}).
- However, \fclang may not support all of the features of \cpp within annotations.
+ However, \framaclang may not support all of the features of \Cpp within annotations.
\end{itemize}
diff --git a/doc/userman/limitations.tex b/doc/userman/limitations.tex
index 6c2016f914b9e41a9d5a65b7ac45b31511005e58..85b534046d4e8b24931c278719e2384cf12f0cdc 100644
--- a/doc/userman/limitations.tex
+++ b/doc/userman/limitations.tex
@@ -1,13 +1,13 @@
\chapter{Known Limitations}
-The development of the \fclang plug-in is still ongoing.
-\fclang does not implement all of current C++ nor all of
+The development of the \framaclang plug-in is still ongoing.
+\framaclang does not implement all of current \Cpp nor all of
\acslpp as defined in its language definition~\cite{acslpp}.
The most important such limitations are listed in this section.
\textit{These lists are not (nearly) complete}
-\section{Implementation of C++}
+\section{Implementation of Cpp}
The following C++ features are not implemented in \acslpp.
\begin{itemize}
@@ -16,7 +16,7 @@ The following C++ features are not implemented in \acslpp.
\item uses of templates are not robust
\item uses of typeid
\item implementation of the standard library is very rudimentary
-\item main target of \fcl is C++11
+\item main target of \framaclang is C++11
\end{itemize}
\section{Implementation of \acslpp}
@@ -24,38 +24,38 @@ The following C++ features are not implemented in \acslpp.
These \acslpp features are not yet implemented
\begin{itemize}
-\item \fclang cannot process annotations that are separate from the source file
-\item \acslpp specifications for standard \cpp library functions are still quite limited
+\item \framaclang cannot process annotations that are separate from the source file
+\item \acslpp specifications for standard \Cpp library functions are still quite limited
\item \acslpp definitions within template declarations
\item ghost code is not yet implemented
\item model declarations
\item set comprehensions
\item using (namespace) declarations (parsed but has no effect)
\item pure functions (parsed but incompletely implemented)
-\item throws clause (parsed but not implemented in \framac)
+\item throws clause (parsed but not implemented in \FramaC)
\item interaction of throws and noexcept
\item parallel \textbackslash let
-\item \textbackslash count and \textbackslash data are parsed but not yet implemented in \framac
+\item \textbackslash count and \textbackslash data are parsed but not yet implemented in \FramaC
\item formal parameters that are references have pre and post states
-\item dynamic casting not yet implemented in \framac
+\item dynamic casting not yet implemented in \FramaC
\item rounding mode and related builtin functions
\item builtin types list and \textbackslash set and related builtin functions
-\item \textbackslash valid\_function \textbackslash allocable \textbackslash freeable \textbackslash fresh are not yet implemented by \framac
-\item extended quantifiers are not yet implemented by \framac
-\item global invariants are not yet implemented by \framac
-\item generalized invariants are not yet implemented by \framac
+\item \textbackslash valid\_function \textbackslash allocable \textbackslash freeable \textbackslash fresh are not yet implemented by \FramaC
+\item extended quantifiers are not yet implemented by \FramaC
+\item global invariants are not yet implemented by \FramaC
+\item generalized invariants are not yet implemented by \FramaC
\item assigns with both \textbackslash from and = is not yet implemented
\end{itemize}
-\section{Other \fcl limitations}
+\section{Other \framaclang limitations}
\begin{itemize}
-\item \option{-fclang-version} is not implemented
+\item \lstinline|-fclang-version| is not implemented
\item parsing routines need work to improve robustness, to improve accuracy of locations, and to guard against leaking memory when parses fail
\item the term/predicate parsing methods should be refactored to avoid deep call stacks
\item resolve issues of tset representations
-\item cannot change the set of C++ suffixes
-\item frama-clang info/warn/error messages are not yet properly categorized and integrated with -fclang-log, -fclang-msg-key, fclang-warn-key. In particular, clang messages are completely independent of the \framac logging framework
+\item cannot change the set of \Cpp suffixes
+\item frama-clang info/warn/error messages are not yet properly categorized and integrated with -fclang-log, -fclang-msg-key, fclang-warn-key. In particular, clang messages are completely independent of the \FramaC logging framework
\end{itemize}
%% Types for ternary, +/-, * etc. , unary & and *
diff --git a/doc/userman/logos/by-nc-nd.eu.png b/doc/userman/logos/by-nc-nd.eu.png
new file mode 100644
index 0000000000000000000000000000000000000000..1653db7476561b663b0a7804a6d57df932e63fb6
Binary files /dev/null and b/doc/userman/logos/by-nc-nd.eu.png differ
diff --git a/doc/userman/logos/by-nc-nd.png b/doc/userman/logos/by-nc-nd.png
new file mode 100644
index 0000000000000000000000000000000000000000..5a8dbd0652e37cc2d89b4899e307abcac8bda553
Binary files /dev/null and b/doc/userman/logos/by-nc-nd.png differ
diff --git a/doc/userman/logos/by-nc-sa.eu.png b/doc/userman/logos/by-nc-sa.eu.png
new file mode 100644
index 0000000000000000000000000000000000000000..433bc81751d21ffbfc2c13456a23ff60dc341eff
Binary files /dev/null and b/doc/userman/logos/by-nc-sa.eu.png differ
diff --git a/doc/userman/logos/by-nc-sa.png b/doc/userman/logos/by-nc-sa.png
new file mode 100644
index 0000000000000000000000000000000000000000..b9a55533c0cb035de1769b2a5ac63ce9b194fc69
Binary files /dev/null and b/doc/userman/logos/by-nc-sa.png differ
diff --git a/doc/userman/logos/by-nc.eu.png b/doc/userman/logos/by-nc.eu.png
new file mode 100644
index 0000000000000000000000000000000000000000..efdb6af68507a180a0fef0398415ff2b92516012
Binary files /dev/null and b/doc/userman/logos/by-nc.eu.png differ
diff --git a/doc/userman/logos/by-nc.png b/doc/userman/logos/by-nc.png
new file mode 100644
index 0000000000000000000000000000000000000000..25e284099a07df1ba95e4140fbfe7a8d1740fdc5
Binary files /dev/null and b/doc/userman/logos/by-nc.png differ
diff --git a/doc/userman/logos/by-nd.png b/doc/userman/logos/by-nd.png
new file mode 100644
index 0000000000000000000000000000000000000000..fc3d26789a0b4f529a132bcae501dca6ce208f45
Binary files /dev/null and b/doc/userman/logos/by-nd.png differ
diff --git a/doc/userman/logos/by-sa.png b/doc/userman/logos/by-sa.png
new file mode 100644
index 0000000000000000000000000000000000000000..8770732928cb20d8aeafee32bec9c5de89d51238
Binary files /dev/null and b/doc/userman/logos/by-sa.png differ
diff --git a/doc/userman/logos/by.png b/doc/userman/logos/by.png
new file mode 100644
index 0000000000000000000000000000000000000000..c8473a24786ab016d9c3e717a380910f7cbb0fff
Binary files /dev/null and b/doc/userman/logos/by.png differ
diff --git a/doc/userman/logos/cc-zero.png b/doc/userman/logos/cc-zero.png
new file mode 100644
index 0000000000000000000000000000000000000000..4ff09a0bb26016cef37b018a23d191be5a1cd0c9
Binary files /dev/null and b/doc/userman/logos/cc-zero.png differ
diff --git a/doc/userman/logos/cea_tech_list.png b/doc/userman/logos/cea_tech_list.png
new file mode 100644
index 0000000000000000000000000000000000000000..4abeb2bee459be6efca10a547ea6d7310e3af5a2
Binary files /dev/null and b/doc/userman/logos/cea_tech_list.png differ
diff --git a/doc/userman/logos/frama-c-guy.png b/doc/userman/logos/frama-c-guy.png
new file mode 100644
index 0000000000000000000000000000000000000000..c6515ac3ed7808cb49c4f75f538b4b8a4053627e
Binary files /dev/null and b/doc/userman/logos/frama-c-guy.png differ
diff --git a/doc/userman/logos/frama-c.png b/doc/userman/logos/frama-c.png
new file mode 100644
index 0000000000000000000000000000000000000000..4d342250616ea0cac92cc620f1417dcc56f16e19
Binary files /dev/null and b/doc/userman/logos/frama-c.png differ
diff --git a/doc/userman/logos/publicdomain.png b/doc/userman/logos/publicdomain.png
new file mode 100644
index 0000000000000000000000000000000000000000..df2c82f3dd0f862e820855a81f7e6123808b0340
Binary files /dev/null and b/doc/userman/logos/publicdomain.png differ
diff --git a/doc/userman/macros.tex b/doc/userman/macros.tex
index a0bcc8512655750dc99d56542550dab93fd52132..796b6b2395a66963eae68dd7687911ea5d5de0e1 100644
--- a/doc/userman/macros.tex
+++ b/doc/userman/macros.tex
@@ -1,305 +1,159 @@
-%%% Environnements dont le corps est suprimé, et
-%%% commandes dont la définition est vide,
-%%% lorsque PrintRemarks=false
-
-\usepackage{comment}
-
-\newcommand{\framac}{\textsc{Frama-C}\xspace}
-\newcommand{\fclang}{\textsc{Frama-Clang}\xspace}
-\newcommand{\clang}{\textsc{clang}\xspace}
-\newcommand{\acsl}{\textsc{ACSL}\xspace}
-\newcommand{\acslpp}{\textsc{ACSL++}\xspace}
-\newcommand{\acslb}{\acsl/\acslpp\xspace}
-
-
-\newcommand{\irg}{\lstinline|framaCIRGen|\xspace}
-\newcommand{\fcl}{\lstinline|frama-clang|\xspace}
-\newcommand{\fc}{\lstinline|frama-c|\xspace}
-\newcommand{\cl}{\lstinline|clang|\xspace}
-
-\newcommand{\rte}{\textsc{RTE}\xspace}
-\newcommand{\C}{\textsc{C}\xspace}
-\newcommand{\cpp}{\textsc{C++}\xspace}
-\newcommand{\jml}{\textsc{JML}\xspace}
-\newcommand{\Eva}{\textsc{Eva}\xspace}
-\newcommand{\variadic}{\textsc{Variadic}\xspace}
-\newcommand{\wpplugin}{\textsc{Wp}\xspace}
-\newcommand{\pathcrawler}{\textsc{PathCrawler}\xspace}
-\newcommand{\gcc}{\textsc{Gcc}\xspace}
-\newcommand{\gmp}{\textsc{GMP}\xspace}
-\newcommand{\dlmalloc}{\textsc{dlmalloc}\xspace}
-
-\newcommand{\nodiff}{\emph{No difference with \acsl.}}
-\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
-\newcommand{\limited}[1]{\emph{Limited to #1.}}
-\newcommand{\absent}{\emph{No such feature in \eacsl.}}
-\newcommand{\absentwhy}[1]{\emph{No such feature in \eacsl: #1.}}
-\newcommand{\absentexperimental}{\emph{No such feature in \eacsl, since it is
- still experimental in \acsl.}}
-\newcommand{\absentexcept}[1]{\emph{No such feature in \eacsl, but #1.}}
-\newcommand{\difficultwhy}[2]{\emph{#1 is usually difficult to implement, since
- it requires #2. Thus you would not wonder if most tools do not support it
- (or support it partially).}}
-\newcommand{\difficultswhy}[2]{\emph{#1 are usually difficult to implement,
- since they require #2. Thus you would not wonder if most tools do not
- support them (or support them partially).}}
-\newcommand{\difficult}[1]{\emph{#1 is usually difficult to implement. Thus
- you would not wonder if most tools do not support it (or support
- it partially).}}
-\newcommand{\difficults}[1]{\emph{#1 are usually difficult to implement. Thus
- you would not wonder if most tools do not support them (or support
- them partially).}}
-
-\newcommand{\changeinsection}[2]{\textbf{Section \ref{sec:#1}:} #2.}
-
-\newcommand{\todo}[1]{{\large \textbf{TODO: #1.}}}
-\newcommand{\option}[1]{\lstinline|#1|}
-
-\newcommand{\markdiff}[1]{{\color{blue}{#1}}}
-\newenvironment{markdiffenv}[1][]{%
- \begin{changebar}%
- \markdiff\bgroup%
-}%
-{\egroup\end{changebar}}
-
-% true = prints remarks for the ACSL working group.
-% false = prints no remark for the distributed version of ASCL documents
-\newboolean{PrintRemarks}
-\setboolean{PrintRemarks}{false}
-
-% true = prints marks signaling the state of the implementation
-% false = prints only the ACSL definition, without remarks on implementation.
-\newboolean{PrintImplementationRq}
-\setboolean{PrintImplementationRq}{true}
-
-% true = remarks about the current state of implementation in Frama-C
-% are in color.
-% false = they are rendered with an underline
-\newboolean{ColorImplementationRq}
-\setboolean{ColorImplementationRq}{true}
-
-%% \ifthenelse{\boolean{PrintRemarks}}%
-%% {\newenvironment{todo}{%
-%% \begin{quote}%
-%% \begin{tabular}{||p{0.8\textwidth}}TODO~:\itshape}%
-%% {\end{tabular}\end{quote}}}%
-%% {\excludecomment{todo}}
-
-\ifthenelse{\boolean{PrintRemarks}}%
- {\newenvironment{remark}[1]{%
- \begin{quote}\itshape%
- \begin{tabular}{||p{0.8\textwidth}}Remarque de {#1}~:}%
- {\end{tabular}\end{quote}}}%
- {\excludecomment{remark}}
-
-\newcommand{\oldremark}[2]{%
-\ifthenelse{\boolean{PrintRemarks}}{%
- %\begin{quote}\itshape%
- %\begin{tabular}{||p{0.8\textwidth}}Vieille remarque de {#1}~: #2%
- %\end{tabular}\end{quote}%
-}%
-{}}
-
-\newcommand{\highlightnotreviewed}{%
-\color{blue}%
-}%
-
-\newcommand{\notreviewed}[2][]{%
-\ifthenelse{\boolean{PrintRemarks}}{%
- \begin{changebar}%
- {\highlightnotreviewed #2}%
- \ifthenelse{\equal{#1}{}}{}{\footnote{#1}}%
- \end{changebar}%
-}%
-{}}
-
-\ifthenelse{\boolean{PrintRemarks}}{%
-\newenvironment{notreviewedenv}[1][]{%
- \begin{changebar}%
- \highlightnotreviewed%
- \ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
- \bgroup}%
- {\egroup%
- \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}}%
-{\excludecomment{notreviewedenv}}
-
-%%% Commandes et environnements pour la version relative à l'implementation
-\newcommand{\highlightnotimplemented}{%
-\ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
- {\ul}%
-}%
-
-\newcommand{\notimplemented}[2][]{%
-\ifthenelse{\boolean{PrintImplementationRq}}{%
- \begin{changebar}%
- {\highlightnotimplemented #2}%
- \ifthenelse{\equal{#1}{}}{}{\footnote{#1}}%
- \end{changebar}%
-}%
-{#2}}
-
-\newenvironment{notimplementedenv}[1][]{%
-\ifthenelse{\boolean{PrintImplementationRq}}{%
- \begin{changebar}%
- \highlightnotimplemented%
- \ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
- \bgroup
-}{}}%
-{\ifthenelse{\boolean{PrintImplementationRq}}{%
- \egroup%
- \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}{}}
-
-%%% Environnements et commandes non conditionnelles
-\newcommand{\experimental}{\textsc{Experimental}}
-
-\newsavebox{\fmbox}
-\newenvironment{cadre}
- {\begin{lrbox}{\fmbox}\begin{minipage}{0.98\textwidth}}
- {\end{minipage}\end{lrbox}\fbox{\usebox{\fmbox}}}
-
-
-\newcommand{\keyword}[1]{\lstinline|#1|\xspace}
-\newcommand{\keywordbs}[1]{\lstinline|\\#1|\xspace}
-
-\newcommand{\integer}{\keyword{integer}}
-\newcommand{\real}{\keyword{real}}
-\newcommand{\bool}{\keyword{boolean}}
-
-\newcommand{\assert}{\keyword{assert}}
-\newcommand{\terminates}{\keyword{terminates}}
-\newcommand{\assume}{\keyword{assume}}
-\newcommand{\requires}{\keyword{requires}}
-\newcommand{\ensures}{\keyword{ensures}}
-\newcommand{\exits}{\keyword{exits}}
-\newcommand{\returns}{\keyword{returns}}
-\newcommand{\breaks}{\keyword{breaks}}
-\newcommand{\continues}{\keyword{continues}}
-\newcommand{\assumes}{\keyword{assumes}}
-\newcommand{\assigns}{\keyword{assigns}}
-\newcommand{\reads}{\keyword{reads}}
-\newcommand{\decreases}{\keyword{decreases}}
-
-\newcommand{\boundseparated}{\keywordbs{bound\_separated}}
-\newcommand{\Exists}{\keywordbs{exists}~}
-\newcommand{\Forall}{\keywordbs{forall}~}
-\newcommand{\bslambda}{\keywordbs{lambda}~}
-\newcommand{\freed}{\keywordbs{freed}}
-\newcommand{\fresh}{\keywordbs{fresh}}
-\newcommand{\fullseparated}{\keywordbs{full\_separated}}
-\newcommand{\distinct}{\keywordbs{distinct}}
-\newcommand{\Max}{\keyword{max}}
-\newcommand{\nothing}{\keywordbs{nothing}}
-\newcommand{\numof}{\keyword{num\_of}}
-\newcommand{\offsetmin}{\keywordbs{offset\_min}}
-\newcommand{\offsetmax}{\keywordbs{offset\_max}}
-\newcommand{\old}{\keywordbs{old}}
-\newcommand{\at}{\keywordbs{at}}
-
-\newcommand{\If}{\keyword{if}~}
-\newcommand{\Then}{~\keyword{then}~}
-\newcommand{\Else}{~\keyword{else}~}
-\newcommand{\For}{\keyword{for}~}
-\newcommand{\While}{~\keyword{while}~}
-\newcommand{\Do}{~\keyword{do}~}
-\newcommand{\Let}{\keywordbs{let}~}
-\newcommand{\Break}{\keyword{break}}
-\newcommand{\Return}{\keyword{return}}
-\newcommand{\Continue}{\keyword{continue}}
-
-\newcommand{\exit}{\keyword{exit}}
-\newcommand{\main}{\keyword{main}}
-\newcommand{\void}{\keyword{void}}
-
-\newcommand{\struct}{\keyword{struct}}
-\newcommand{\union}{\keywordbs{union}}
-\newcommand{\inter}{\keywordbs{inter}}
-\newcommand{\typedef}{\keyword{typedef}}
-\newcommand{\result}{\keywordbs{result}}
-\newcommand{\separated}{\keywordbs{separated}}
-\newcommand{\sizeof}{\keyword{sizeof}}
-\newcommand{\strlen}{\keywordbs{strlen}}
-\newcommand{\Sum}{\keyword{sum}}
-\newcommand{\valid}{\keywordbs{valid}}
-\newcommand{\validrange}{\keywordbs{valid\_range}}
-\newcommand{\offset}{\keywordbs{offset}}
-\newcommand{\blocklength}{\keywordbs{block\_length}}
-\newcommand{\baseaddr}{\keywordbs{base\_addr}}
-\newcommand{\comparable}{\keywordbs{comparable}}
-
-\newcommand{\N}{\ensuremath{\mathbb{N}}}
-\newcommand{\ra}{\ensuremath{\rightarrow}}
-\newcommand{\la}{\ensuremath{\leftarrow}}
-
-% BNF grammar
-\newcommand{\indextt}[1]{\index{#1@\protect\keyword{#1}}}
-\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
-\newif\ifspace
-\newif\ifnewentry
-\newcommand{\addspace}{\ifspace ~ \spacefalse \fi}
-\newcommand{\term}[2]{\addspace\hbox{\lstinline|#1|%
-\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
-\newcommand{\nonterm}[2]{%
- \ifthenelse{\equal{#2}{}}%
- {\addspace\hbox{\textsl{#1}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}%
- {\addspace\hbox{\textsl{#1}\footnote{#2}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}}
-\newcommand{\repetstar}{$^*$\spacetrue}
-\newcommand{\repetplus}{$^+$\spacetrue}
-\newcommand{\repetone}{$^?$\spacetrue}
-\newcommand{\lparen}{\addspace(}
-\newcommand{\rparen}{)}
-\newcommand{\orelse}{\addspace$\mid$\spacetrue}
-\newcommand{\sep}{ \\[2mm] \spacefalse\newentrytrue}
-\newcommand{\newl}{ \\ & & \spacefalse}
-\newcommand{\alt}{ \\ & $\mid$ & \spacefalse}
-\newcommand{\is}{ & $::=$ & \newentryfalse}
-\newenvironment{syntax}{\begin{tabular}{@{}rrll@{}}\spacefalse\newentrytrue}{\end{tabular}}
-\newcommand{\synt}[1]{$\spacefalse#1$}
-\newcommand{\emptystring}{$\epsilon$}
-\newcommand{\below}{See\; below}
-
-% colors
-
-\definecolor{darkgreen}{rgb}{0, 0.5, 0}
-
-% theorems
-
-\newtheorem{example}{Example}[chapter]
-
-% for texttt
-
-\newcommand{\bs}{\ensuremath{\backslash}}
-
-% Index
-
-\newcommand{\optionidx}[2]{\index{#2@\texttt{#1#2}}}
-\newcommand{\codeidx}[1]{\index{#1@\texttt{#1}}}
-\newcommand{\scodeidx}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}}}
-\newcommand{\sscodeidx}[3]{%
- \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}}}
-\newcommand{\bfit}[1]{\textbf{\textit{\hyperpage{#1}}}}
-\newcommand{\optionidxdef}[2]{\index{#2@\texttt{#1#2}|bfit}}
-\newcommand{\codeidxdef}[1]{\index{#1@\texttt{#1}|bfit}}
-\newcommand{\scodeidxdef}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}|bfit}}
-\newcommand{\sscodeidxdef}[3]{%
- \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}|bfit}}
-
-\newcommand{\pragmadef}[1]{\texttt{#1}\index{Pragma!#1@\texttt{#1}}}
-\newcommand{\optiondef}[2]{\texttt{#1#2}\optionidxdef{#1}{#2}}
-\newcommand{\textttdef}[1]{\texttt{#1}\codeidxdef{#1}}
-
-\newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
-\newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
-\newcommand{\shortopt}[1]{\optionuse{-}{#1}}
-\newcommand{\longopt}[1]{\optionuse{{-}{-}}{#1}}
-% Shortcuts for truetype, italic and bold
-\newcommand{\T}[1]{\texttt{#1}}
-\newcommand{\I}[1]{\textit{#1}}
-\newcommand{\B}[1]{\textbf{#1}}
-
-\definecolor{gris}{gray}{0.85}
-\makeatletter
-\newenvironment{important}%
-{\hspace{5pt plus \linewidth minus \marginparsep}%
- \begin{lrbox}{\@tempboxa}%
- \begin{minipage}{\linewidth - 2\fboxsep}}
-{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Date
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Useful for today's short date
+\def\shorttoday{\leavevmode\hbox{\the\year-\twodigits\month-\twodigits\day}}
+\def\twodigits#1{\ifnum#1<10 0\fi\the#1}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Indexed Keywords
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Frama-C plug-in names (e.g., \plugin{Eva})
+\newcommand{\plugin}[1]{\textsf{#1}\xspace}
+
+% Tools (e.g., \tool{Why3})
+\newcommand{\tool}[1]{\textsf{#1}\xspace}
+
+% Languages (e.g., \lang{ACSL}, \lang{C})
+\newcommand{\lang}[1]{\textsf{#1}\xspace}
+
+% Libraries (e.g., \library{Gmp})
+\newcommand{\library}[1]{\textsf{#1}\xspace}
+
+% Benchmarks (e.g, \benchmark{SpecCPU})
+\newcommand{\benchmark}[1]{\textsf{#1}\xspace}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frama-C Related Names
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\FramaC}{\tool{Frama-C}}
+\newcommand{\acsl}{\lang{ACSL}}
+\newcommand{\eacsllang}{\lang{E-ACSL}}
+\newcommand{\acslpp}{\lang{ACSL++}}
+
+% plug-ins
+\newcommand{\aorai}{\plugin{Aora\"i}}
+\newcommand{\cafe}{\plugin{CaFE}}
+\newcommand{\callgraph}{\plugin{Callgraph}}
+\newcommand{\constfold}{\plugin{Consfold}}
+\newcommand{\dive}{\plugin{Dive}}
+\newcommand{\dominators}{\plugin{Dominators}}
+\newcommand{\eacsl}{\plugin{E-ACSL}}
+\newcommand{\Eva}{\plugin{Eva}}
+\newcommand{\framaclang}{\plugin{Frama-Clang}}
+\newcommand{\from}{\plugin{From}}
+\newcommand{\GUI}{\plugin{GUI}}
+\newcommand{\impact}{\plugin{Impact}}
+\newcommand{\inout}{\plugin{InOut}}
+\newcommand{\instantiate}{\plugin{Instantiate}}
+\newcommand{\ltest}{\plugin{LTest}}
+\newcommand{\mdr}{\plugin{MdR}}
+\newcommand{\metacsl}{\plugin{MetAcsl}}
+\newcommand{\metrics}{\plugin{Metrics}}
+\newcommand{\nonterm}{\plugin{NonTerm}}
+\newcommand{\obfuscator}{\plugin{Obfuscator}}
+\newcommand{\occurrence}{\plugin{Occurrence}}
+\newcommand{\pathcrawler}{\plugin{PathCrawler}}
+\newcommand{\pdg}{\plugin{Pdg}}
+\newcommand{\pilat}{\plugin{Pilat}}
+\newcommand{\postdominators}{\plugin{Postdominators}}
+\newcommand{\printinterface}{\plugin{PrintInterface}}
+\newcommand{\reduction}{\plugin{Reduction}}
+\newcommand{\report}{\plugin{Report}}
+\newcommand{\rpp}{\plugin{RPP}}
+\newcommand{\rte}{\plugin{Rte}}
+\newcommand{\scope}{\plugin{Scope}}
+\newcommand{\secureflow}{\plugin{SecureFlow}}
+\newcommand{\securityslicing}{\plugin{SecuritySlicing}}
+\newcommand{\server}{\plugin{Server}}
+\newcommand{\slicing}{\plugin{Slicing}}
+\newcommand{\sparecode}{\plugin{SpareCode}}
+\newcommand{\stady}{\plugin{StaDy}}
+\newcommand{\studia}{\plugin{Studia}}
+\newcommand{\users}{\plugin{Users}}
+\newcommand{\variadic}{\plugin{Variadic}}
+\newcommand{\Wp}{\plugin{WP}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Standard Keywords
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Some programming languages
+\newcommand{\ada}{\lang{Ada}}
+\newcommand{\awk}{\lang{Awk}}
+\newcommand{\C}{\lang{C}}
+\newcommand{\coq}{\lang{Coq}}
+\newcommand{\Cpp}{\lang{C++}}
+\newcommand{\csharp}{\lang{C\#}}
+\newcommand{\dafny}{\lang{Dafny}}
+\newcommand{\dotnet}{\lang{.NET}}
+\newcommand{\eiffel}{\lang{Eiffel}}
+\newcommand{\fortran}{\lang{Fortran}}
+\newcommand{\isabelle}{\lang{Isabelle}}
+\newcommand{\java}{\lang{Java}}
+\newcommand{\javacard}{\lang{JavaCard}}
+\newcommand{\K}{\ensuremath{\mathbb{K}}}
+\newcommand{\ocaml}{\lang{OCaml}}
+\newcommand{\php}{\lang{PHP}}
+\newcommand{\python}{\lang{Python}}
+\newcommand{\smalltalk}{\lang{Smalltalk}}
+\newcommand{\spark}{\lang{Spark2014}}
+\newcommand{\vbnet}{\lang{VB.NET}}
+
+% Some modeling languages
+\newcommand{\lustre}{\lang{Lustre}}
+\newcommand{\scade}{\lang{Scade}}
+\newcommand{\simulink}{\lang{Simulink}}
+
+% Some specification languages
+\newcommand{\codecontract}{\lang{Code Contract}}
+\newcommand{\ltl}{\lang{LTL}}
+\newcommand{\jml}{\lang{JML}}
+\newcommand{\specsharp}{\lang{Spec\#}}
+\newcommand{\vcc}{\lang{VCC}}
+
+% Some libraries
+\newcommand{\cil}{\library{Cil}}
+\newcommand{\gtk}{\library{Gtk2}}
+\newcommand{\gtkt}{\library{Gtk3}}
+\newcommand{\gmp}{\library{Gmp}}
+\newcommand{\lablgtk}{\library{LablGtk2}}
+\newcommand{\lablgtkt}{\library{LablGtk3}}
+\newcommand{\libc}{\library{libc}}
+\newcommand{\libtomcrypt}{\library{LibTomCrypt}}
+
+% Some analysis and verification tools
+\newcommand{\addresssanitizer}{\tool{AddressSanitizer}}
+\newcommand{\aiT}{\tool{aiT}}
+\newcommand{\astree}{\tool{Astr\'ee}}
+\newcommand{\caduceus}{\tool{Caduceus}}
+\newcommand{\drmemory}{\tool{Dr.~Memory}}
+\newcommand{\insurepp}{\tool{Insure++}}
+\newcommand{\memcheck}{\tool{MemCheck}}
+\newcommand{\memorysanitizer}{\tool{MemorySanitizer}}
+\newcommand{\memsanitizer}{\tool{MemorySanitizer}}
+\newcommand{\openjml}{\tool{OpenJML}}
+\newcommand{\polyspace}{\tool{PolySpace}}
+\newcommand{\purify}{\tool{Purify}}
+\newcommand{\rvmatch}{\tool{RV-Match}}
+\newcommand{\stackanalyzer}{\tool{Stackanalyzer}}
+\newcommand{\threadsanitizer}{\tool{ThreadSanitizer}}
+\newcommand{\undefsanitizer}{\tool{UndefinedBehaviorSanitizer}}
+\newcommand{\valgrind}{\tool{Valgrind}}
+\newcommand{\verasco}{\tool{Verasco}}
+\newcommand{\why}{\tool{Why}}
+\newcommand{\whyt}{\tool{Why3}}
+
+% Some other tools
+\newcommand{\altergo}{\tool{Alt-Ergo}}
+\newcommand{\clang}{\tool{Clang}}
+\newcommand{\clousot}{\tool{Clousot}}
+\newcommand{\compcert}{\tool{CompCert}}
+\newcommand{\gcc}{\tool{Gcc}}
+\newcommand{\gdb}{\tool{gdb}}
+\newcommand{\git}{\tool{Git}}
+\newcommand{\llvm}{\tool{LLVM}}
+\newcommand{\opam}{\tool{opam}}
diff --git a/doc/userman/main.tex b/doc/userman/main.tex
index 2b8fd10c57c05c138e4801ecfca7c59825473cea..dd88919b16f5da4de5179eb08c53d6aa37acfa87 100644
--- a/doc/userman/main.tex
+++ b/doc/userman/main.tex
@@ -1,5 +1,5 @@
\documentclass{frama-c-book}
-\usepackage{graphicx}
+\usepackage{makeidx}
\usepackage{calc}
\usepackage{datetime}
\newdateformat{ddMyyyydate}{\THEDAY~\monthname[\THEMONTH]~\THEYEAR}
@@ -7,41 +7,28 @@
\input{macros.tex}
\input{fclangversion.tex}
+\newcommand{\irg}{\tool{framaCIRGen}}
+
\makeindex
-\begin{document}
+\title{\framaclang Plug-in User Manual}
+\subtitle{%
+version \version\\[.3em]
+for \FramaC version \framacversion}
+
+\author{David~R.~Cok}
+
+\acknowledge{Virgile Prevosto}
+\acknowledge{Armand Puccetti}
+\acknowledge{Franck Védrine}
+
+\copyrightstarts{2013}
+\cclicence{by-sa}
-\coverpage{ \vbox{
-\centerline{\fclang User Manual}
-\vspace{.3em}
-\centerline{\normalsize{version \version}}
-\vspace{.3em}
-\centerline{\normalsize{for \fclang version \fclangversion}}
-\vspace{.3em}
-\centerline{\normalsize{and \framac version \fcversion}}
-}}
-
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{\fclang Plug-in User Manual}{\fclang \fclangversion}
-\author{David R. Cok}
-\begin{center}
-CEA LIST\\ Software Safety \& Security Laboratory
-\end{center}
-\begin{center}
- Document printed \ddMyyyydate\today
-\end{center}
-\vfill
-\begin{flushleft}
- \textcopyright 2013-2022 CEA List
-%%
- %% This work has been supported by the VESSEDIA project).
-\end{flushleft}
-\end{titlepage}
+\begin{document}
+
+\maketitle
\tableofcontents
@@ -51,25 +38,20 @@ CEA LIST\\ Software Safety \& Security Laboratory
\markright{}
\addcontentsline{toc}{chapter}{Foreword}
-This is the user manual for the \framac plug-in
-\fclang.\footnote{\url{https://frama-c.com/frama-clang.html}}
+This is the user manual for the \FramaC plug-in
+\framaclang.\footnote{\url{https://frama-c.com/frama-clang.html}}
The contents of this
document correspond to version \fclangversion of the plug-in compatible with the
-\fcversion version of \framac~\cite{userman,fac15}. The development of
-the \fclang plug-in is still ongoing. Features described by this document will certainly
+\framacversion version of \FramaC~\cite{userman,baudinCACM21}. The development of
+the \framaclang plug-in is still ongoing. Features described by this document will certainly
evolve in the future.
\section*{Acknowledgements}
-We gratefully thank the people who contributed to this document:
-David R. Cok, Virgile Prevosto, Armand Puccetti, Franck Védrine.
-
-This document was initially written in the context of project VESSEDIA,
-which received funding from the European Union's 2020
-Research and Innovation Program under grant agreement
-No. 731453.
-
-
+\insertpeople
+\\[1em]
+\acknowledgeEU{the European Union's Horizon 2020 Programme
+ under grant agreement N°\,731453 (VESSEDIA)}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -94,9 +76,9 @@ No. 731453.
% \item Add/revise list of contributors/reviewers
% \item permanent location of source documents
% \item generation of doxygen
-% \item (Introduction) Verify the version of \framac and \clang supported
+% \item (Introduction) Verify the version of \FramaC and \clang supported
% \item Sort out the interactions among the options -verbose -debug -quiet -fclang-debug -fclang-verbose -fclang-msg-key -fclang-warn-key
-% \item -no-pp-annot is not recognized by \fclang
+% \item -no-pp-annot is not recognized by \framaclang
% \item Add comments about using system header files
% \item Comment on the demangling options
% \item Review the clang and \irg options
diff --git a/doc/userman/preprocessing.tex b/doc/userman/preprocessing.tex
index c22376565b8ae63e0b82827c35ecf32506036c26..5bbf9486526bfb913b3c1fe1780cb8529ff25129 100644
--- a/doc/userman/preprocessing.tex
+++ b/doc/userman/preprocessing.tex
@@ -1,18 +1,18 @@
\chapter{Preprocessing}
\label{sec:preprocessing}
-This section describes the implementation of the \cpp preprocessor for \acslpp
-annotations. Recall that the \cpp preprocessor replaces comments (including
+This section describes the implementation of the \Cpp preprocessor for \acslpp
+annotations. Recall that the \Cpp preprocessor replaces comments (including
\acslpp comments) by white space, without operations such as handling
-preprocessor directives. Accordingly, \fclang must handle standard
+preprocessor directives. Accordingly, \framaclang must handle standard
preprocessing within \acslpp annotations itself.
-As a refresher, the \C/\cpp preprocessor (CPP) (cf. \url{https://gcc.gnu.org/onlinedocs/cpp/}) conceptually implements the following operations on a \cpp source file:
+As a refresher, the \C/\Cpp preprocessor (CPP) (cf. \url{https://gcc.gnu.org/onlinedocs/cpp/}) conceptually implements the following operations on a \Cpp source file:
\begin{itemize}
\item The input is translated into a basic set of characters, including replacing trigraph sequences by their source character set equivalents
\item Any backslash-whitespace-line-terminator sequence is removed and the line that it ends is combined with the following line, producing a sequence of logical lines.
\item Comments are replaced by single spaces. This requires tokenizing the input to avoid recognizing comment markers within strings as indicating a comment. Note that this allows block comments to hide line terminations.
- \item The input text is divided into preprocessing tokens grouped in logical lines. Each preprocessor token becomes a compiler token (except where \#\# concatenation occurs). However, \acslb tokens are slightly different, as described below.
+ \item The input text is divided into preprocessing tokens grouped in logical lines. Each preprocessor token becomes a compiler token (except where \#\# concatenation occurs). However, \acslpp tokens are slightly different, as described below.
\item The source text is transformed according to any preprocessing directives contained within it.
Each preprocessing directive must be contained within one logical line. The result has no preprocessing directives remaining.
\item Adjacent string literals (separated only by white-space or line-endings) are concatenated into a single string literal.
@@ -21,21 +21,21 @@ As a refresher, the \C/\cpp preprocessor (CPP) (cf. \url{https://gcc.gnu.org/onl
The result is a sequence of preprocessing tokens that is passed on to the
remaining compiler phases.
-\section{\fclang preprocessor implementation}
-The \fclang implementation operates as follows, on each \acslpp annotation comment in turn:
+\section{\framaclang preprocessor implementation}
+The \framaclang implementation operates as follows, on each \acslpp annotation comment in turn:
\begin{itemize}
\item A simplified custom lexer converts the text into preprocessor tokens, without doing macro substitution, to find instances of forbidden preprocessor directives. If possible and reasonable, these are elided from the input text and processing continues.
-\item The text is then submitted to \cl to obtain the complete sequence of preprocessor tokens, now with full preprocessing (except for adjacent string concatenation).
-\item \fcl transforms the clang preprocessor tokens into \acslpp tokens, which are then passed on to the \acslpp parser to produce the desired AST.
+\item The text is then submitted to \clang to obtain the complete sequence of preprocessor tokens, now with full preprocessing (except for adjacent string concatenation).
+\item \framaclang transforms the clang preprocessor tokens into \acslpp tokens, which are then passed on to the \acslpp parser to produce the desired AST.
\end{itemize}
\section{Trigraphs}
-Trigraphs are defined for \cpp but will currently be removed in C++17. Since trigraph processing by clang occurs before any recognition of comments, trigraphs in \acslpp annotations are translated, if enabled in \clang. As they will be removed from \cpp, they are not recommended for use in \acslpp annotations. Preprocessing of trigraphs is enabled by default.
+Trigraphs are defined for \Cpp but will currently be removed in C++17. Since trigraph processing by clang occurs before any recognition of comments, trigraphs in \acslpp annotations are translated, if enabled in \clang. As they will be removed from \Cpp, they are not recommended for use in \acslpp annotations. Preprocessing of trigraphs is enabled by default.
\section{Digraphs}
Digraphs are alternate spellings of preprocessor tokens, in particular, of
-punctuation character sequences. Digraphs in \acslpp annotations are translated just as they are in \cpp (by \clang).
+punctuation character sequences. Digraphs in \acslpp annotations are translated just as they are in \Cpp (by \clang).
Using digraphs is not recommended.
\section{Preprocessor tokens}
@@ -53,15 +53,15 @@ becomes a compiler token, which then may be an illegal compiler token.
The token definitions imply that arbitrary text can always be broken into
legitimate preprocessor tokens, with the exception of a few characters and of badly formed unicode sequences.
-Note that not all preprocessor tokens are valid \C/\cpp parser tokens. Tokens in the other category have no meaning to \C/\cpp and the \texttt{number} category allows many sequences that are not legal \C/\cpp numeric tokens. These tokens will generally provoke compiler errors. For example in \C/\cpp, 0..2 is one token and is not interpreted as two consecutive numeric tokens.
+Note that not all preprocessor tokens are valid \C/\Cpp parser tokens. Tokens in the other category have no meaning to \C/\Cpp and the \texttt{number} category allows many sequences that are not legal \C/\Cpp numeric tokens. These tokens will generally provoke compiler errors. For example in \C/\Cpp, 0..2 is one token and is not interpreted as two consecutive numeric tokens.
\acsl and \acslpp have slightly different tokens than the preprocessor, so the preprocessor tokens need to be re-tokenized in some cases:
\begin{itemize}
- \item The \verb|@| token is a whitespace character in the interior of a \acslb annotation.
- \item There are some \acslb multi-character punctuator tokens that are not
+ \item The \verb|@| token is a whitespace character in the interior of a \acslpp annotation.
+ \item There are some \acslpp multi-character punctuator tokens that are not
single preprocessor tokens:
\begin{itemize}
- \item all \acslb keywords that begin with a backslash, such as \verb|\result|.
+ \item all \acslpp keywords that begin with a backslash, such as \verb|\result|.
\item \verb|==>| (logical implies)
\item \verb|-->| (bit-wise implies)
\item \verb|<==>| (logical equality)
@@ -70,14 +70,14 @@ Note that not all preprocessor tokens are valid \C/\cpp parser tokens. Tokens in
\item \verb|^*| (list repetition)
\item \verb:[|: and \verb:|]: (list creation)
\end{itemize}
- These \acslb tokens need to be assembled from multiple CPP tokens (and those CPP tokens must not be separated by white space)
- \item A CPP numeric token that contains .. will not be a legal \C/\cpp number, but may be a sequence of
- legal \acslb tokens with the .. representing the range operator. For example, the single CPP token \texttt{0..last} is retokenized for \acslb as if it were written \texttt{0 .. last} .
- \item \acslb allows certain built-in non-ASCII symbols.
+ These \acslpp tokens need to be assembled from multiple CPP tokens (and those CPP tokens must not be separated by white space)
+ \item A CPP numeric token that contains .. will not be a legal \C/\Cpp number, but may be a sequence of
+ legal \acslpp tokens with the .. representing the range operator. For example, the single CPP token \texttt{0..last} is retokenized for \acslpp as if it were written \texttt{0 .. last} .
+ \item \acslpp allows certain built-in non-ASCII symbols.
An example is
$\forall$ (unicode 0x2200) to designate a universal quantifier,
which is an alternative form of \verb|\forall|.
- A complete list of such tokens is given in the \acslb language definition.
+ A complete list of such tokens is given in the \acslpp language definition.
\end{itemize}
\section{Preprocessor directives}
@@ -93,8 +93,8 @@ The preprocessing language contains a fixed set of preprocessing directive ident
\end{itemize}
In addition, identifiers that have been defined (by a \texttt{\#define} directive) as macros are expanded according to the macro expansion rules (not described here).
-Because \acslb annotations are contained in \C/\cpp comments,
-any directives contained in the annotation are not seen when the source file is processed simply as a \C/\cpp source file. However, the effect of some directives lasts until the end of the source file.
+Because \acslpp annotations are contained in \C/\Cpp comments,
+any directives contained in the annotation are not seen when the source file is processed simply as a \C/\Cpp source file. However, the effect of some directives lasts until the end of the source file.
Accordingly, \acslpp imposes constraints on the directives that may be present within annotations:
\begin{itemize}
\item \texttt{define} and \texttt{undef} are not permitted in an annotation. (If they were to be allowed, their scope would have to extend only to the end of the annotation, which could be confusing to readers.)
@@ -109,7 +109,7 @@ Accordingly, \acslpp imposes constraints on the directives that may be present w
\item stringizing (\verb|#|) and string concatenation (\verb|##|) operators are permitted
\item the \verb|defined| operator is permitted
\item the standard predefined macro names are permitted:
- \texttt{\_\_cpluscplus} (in \cpp compilers),
+ \texttt{\_\_cpluscplus} (in \Cpp compilers),
\texttt{\_\_DATE\_\_},
\texttt{\_\_TIME\_\_},
\texttt{\_\_FILE\_\_},