From 9f7e9ec7a88b3e4cb650f7d8ab9c2c466b563bd3 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 29 Nov 2021 15:22:48 +0100
Subject: [PATCH] [userman] proof read overview update
---
doc/userman/user-overview.tex | 10 +++++-----
doc/userman/userman.bib | 23 +++++++++++------------
2 files changed, 16 insertions(+), 17 deletions(-)
diff --git a/doc/userman/user-overview.tex b/doc/userman/user-overview.tex
index 69988fc01fc..7f79dbaae40 100644
--- a/doc/userman/user-overview.tex
+++ b/doc/userman/user-overview.tex
@@ -11,7 +11,7 @@ other analyzers in the framework. Thanks to this approach, \FramaC can provide
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.
+or a set of tools for various test coverage criteria (LTest~\cite{ltest}), among many others.
\section{\FramaC as a Code Analysis Tool}
@@ -110,9 +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}\footnote{Some common
-GCC extensions, as well as some parts of the \tool{C11} standard, are
-also supported.}. \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}.
@@ -141,7 +141,7 @@ 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{Frama-Clang}
-plug-in~\cite{framaclang}, which provides a front-end for C++ code;
+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.
diff --git a/doc/userman/userman.bib b/doc/userman/userman.bib
index 6f28c0523a6..d4e9482f6dd 100644
--- a/doc/userman/userman.bib
+++ b/doc/userman/userman.bib
@@ -127,18 +127,17 @@ note={Extended version of \cite{sefm12}},
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},
+@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,
--
GitLab