From 52bc0082e9fd4edb1459d0eb6ad6431537475fda Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 12 Jun 2019 18:38:01 +0200
Subject: [PATCH] [Doc/Eva] user manual: fix some typos, add section about
summary
---
doc/value/main.tex | 53 ++++++++++++++++++++++++++++++++++++++++------
1 file changed, 47 insertions(+), 6 deletions(-)
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 772bffef6b8..1b0c79cddf0 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -1748,8 +1748,10 @@ For instance, the first of these warnings is:
Then \Eva{} is run on the program.
In the example at hand, the analysis finds problems at lines 5 and 7.
\begin{logs}
-[eva:alarm] se.c:5: Warning: undefined multiple accesses in expression. assert \separated(&x, &x);
-[eva:alarm] se.c:7: Warning: undefined multiple accesses in expression. assert \separated(&x, p);
+[eva:alarm] se.c:5: Warning: undefined multiple accesses in expression.
+ assert \separated(&x, &x);
+[eva:alarm] se.c:7: Warning: undefined multiple accesses in expression.
+ assert \separated(&x, p);
\end{logs}
At line 5, it can guarantee that an undefined behavior exists, and the analysis
is halted.
@@ -1879,7 +1881,7 @@ they do {\bf not} use the word ``assert''.
These messages
are intended to help the user trace the results of the analysis, and
give as much information as possible in order to help
-em find when and why the analysis becomes imprecise.
+them find when and why the analysis becomes imprecise.
These messages are only useful when it is important to analyze the application
with precision. \Eva{} remains correct even when it
is imprecise.
@@ -1909,6 +1911,45 @@ Note that a few messages are prefixed with \verb|[kernel]| instead of
\verb|[eva]|, for technical reasons, but it is the analysis by \Eva{}
which causes them to be emitted.
+\subsection{Analysis summary}
+
+By default, at the end of the analysis \Eva{} produces a summary such as the
+following:
+
+\begin{logs}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 6 functions analyzed (out of 44): 13% coverage.
+ In these functions, 588 statements reached (out of 626): 93% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 143 alarms generated by the analysis:
+ 71 integer overflows
+ 64 accesses to uninitialized left-values
+ 8 illegal conversions from floating-point to integer
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 11 valid 0 unknown 0 invalid 11 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
+\end{logs}
+
+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{}.
+\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.
+
+
\section{About these alarms the user is supposed to check\ldots}
When writing a Frama-C plug-in to assist in
@@ -5260,7 +5301,7 @@ evaluating \lstinline|if| or \lstinline|switch| conditionals (but it is consumed
by them, which can be confusing for the user).
Both approaches do have a minor drawback, in that they do not allow to observe
-a specific iteration step of the loop. The main advantage of these options are
+a specific iteration step of the loop. The main advantage of these options is
that they leave the source code unchanged.
The Frama-C kernel has an option \lstinline|-ulevel|, which performs a
@@ -5293,7 +5334,7 @@ perform a choice over what may happen after dereferencing
\lstinline|NULL|. It is possible to give some new information to the tool
so that analysis can continue after a true alarm. This technique is called
debugging. Once the issue has been corrected in the source code under
-analysis ---~more precisely, once the user has convinced emself
+analysis ---~more precisely, once the user has convinced themselves
that there is no problem at this point in the source code~--- it
becomes possible to trust the alarms that occur after the given point,
or the absence thereof (see next question).
@@ -5329,7 +5370,7 @@ proceeds with the analysis, the plug-in detects that line 8 is safe, and
that there is an alarm on line 9. These results must be interpreted
thus: assuming that the array access on line 7 was legitimate, then
line 8 is safe, and there is a threat on line 9. As a consequence, if
-the user can convince emself that the threat on line 7 is false,
+the user can convince themselves that the threat on line 7 is false,
they can trust these results ({\it i.e.} there is nothing to worry
about on line 8, but line 9 needs further investigation).
%\bigskip
--
GitLab