Merge branch 'stable/chromium'

ALL_VERSIONS

 Version number			Date of release		Notes
 ==============			===============		=====
+24.0 (Chromium)                 2021, November 30
 23.1 (Vanadium)                 2021, July 20
 23.0 (Vanadium)                 2021, July 7
 22.0 (Titanium)                 2020, November 17

VERSION

-24.0-beta+dev
+24.0+dev

doc/userman/user-changes.tex

@@ -3,6 +3,11 @@
 This chapter summarizes the changes in this documentation between each \FramaC
 release. First we list changes of the last release.
 
+\section*{24.0 (Chromium)}
+\begin{itemize}
+\item \textbf{Standard library (libc):} Section added
+\end{itemize}
+
 \section*{23.0 (Vanadium)}
 
 \begin{itemize}

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 set of tools for various test coverage criteria (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 parts of
+the \tool{C11} standard, as well as some common GCC extensions,
+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 an experimental 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-sources.tex

@@ -113,7 +113,8 @@ is set by default). Unless a custom preprocessor is specified
 installed and uses it as preprocessor.
 If you do \emph{not} want annotations to be preprocessed, you need to pass
 option \texttt{-no-pp-annot} to \FramaC. Note that some headers in the
-standard C library provided with \FramaC (described below) use such annotations,
+standard C library provided with \FramaC (described in Section~\ref{sec:libc})
+use such annotations,
 therefore it might be necessary to disable inclusion of such headers.
 
 Also note that ACSL annotations are preprocessed separately from the C
@@ -131,20 +132,6 @@ preprocessing for ACSL annotations only. Those files may contain
 the previous paragraph. This allows to have macros in ACSL annotations while
 using a non-GNU-like preprocessor.
 
-\begin{important}
-  An experimental, incomplete, C standard library is bundled with \FramaC and installed
-  in the sub-directory \texttt{libc} of the directory printed by
-  \texttt{frama-c -print-share-path}. It contains standard \C headers,
-  some \acsl specifications and definitions for some library functions.
-  By default, these headers are used instead of the standard library ones:
-  option \optiondef{-}{frama-c-stdlib} (set by default) adds
-  \texttt{-I\$FRAMAC\_SHARE/libc} to the preprocessor command, and also
-  \texttt{-nostdinc} if \optionuse{-}{cpp-frama-c-compliant} is set.
-  Note that this library is provided on a best-effort basis, but it is part
-  of the {\em trusted computing base}: the specifications must be proofread
-  for correctness.
-\end{important}
-
 \section{Merging the Source Code files}
 
 After preprocessing, \FramaC parses, type-checks and links the source
@@ -427,6 +414,58 @@ indicate the option needed to allow the file to be parsed:
          allowed in C11 (option -c11).
 \end{verbatim}
 
