[Eva] User manual: minor changes in the loop unrolling section.

doc/value/main.tex

@@ -3319,24 +3319,24 @@ The annotations above will ensure
 that \Eva{} will unroll the loops and keep the analysis precise; otherwise,
 the array access \lstinline|a[i][j]| might generate alarms due to imprecisions.
 
-The \lstinline|loop unroll| parameter can be any C expression such that there
-is only one possible integer value found by \Eva{} for this expression.
+The \lstinline|loop unroll| parameter can be any C expression evaluated to a
+single integer value by \Eva{} each time the analysis reaches the loop.
+Otherwise, the annotation is ignored and a warning is issued.
 Constants obtained via \lstinline|#define| macros, variables which always have
-a unique value or a combination of these with arithmetic operator are
-suitable. For expressions which do not obviously represent only one integer,
+a unique value and arithmetic operators are suitable.
+For expressions that have several possible values,
 the acceptability of the annotation depends on the precision of the analyzer.
-Note that there are interesting cases of non-constant expression for
+Note that there are interesting cases of non-constant expressions for
 unrolling annotations. The example below shows a function with two nested loops.
 
 \lstinputlisting{examples/parametrizing/loop-unroll-nested.c}
 
-The number of iterations of the outer one is constant while the number of
-iterations of the inner one is variable but depends on the current iteration of
-the outer loop. However, if we instructs \Eva{} to unroll the outer loop then
-the parameter \lstinline|sizes[i]| of the \lstinline|loop unroll| annotation
-always evaluate to a single possible integer and thus the inner loop annotation
-is accepted. Note that, in this example, it is also possible to use an upper
-bound like $4$.
+The number of iterations of the outer loop is constant while the number of
+iterations of the inner loop depends on the current iteration of the outer
+one. As we have instructed \Eva{} to unroll the outer loop, it evaluates the
+parameter \lstinline|sizes[i]| to a single possible integer for each iteration
+of the outer loop, and thus the inner loop annotation is accepted. In this
+example, it is also possible to use an upper bound like $4$.
 
 The unrolling mechanism is independent of \lstinline|-eva-slevel|
 (see next subsection): annotated loops are always unrolled at least the specified