From 15c890d868fdfc8bf1ae09d736ab03a760d10fb1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 20 Jun 2019 15:40:14 +0200
Subject: [PATCH] [Eva] User manual: splits can only be performed on integer
expressions.
---
doc/value/main.tex | 16 +++++++++-------
1 file changed, 9 insertions(+), 7 deletions(-)
diff --git a/doc/value/main.tex b/doc/value/main.tex
index efa337f973f..018e077c1f4 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3800,21 +3800,23 @@ reason by case during the whole analysis. The command line parameter
\lstinline|-eva-partition-value <V>| forces the analyzer to reason at all times
on single values of the global variable \lstinline|<V>|.
-There are three limitations to partitioning on values:
+There are four limitations to the value partitioning:
\begin{enumerate}
-\item While the number of simultaneous splits (whether local with annotations
- or global through command line) is not bounded, there can be only one split
- per expression. If two \lstinline|split| annotations use the same expression,
- only the latest one encountered on the path will be kept. Although it is a
- limitation, it can be used to define strategies where a case-based reasoning
- is controlled accross the whole program.
+\item Splits can only be performed on integer expressions. Pointers and
+ floating-point values are not supported yet.
\item The expression on which the split is done must evaluate to a small set of
integer values, in order to limit the cost of the partitioning and ensure the
termination of the analysis. If the number of possible values infered for the
expression exceeds a defined limit, \Eva{} cancels the split and emits a
warning. The limit is 100 by default and can be changed with option
\lstinline|-eva-split-limit <n>|.
+\item While the number of simultaneous splits (whether local with annotations
+ or global through command line) is not bounded, there can be only one split
+ per expression. If two \lstinline|split| annotations use the same expression,
+ only the latest one encountered on the path will be kept. Although it is a
+ limitation, it can be used to define strategies where a case-based reasoning
+ is controlled accross the whole program.
\item When the expression is complex, the ability of \Eva{} to reason
precisely by cases depends on the enabled abstract domains (see section
\ref{sec:eva}) and their capability to learn from the value of the expression.
--
GitLab