From 9752800f759746738204b2ddddcb81bea2540c86 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 18 Mar 2020 17:44:56 +0100
Subject: [PATCH] [Eva] User manual: documents the -eva-domains-function
option.
---
doc/value/main.tex | 18 ++++++++++++++++--
1 file changed, 16 insertions(+), 2 deletions(-)
diff --git a/doc/value/main.tex b/doc/value/main.tex
index dd2d364f61e..96d66840582 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3904,7 +3904,7 @@ with large arrays and matrices, it is worth considering its usage.
\label{sec:eva}
-Starting from \FramaC Silicon, new analysis \emph{domains} are
+This section presents the analysis \emph{domains}
available to improve the precision on specific code constructs.
They can (and probably should) be enabled at the beginning of the analysis.
Their only downside is that they increase the analysis time.
@@ -3913,7 +3913,21 @@ These analysis domains are enabled by the option \texttt{-eva-domains}, followed
by a list of domain names. A list of the available domains, and a short
description of each one, can be displayed with \texttt{-eva-domains help}.
-\emph{Restrictions:}
+Domains can also be enabled for specific functions through option
+\texttt{-eva-domains-function}:
+\begin{itemize}
+\item \texttt{-eva-domains-function d1:f,d1:g,d2:h} enables the domain
+ \texttt{d1} on functions \lstinline+f+ and \lstinline+g+, and the domain
+ \texttt{d2} on function \lstinline+h+.
+\item \texttt{-eva-domains-function d:f+} enables the domain
+ \texttt{d} on function \lstinline+f+ and on any function called
+ from \lstinline+f+.
+\item \texttt{-eva-domains-function d:f-} disables the domain
+ \texttt{d} on function \lstinline+f+ and on any function called
+ from \lstinline+f+.
+\end{itemize}
+
+These analysis domains currently have some restrictions:
\begin{itemize}
\item adding a new domain may interact with the \lstinline+slevel+ partitioning
in unpredictable ways, and new alarms may sometimes appear;
--
GitLab