+\section{Standard library (libc)}\label{sec:libc}
+
+\FramaC bundles a C standard library in order to help parse and analyze code
+that relies on the functions specified in the ISO C standard.
+Furthermore, In order to simplify parsing of code using common open-source libraries,
+\FramaC's standard library also includes some POSIX and non-POSIX headers which
+are not part of ISO C.
+Such libraries are provided on a best-effort basis, and they are part of the
+{\em trusted computing base}: to ensure its correctness, the specifications
+must be ultimately proofread by the user.
+
+This library, while incomplete, is constantly being improved and extended.
+It is installed in the sub-directory \texttt{libc} of the directory printed by
+\texttt{frama-c -print-share-path}. It contains standard \C headers,
+some \acsl specifications, and definitions for a few library functions.
+
+By default, \FramaC's preprocessing will include the headers of its own standard
+library, instead of those installed in the user's machine. This avoids issues
+with non-portable, compiler-specific features.
+Option \optiondef{-}{frama-c-stdlib} (set by default)
+adds \texttt{-I\$FRAMAC\_SHARE/libc} to the preprocessor command, as well as
+GCC-specific option \texttt{-nostdinc}. If the latter is not recognized by
+your preprocessor,
+\optionuse{-}{no-cpp-frama-c-compliant} can be given to \FramaC
+(see section~\ref{sec:preprocessing}).
+
+The use of \FramaC's standard library contains a few caveats:
+\begin{itemize}
+\item definitions which are not present in \FramaC's standard library may cause
+  parsing errors, e.g. missing type definitions, or missing fields in structs;
+\item if a header is included which is not available in \FramaC's library,
+  preprocessing will fail by default (due to the \texttt{-nostdinc} option);
+  if the user manually includes the system's library, e.g. by adding
+  \texttt{-cpp-extra-args='-I/usr/include'}, the preprocessor will end up
+  mixing headers from \FramaC's library with those from the system, often
+  leading to incompatible definitions and unexpected parsing errors.
+  In this case, the best approach is usually to include {\em only} the missing
+  definitions, for instance by copying them to a separate header file, included
+  manually or via the GCC-compatible option \texttt{-include <header.h>}
+  (see {\em GCC's Preprocessor Options} for more details). Alternatively,
+  consider filing an issue (see Chapter~\ref{user-errors}) to ask for the
+  inclusion of such headers and/or definitions in \FramaC's standard library.
+\end{itemize}
+
+Note that, while \FramaC's library intends to offer maximum portability, some
+definitions such as numeric constants require actual values to be defined.
+For pragmatic reasons, such definitions are most often based on the values
+defined in GNU/Linux's libc, and may differ from those in your system.
+As stated before, if you want to ensure the code analyzed by \FramaC is
+strictly equivalent to the one from the target system, you must either
+proofread the definitions, or provide your own library files.
+
 \section{Warnings during normalization}\label{sec:warnings-normalize}
 
 \emph{Note: the options below are deprecated, replaced by the more general and

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,64 @@ 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}},
 }
