[Eva] User manual: adds subsection about -eva-subdivide-non-linear.

doc/eva/main.tex

@@ -4167,6 +4167,43 @@ analysis, both in terms of precision and performance. However, when dealing
 with large arrays and matrices, it is worth considering its usage.
 
 
+\subsection{Subdividing the evaluation of non-linear expressions}
+
+Option \verb|-eva-subdivide-non-linear| improves the analysis precision on
+non-linear expressions, such as \lstinline|x * x|,
+or on any expression with multiple occurrences of the same lvalue.
+
+The interval semantics is inherently imprecise on non-linear expressions.
+When $x \in [-10..10]$, the interval semantics computes $x*x \in [-100..100]$.
+Subdivisions can mitigate this imprecision by splitting the evaluation of
+\lstinline|x*x| according to the possible values of \lstinline|x|,
+and then joining the results.
+When \verb|-eva-subdivide-non-linear| is enabled, \Eva{} evaluates the
+expression \lstinline|x*x| separately for $x \in [-10..0]$ and $x \in [0..10]$,
+and computes the precise interval $x*x \in [0..100]$ for both cases.
+On this example, splitting the values of x further would not improve the result.
+
+The argument of \verb|-eva-subdivide-non-linear| is the maximal number of
+subdivisions that can be performed for each non-linear expression.
+This limit is not always reached, as heuristics may detect when more
+subdivisions cannot lead to a better result.
+This option slightly slows down the analysis, as more computations are performed;
+in practice, the limit can usually be set up to several hundreds even on
+large programs.
+
+The option is global, and subdivisions are applied to any non-linear expression
+of integer or floating-point type.
+Subdivisions can also be controlled locally by writing annotations
+in the analyzed code:
+a \lstinline|//@  subdivide N;| annotation instructs \Eva{}
+to apply up to $N$ subdivisions when evaluating the following statement,
+regardless of option \verb|-eva-subdivide-non-linear|.
+
+Finally, \Eva is also able to subdivide the evaluation of an expression
+according to the values off an arbitrary number of lvalues;
+thus, this subdivision mechanism can also improve the precision on expressions
+non-linear on several lvalues, such as \lstinline|x*x - 2*x*y + y*y|.
+
 \section{Analysis domains}
 \label{sec:eva}