From c9e4643df203d6f5b46fcc310d11b58a0ed9f804 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 12 Jun 2019 17:33:06 +0200
Subject: [PATCH] [Eva] User manual: slightly rewrites FAQ about loop
 unrolling.

---
 doc/value/main.tex | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

diff --git a/doc/value/main.tex b/doc/value/main.tex
index 0542c171d2c..772bffef6b8 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -5249,23 +5249,19 @@ return \lstinline|6| and \lstinline|36| respectively.
 \question{Which option should I use to improve the handling of loops
   in my program?}
 
-The recommended way is to use \lstinline|loop unroll| annotations, which are
-the most precise and stable mechanism currently in \Eva{}.
+The recommended way is to use \lstinline|loop unroll| annotations on a case by
+case basis, which is the most precise and stable mechanism currently in \Eva{}.
 Alternatively, using \lstinline|-eva-slevel| is the next best approach.
+This option is more costly, often hard to predict, and can only be specified
+globally or at the function level (via \lstinline|-eva-slevel-function|).
+However, it works for loops that are built using \lstinline|goto|s instead of
+\lstinline|for| or \lstinline|while|, and it also improves precision when
+evaluating \lstinline|if| or \lstinline|switch| conditionals (but it is consumed
+by them, which can be confusing for the user).
 
 Both approaches do have a minor drawback, in that they do not allow to observe
-a specific iteration step of the loop.
-In fact, they may even be a little
-confusing for the user when the program contains loops for which the
-analysis cannot decide easily the truth value of the condition,
-nested loops, or if-then-else
-statements\footnote{if-then-else statements are ``unrolled''
-  in a manner similar to loops}. The main advantage of these options are
-that they leave the source code unchanged. Also, \lstinline|-eva-slevel| works
-with loops that are built using \lstinline|goto|s instead of \lstinline|for|
-or \lstinline|while|.
-\lstinline|-eva-slevel| also improves precision when evaluating \lstinline|if|
-or \lstinline|switch| conditionals (but it is consumed by them).
+a specific iteration step of the loop. The main advantage of these options are
+that they leave the source code unchanged.
 
 The Frama-C kernel has an option \lstinline|-ulevel|, which performs a
 syntactic modification of the analyzed source code. Its advantage is that,
-- 
GitLab