[Doc] Userman: review and update initial sections

doc/userman/user-overview.tex

@@ -8,10 +8,12 @@
 a single collaborative extensible framework. The collaborative approach of
 \FramaC allows analyzers to build upon the results already computed by
 other analyzers in the framework. Thanks to this approach, \FramaC can provide
-a number of sophisticated tools such as a slicer~\cite{slicing}, and a dependency
-analyzer~\cite[Chap.~6]{value}.
+a number of sophisticated tools such as a concurrency safety analysis
+(Mthread~\cite{mthread}),
+an enforcer of secure information flow (SecureFlow~\cite{secureflow1,secureflow2}),
+or a coverage-based test generator (LTest~\cite{ltest}), among many others.
 
-\section{\FramaC as a Static Analysis Tool}
+\section{\FramaC as a Code Analysis Tool}
 
 \emph{Static analysis} of source code is the science of computing synthetic
 information about the source code without executing it.
@@ -34,7 +36,7 @@ where an error can happen at run-time. And it allows its user to manipulate
 \emph{functional specifications}, and to \emph{prove} that the source code
 satisfies these specifications.
 
-\FramaC is not the only correct static analyzer out there, but analyzers of the
+\FramaC is not the only correct code analyzer out there, but analyzers of the
 \emph{correct} family are less widely known and used. Software metrics tools do
 not guarantee anything about the behavior of the program, only about the way it
 is written. Heuristic bug-finding tools can be very useful, but because they do
@@ -48,6 +50,20 @@ require comparatively little intervention from the user, and the collaborative
 approach proposed in \FramaC allows the user to get results about complex
 semantic properties.
 
+\FramaC also provides some {\em dynamic analysis}, via plug-ins such as
+\tool{E-ACSL}~\cite{eacsl}, which performs {\em runtime verification}.
+It is often used as a complement to static analysis: when some properties
+cannot be proven statically, \tool{E-ACSL} instruments the code so that,
+during execution, such properties are verified and {\em enforced}:
+violations lead to alerts or immediate termination, preventing silent program
+corruption or malicious infiltration, and helping pinpoint the exact cause
+of a problem, instead of an indirect consequence much later.
+
+For both static and dynamic analyses, \FramaC focuses on the {\em source code}.
+Plug-ins can help translate higher-level properties and specifications, or
+even provide front-ends to other languages; but, in the end, the strength of
+the platform is centered around the code and its properties.
+
 \subsection{\FramaC as a Lightweight Semantic-Extractor Tool}
 
 \FramaC analyzers, by offering the possibility to extract semantic information
@@ -94,7 +110,9 @@ review.
 \section{\FramaC as a Tool for \C programs}
 
 The \C source code analyzed by \FramaC is assumed to follow the \tool{C99} ISO
-standard\index{C99 ISO standard@\tool{C99} ISO standard}. \C comments may
+standard\index{C99 ISO standard@\tool{C99} ISO standard}\footnote{Some common
+GCC extensions, as well as some parts of the \tool{C11} standard, are
+also supported.}. \C comments may
 contain \acsl annotations~\cite{acsl} used as specifications to be interpreted
 by \FramaC. The subset of \acsl currently interpreted in \FramaC is described
 in~\cite{acsl-implem}.
@@ -106,7 +124,7 @@ plug-in's documentation.
 \section{\FramaC as an Extensible Platform}
 
 \FramaC is organized into a modular architecture (comparable to that of the
-\tool{Gimp} or \tool{Eclipse}): each analyzer comes in the form of a
+\tool{Eclipse} IDE): each analyzer comes in the form of a
 \emph{plug-in} and is connected to the platform itself, or \emph{kernel}, which
 provides common functionalities and collaborative data structures.
 
@@ -115,17 +133,17 @@ manual covers the set of features common to all plug-ins, plus some plug-ins
 which are used by several others, such as the graphical user interface
 (\GUI) and reporting tools (\Report).
 It does not cover use of the plug-ins that come in the \FramaC
-distribution: value analysis (\Value), functional dependencies (\From),
-functional verification (\WP), program slicing (\Slicing), \etc.
+distribution: value analysis (\Value), functional verification (\WP),
+runtime verification (\tool{E-ACSL}), \etc.
 Each of these analyses has its own specific
-documentation~\cite{value,wp,slicing}.
+documentation~\cite{value,wp,eacsl}.
 
 Additional plug-ins can be provided by third-party developers and installed
 separately from the kernel. \FramaC is thus not limited to the set of analyses
-initially installed. For instance, it may be extended with the \tool{E-ACSL}
-plug-in~\cite{eacsl,sac13} which instruments the program in order to check annotations
-at runtime. In this way, \FramaC is not restricted to static analysis of source
-code, but also provides dynamic analysis.
+initially installed. For instance, it may be extended with the \tool{Frama-Clang}
+plug-in~\cite{framaclang}, which provides a front-end for C++ code;
+or \tool{MetAcsl}~\cite{metacsl}, which allows specifying higher-level
+meta-properties; among others.
 
 \section{\FramaC as a Collaborative Platform}
 

