From 5873b2a30484e0281dc40c30daea132724cf5e61 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 13 Jun 2019 10:22:59 +0200
Subject: [PATCH] [Eva] User manual: a few more details about the summary.
---
doc/value/main.tex | 20 +++++++++++++++-----
1 file changed, 15 insertions(+), 5 deletions(-)
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 16388f474bb..a541d32a9a7 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -1913,7 +1913,7 @@ which causes them to be emitted.
\subsection{Analysis summary}
-By default, at the end of the analysis \Eva{} produces a summary such as the
+At the end of the analysis, \Eva{} produces a summary such as the
following:
\begin{logs}
@@ -1939,15 +1939,25 @@ following:
It contains:
\begin{itemize}
-\item semantic coverage metrics;
-\item total number of errors and warnings;
-\item total number of alarms, grouped by kind;
-\item total number of property statuses evaluated by \Eva{}.
+\item semantic coverage metrics, with the number of functions and
+ statements analyzed;
+\item total number of errors and warnings, pointing out potential issues that
+ could jeopardize the correction of the analysis;
+\item total number of alarms emitted by the analysis, grouped by kind;
+\item total number of logical properties (assertions and preconditions at each call-site)
+ proven by the analysis.
+ Note that this only indicates the logical statuses evaluated by \Eva{};
+ some logical properties may have been proven by other plugins.
\end{itemize}
The summary provides a quick glance at the analysis, being especially useful
for side-by-side comparisons of different parametrizations. It also allows
one to quickly determine whether there remain issues to be resolved.
+More detailed information is provided through the graphical interface and
+by the Report plugin.
+
+The summary display can be disabled by using option
+\lstinline|-eva-msg-key=-summary|.
\section{About these alarms the user is supposed to check\ldots}
--
GitLab