+
+@phdthesis{secureflow1,
+  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},
+}
+
+@inproceedings{secureflow2,
+  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,
+}
+
+@inproceedings{ltest,
+  author    = {Micha{\"{e}}l Marcozzi and
+               S{\'{e}}bastien Bardin and
+               Micka{\"{e}}l Delahaye and
+               Nikolai Kosmatov and
+               Virgile Prevosto},
+  title     = {Taming Coverage Criteria Heterogeneity with LTest},
+  booktitle = {2017 {IEEE} International Conference on Software Testing, Verification
+               and Validation, {ICST} 2017, Tokyo, Japan, March 13-17, 2017},
+  pages     = {500--507},
+  year      = {2017},
+}
+
+@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},
+}

doc/value/biblio.bib

@@ -133,4 +133,14 @@
  acmid = {1275501},
  publisher = {ACM},
  address = {New York, NY, USA},
-} 
+}
\ No newline at end of file
+
+@manual{acsl,
+  author = {Baudin, Patrick and Cuoq, Pascal and Filli\^{a}tre, Jean-Christophe and
+            March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
+            Prevosto, Virgile},
+  month = jun,
+  note = {Available at \url{https://frama-c.com/download/acsl.pdf}}},
+  title = {{ACSL: ANSI/ISO C Specification Language. Version 1.17}},
+  year = {2021}
+}

opam/opam

 opam-version: "2.0"
 name: "frama-c"
 synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "24.0~beta"
+version: "24.0"
 description:"""
 Frama-C gathers several analysis techniques in a single collaborative
 framework, based on analyzers (called "plug-ins") that can build upon the
@@ -87,7 +87,7 @@ tags: [
 ]
 
 build: [
-  ["autoconf"] {pinned}
+  ["autoconf"] {dev}
   ["./configure" "--prefix" prefix
                  "--mandir=%{man}%"
   ]

src/plugins/e-acsl/doc/Changelog

@@ -41,6 +41,8 @@ Plugin E-ACSL <next-release>
 Plugin E-ACSL 24.0 (Chromium)
 #############################
 
+-* E-ACSL       [2021-11-24] Fix code generation of properties proven invalid
+                with a previous analysis (frama-c/e-acsl#166).
 -  E-ACSL       [2021-10-20] Add option -e-acsl-assert-print-data
                 (--assert-print-data in e-acsl-gcc.sh) to print data
                 contributing to a failed assertion along with the error message.

src/plugins/e-acsl/src/project_initializer/prepare_ast.ml

@@ -203,7 +203,34 @@ let dup_global loc spec sound_verdict_vi kf vi new_vi =
       let e = Emitter.Usable_emitter.get ep.emitter in
       if ep.logical_consequence
       then logical_consequence e new_ip ep.properties
-      else emit e new_ip ~hyps:ep.properties status
+      else
+        let status, hyps =
+          match status, ep.properties with
+          | True, _ | Dont_know, _
+          | False_and_reachable, [] | False_if_reachable, [] ->
+            (* Valid emission: either [true] status with arbitrary hypotheses or
+               [false] status with empty hypotheses. *)
+            status, ep.properties
+          | False_and_reachable, [ IPReachable _ ]
+          | False_if_reachable, [ IPReachable _ ] ->
+            (* [False] status with a reachability hypothesis: remove the
+               hypothesis and set the status to [False_if_reachable]. *)
+            False_if_reachable, []
+          | False_and_reachable, hyps | False_if_reachable, hyps ->
+            (* Invalid emission: [false] status with arbitrary hypotheses. *)
+            Options.fatal
+              "Property with status '%s' and non-empty hypotheses:\n\
+               * Property: %a\n\
+               * Hypotheses:\n- %a"
+              (match status with
+               | True -> "True"
+               | Dont_know -> "Dont_know"
+               | False_if_reachable -> "False_if_reachable"
+               | False_and_reachable -> "False_and_reachable")
+              Property.short_pretty new_ip
+              (Pretty_utils.pp_list ~sep:"\n- " Property.short_pretty) hyps
+        in
+        emit e new_ip ~hyps status
     in
     match get old_ip with
     | Never_tried ->
@@ -212,9 +239,9 @@ let dup_global loc spec sound_verdict_vi kf vi new_vi =
       List.iter (cp s) epl
     | Inconsistent icst ->
       List.iter (cp True) icst.valid;
-      (* either the program is reachable and [False_and_reachable] is
-         fine, or the program point is not reachable and it does not
-         matter for E-ACSL that checks it at runtime. *)
+      (* Copy invalid properties with [False_and_reachable], if a reachability
+         hypothesis is present then the [cp] function will convert it to
+         [False_if_reachable]. *)
       List.iter (cp False_and_reachable) icst.invalid
   in
   let ips kf s = Property.ip_of_spec kf Kglobal ~active:[] s in

src/plugins/e-acsl/tests/bts/issue-eacsl-166.i

+/* run.config
+   COMMENT: Change order of options to run Eva before E-ACSL so that the ensures
+   COMMENT: clause is proven invalid before running E-ACSL. Eva will prove the
+   COMMENT: ensures invalid under hypotheses of reachability, this test shows
+   COMMENT: that when we duplicate the invalid property statuses, we remove the
+   COMMENT: hypotheses to satisfy kernel invariants.
+   OPT: @GLOBAL@ @EVA@ -then @EACSL@ -then-last @EVENTUALLY@
+*/
+/* run.config_dev
+   COMMENT: No need to compile and execute the test since we know the property
+   COMMENT: will be invalid.
+   DONTRUN:
+*/
+
+/*@ ensures \result == 1; */
+int f() {
+  return 0;
+}
+
+int main() {
+  f();
+  return 0;
+}

src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle

+[eva:alarm] tests/bts/issue-eacsl-166.i:15: Warning: 
+  function f: postcondition got status invalid.
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-166.i:15: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status invalid.