doc/userman/user-start.tex

@@ -41,7 +41,7 @@ and running \FramaC are described below.
 \item[A \C compiler]\index{C compiler} is required to compile the \FramaC
   kernel.
 \item[A \tool{Unix}-like compilation environment] with at least the tool
-  \texttt{GNU make}\footnote{\url{http://www.gnu.org/software/make}},
+  \texttt{GNU make}\footnote{\url{http://www.gnu.org/software/make}} $\ge 4.0$,
   as well as various POSIX commands, libraries and header files, is necessary
   for compiling \FramaC and its plug-ins.
 \item[The \caml compiler]\index{OCaml compiler}\footnote{\url{http://ocaml.org}}
@@ -55,54 +55,60 @@ etc., are listed in the \texttt{INSTALL.md} and \texttt{opam/opam} files.
 
 \section{One Framework, Several Executables}\label{sec:modes}
 
-\FramaC installs some executables\footnote{On Windows OS, the
-  usual extension \texttt{.exe} is added to each file name.}, namely:
+The main executables installed by \FramaC are:
+
+\begin{itemize}
+\item \texttt{frama-c}\codeidx{frama-c}: batch version (command line);
+\item \texttt{frama-c-gui}\codeidx{frama-c-gui}: interactive version (graphical interface).
+\end{itemize}
+
+\begin{description}
+\item[Batch version]\index{Batch version}
+
+  The \texttt{frama-c} binary can be used to perform most \FramaC analyses:
+  from parsing the sources to running complex analyses, on-demand or as part
+  of a continuous integration pipeline. Many analyses can display their output
+  in simple text form, but some structured results (HTML, CSV or JSON) are
+  also available. For instance, a SARIF~(see Section~\ref{sarif}) output
+  based on JSON is can be produced by the \tool{Markdown Report} plug-in.
+  While the batch version is very powerful, it does not offer the visualization
+  features of the interactive version.
+
+\item[Interactive version]\index{Interactive version}
+  The interactive version is a GUI that can be used to select the set of files
+  to analyze, specify options, launch analyses, browse the code and observe
+  analysis results at one's convenience (see Chapter~\ref{user-gui} for
+  details). For instance, you can hover over an expression in the code and
+  obtain immediate syntactic and semantic information about it; or use context
+  menus for easy code navigation.
+  However, the initial analysis setup (especially parsing) can be complex for
+  some projects, and the batch version is better suited for providing error
+  messages at this stage.
+
+\end{description}
+
+Both versions are complementary: the batch version is recommended
+for initial setup and analysis, while the interactive version is recommended for
+results visualization and interactive proofs.
+
+Besides these two executables, \FramaC also provides a few other command line
+binaries:
 \begin{itemize}
-\item \texttt{frama-c}\codeidx{frama-c}: natively-compiled batch version;
-\item \texttt{frama-c.byte}\codeidx{frama-c.byte}: bytecode batch version;
-\item \texttt{frama-c-gui}\codeidx{frama-c-gui}: natively-compiled interactive
-  version;
-\item \texttt{frama-c-gui.byte}\codeidx{frama-c-gui.byte}: bytecode interactive version;
 \item \texttt{frama-c-config}\codeidx{frama-c-config}: auxiliary batch version for
-  quickly retrieving configuration information (e.g. installation path);
+  quickly retrieving configuration information (e.g. installation paths);
+  it is only useful for scripting and running a large amount of analyses;
 \item \texttt{frama-c-script}\codeidx{frama-c-script}: contains several
   utilities related to source preparation, results visualization and analysis
   automation. Run it without arguments to obtain more details.
 \end{itemize}
-The differences between these versions are described below.
-\begin{description}
-\item[\emph{native-compiled \emph{vs} bytecode}:]
-  \index{Native-compiled|bfit}\index{Bytecode|bfit} native executables contain
-  machine code, while bytecode executables contain machine-independent
-  instructions which are run by a bytecode interpreter.
-
-  The native-compiled version is usually ten times faster than the bytecode one.
-  The bytecode is sometimes able to provide better debugging information.
-  Use the native-compiled version unless you have a specific reason to use the
-  bytecode one.
-
-\item[\emph{batch \emph{vs} interactive}:]\index{Batch
-    version}\index{Interactive version} The interactive version is a
-  GUI that can be used to select the set of files to analyze, specify
-  options, launch analyses, browse the code and observe analysis
-  results at one's convenience (see Chapter~\ref{user-gui} for details).
-
-  With the batch version, all settings and actions
-  must be provided on the command-line. This is not possible for all plug-ins,
-  nor is it always easy for beginners.
-  Modulo the limited user interactions, the batch version allows
-  the same analyses as the interactive version\footnote{For a single analysis
-    project. Multiple projects can only be handled in the interactive version
-   or programmatically. See Section~\ref{sec:project}}.
-  A batch analysis session consists in launching \FramaC in a
-  terminal. Results are printed on the standard output.
-
-  The task of analyzing some \C code being iterative and error-prone,
-  \FramaC provides functionalities to set up an analysis project,
-  observe preliminary results, and progress until a complete and
-  satisfactory analysis of the desired code is obtained.
 
-\end{description}
+Finally, note that the two main binaries (\texttt{frama-c} and
+\texttt{frama-c-gui} are also provided in {\em bytecode} version, as
+\texttt{frama-c.byte} and \texttt{frama-c-gui.byte}.
+\index{Native-compiled|bfit}\index{Bytecode|bfit}
+The bytecode is sometimes able to provide better debugging information;
+but since the native-compiled version is usually much faster (10x),
+use the latter unless you have a specific reason to use the bytecode one.
 
 \section{\FramaC Command Line and General Options}\index{Options}
 
@@ -145,6 +151,11 @@ all documented with \texttt{-kernel-h}:
 
 There are many aliases for these options, but for backward compatibility purposes only.
 Those listed above should be used for scripting.
+Note that, for all of these options except \texttt{-plugins},
+you can use \texttt{frama-c-config} (instead of \texttt{frama-c}),
+which offers faster loading times.
+This is unnecessary for occasional usage, but when running hundreds of
+instances of short analyses on \FramaC, the difference is significant.
 
 For a more thorough display of configuration-related data, in JSON format,
 use option \optiondef{-}{print-config-json}. Note that the data output by this

doc/userman/userman.bib

@@ -109,3 +109,65 @@ note={Extended version of \cite{sefm12}},
   author = {Julien Signoles and Basile Desloges and Kostyantyn Vorobyov},
   note   = {\url{https://frama-c.com/fc-plugins/e-acsl.html}},
 }
+
+@inproceedings{secureflow1,
+  author = {Gerg\"o Barany and Julien Signoles},
+  title  = {{Hybrid Information Flow Analysis for Real-World C Code}},
+  booktitle  = {International Conference on Tests and Proofs (TAP'17)},
+  year   = 2017,
+  month  = jul,
+}
+
+@phdthesis{secureflow2,
+  author = {Mounir Assaf},
+  title  = {{From Qualitative to Quantitative Program Analysis:
+ Permissive Enforcement of Secure Information Flow}},
+  year   = 2015,
+  month  = may,
+  school = {Universit\'e Rennes 1},
+}
+
+@article{ltest,
+  TITLE = {{Detection of Polluting Test Objectives for Dataflow Criteria}},
+  AUTHOR = {Martin, Thibault and Kosmatov, Nikolai and Pr{\'e}vosto, Virgile and Lemerre, Matthieu},
+  URL = {https://hal-cea.archives-ouvertes.fr/cea-02974228},
+  NOTE = {International Conference on Integrated Formal Methods 2020-11-16/20, Lugano, Suisse},
+  JOURNAL = {{Lecture Notes in Computer Science}},
+  PUBLISHER = {{Springer}},
+  NUMBER = {12546},
+  YEAR = {2020},
+  PDF = {https://hal-cea.archives-ouvertes.fr/cea-02974228/file/main.pdf},
+  HAL_ID = {cea-02974228},
+  HAL_VERSION = {v1},
+}
+
+@manual{mthread,
+  author = {Boris Yakobowski and Richard Bonichon},
+  title  = {{Frama-C}'s {Mthread} plug-in},
+  year   = 2012,
+  note   = {\mbox{\url{http://frama-c.com/download/frama-c-mthread-manual.pdf}}},
+}
+
+@manual{framaclang,
+  author = {David Cok},
+  title  = {{Frama-C}'s {Frama-Clang} plug-in},
+  year   = 2021,
+  note   = {\mbox{\url{https://www.frama-c.com/download/frama-clang-manual.pdf}}},
+}
+
+@inproceedings{metacsl,
+  TITLE = {{MetAcsl: Specification and Verification of High-Level Properties}},
+  AUTHOR = {Robles, Virgile and Kosmatov, Nikolai and Pr{\'e}vosto, Virgile and Rilling, Louis and Le Gall, Pascale},
+  URL = {https://hal-cea.archives-ouvertes.fr/cea-02019790},
+  BOOKTITLE = {{TACAS 2019}},
+  ADDRESS = {Prague, Czech Republic},
+  SERIES = {LNCS},
+  VOLUME = {11427},
+  YEAR = {2019},
+  MONTH = Apr,
+  DOI = {10.1007/978-3-030-17462-0\_22},
+  KEYWORDS = {Frama-C ; meta-properties ; deductive verification ; formal specification},
+  PDF = {https://hal-cea.archives-ouvertes.fr/cea-02019790/file/main.pdf},
+  HAL_ID = {cea-02019790},
+  HAL_VERSION = {v1},
+}