From 4790a86cb85a99621ac3f02eaaebe86c307c8897 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 7 Oct 2022 12:02:02 +0200
Subject: [PATCH] [Eva] User manual: fixes description of a message in the ACSL
FAQ.
---
doc/eva/main.tex | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 070536757ad..735243bcd4c 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -6653,15 +6653,14 @@ value is saved in \texttt{old}'') and has been called with a null pointer.
In this case, the message can be safely ignored.
\paragraph{Cannot evaluate ACSL term, unsupported ACSL construct: [...]}
-This message can be emitted as a warning, or as a simple feedback message.
-In the latter case, this is just a notification concerning the fact that
-an analyzed specification is ``too complex'' for \Eva{} to currently interpret
-it, but unnecessary for the soundness of the analysis (otherwise it would have
-been emitted as a warning).
+This message indicates that a specification is ``too complex'' for \Eva{} to
+currently interpret it, and is ignored by the analysis:
+\Eva{} cannot prove the specification, nor use it to improve its analysis.
+However, this has no impact on the soundness of the analysis.
This often arrives when using Frama-C's libc specifications for functions in
\texttt{string.h}, because these functions include a logical axiomatization
-that is useful for the \textsf{WP} plug-in. In this context, and without
-the warning, they can be safely ignored.
+that is useful for the \textsf{WP} plug-in.
+In this context, they can be safely ignored.
\end{document}
--
GitLab