diff --git a/doc/eva/examples/parametrizing/split-array.log b/doc/eva/examples/parametrizing/split-array.log
index 53a9ddd932748d851458163c1c4c9e1f4d461370..5adefbaf6d4c26f05da62738388ced7a7cab5977 100644
--- a/doc/eva/examples/parametrizing/split-array.log
+++ b/doc/eva/examples/parametrizing/split-array.log
@@ -27,7 +27,7 @@
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
   1 function analyzed (out of 1): 100% coverage.
-  In this function, 9 statements reached (out of 9): 100% coverage.
+  In this function, 10 statements reached (out of 10): 100% coverage.
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 9e3f8359025a9433a42d8dbb58b7c74aefb70b7b..fc9d9c1af019942617ce5a4bc107308f39f54d86 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -4203,13 +4203,13 @@ Most domains are also presented in more details in the following subsections.
     \tabularnewline
     \midrule
     octagon & d-octagon & \ref{sec:octagons} &
-    Infers relations between scalar variables. \\
-    Efficient but limited.
+    Infers relations of the form $l \leq \pm X \pm Y \leq u$ between integer or
+    pointer lvalues. Efficient.
     \tabularnewline
     \midrule
     multidim & d-multidim & \ref{sec:multidim} &
     More precise representation of arrays of structures,
-    multidimensional arrays and arrays invariants. \\
+    multidimensional arrays and arrays invariants.
     Experimental.
     \tabularnewline
     \midrule
@@ -4435,7 +4435,8 @@ and \texttt{y} is not affine.
 
 Activating option \texttt{-eva-domains octagon} instructs Eva to infer relations
 between variables as numerical constraints of the form $l \leq \pm X \pm Y \leq
-u$, where $X$ and $Y$ are program variables, and $l$ and $u$ are constants.
+u$, where $X$ and $Y$ are program variables or lvalues,
+and $l$ and $u$ are constants.
 
 These relations are then used to evaluate more precisely the possible values
 of an expression involving $X$ and $Y$, or to deduce a reduction of
@@ -4455,16 +4456,23 @@ void main (int y) {
 \end{listing-nonumber}
 
 
-Currently, the octagon domain is fast but has two strong limitations:
+Currently, the octagon domain is fast but has some limitations:
 \begin{itemize}
 \item
-  The domain only infers relations between scalar variables of integer types.
-  It ignores pointers, arrays and structure fields.
+  The domain only infers relations between lvalues of integer or
+  pointer types.
+  It does not support relations between floating-point values.
 \item
   The domain only infers relations between pairs of variables occurring in the
   same instruction, as \lstinline|x = y + k;| or \lstinline|if (x < y + k)|.
   If an instruction involves 3 variables or more, relations are inferred for
   each pair of variables.
+\item
+  The domain has no involved memory model and can only infer and use relations
+  about the syntactic lvalues as they appear in the program.
+  For instance, if two pointers \lstinline|p| and \lstinline|q| point to the
+  same location, and a relation is inferred on \lstinline|*p|, the domain cannot
+  use it to improve the value of \lstinline|*q|.
 \end{itemize}
 
 The domain is intraprocedural by default: the inferred relations are local to
@@ -4474,8 +4482,9 @@ to its caller.
 The option \verb+-eva-octagon-through-calls+ makes the octagon domain
 interprocedural, which is a more precise but slower mode where
 the inferred relations are propagated through function calls.
-The analysis of a function can then use the relations inferred in the callers,
-and at the end, the inferred relations are propagated back to the caller.
+The analysis of a function can then use the relations previously inferred in the
+callers, and at the end, the inferred relations are propagated back to the
+caller.
 
 
 \subsection{Multidim}