diff --git a/doc/eva/examples/nondet.c b/doc/eva/examples/nondet.c
index 808ba9c653ee9a33e59b006d03dac4c9224c1a6d..b73510ecab61fbce6e8034709be01b4a68484b06 100644
--- a/doc/eva/examples/nondet.c
+++ b/doc/eva/examples/nondet.c
@@ -1,9 +1,11 @@
 #include "__fc_builtin.h"
 
 int A,B,X;
+int arr[20];
 void main(void)
 {
   A = Frama_C_nondet(6, 15);
   B = Frama_C_interval(-3, 10);
   X = A * B;
+  Frama_C_make_unknown(arr, sizeof(arr));
 }
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index b3c5be5239cf7e0bf761765a6392fc75349eacc3..0eca8aeee872080e5c835ee0fc3c2a208ec94db8 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -5574,7 +5574,9 @@ allocation fails.
 \label{nondeterminism}
 
 The following functions, declared in \lstinline|share/libc/__fc_builtin.h|, allow to
-introduce some non-determinism in the analysis. The results given by
+introduce some non-determinism in the analysis.
+
+The results given by
 \Eva{} are
 valid \textbf{for all values proposed by the user}, as opposed
 to what a test-generation tool would typically do. A tool based
@@ -5583,6 +5585,10 @@ would indeed necessarily pick only a subset of the billions
  of possible entries
 to execute the application.
 
+Note that these functions are not specific to \Eva{}; their ACSL specifications
+(omitted here for brevity) allow them to be understood by any plug-in capable of
+interpreting them.
+
 \begin{listing-nonumber}
 int Frama_C_nondet(int a, int b);
     /* returns either a or b */
@@ -5593,28 +5599,23 @@ void *Frama_C_nondet_ptr(void *a, void *b);
 int Frama_C_interval(int min, int max);
     /* returns any value in the interval from min to max inclusive */
 
-float Frama_C_float_interval(float min, float max);
-    /* returns any value in the interval from min to max inclusive */
+<type> Frama_C_<type>_interval(<type> min, <type> max);
+    /* a series of functions equivalent to Frama_C_interval, but defined
+       for other integer and floating-point types */
 
-double Frama_C_double_interval(double min, double max);
-    /* returns any value in the interval from min to max inclusive */
+double Frama_C_make_unknown(char *p, size_t l);
+    /* assigns an arbitrary value to each byte between *p and *(p+l-1) */
 \end{listing-nonumber}
 
-The implementation of these functions might change in future versions
-of Frama-C, but their types and their behavior will stay the same.
-
 Example of use of the functions introducing non-determinism:
 \csource{examples/nondet.c}
 
 With the command below, the obtained result for
-variable \lstinline|X| is \lstinline|[-45..150],0%3|.
+variable \lstinline|X| is \lstinline|[-45..150],0%3|, and for the
+array \lstinline|arr|, \lstinline|[0..19] ∈ [--..--]|.
 \begin{frama-c-commands}
-frama-c -eva ex_nondet.c .../share/libc/__fc_builtin.c
+frama-c -eva ex_nondet.c
 \end{frama-c-commands}
-The inclusion of \lstinline|.../share/libc/__fc_builtin.c| is only required
-when using the functions \lstinline|Frama_C_float_interval| and
-\lstinline|Frama_C_double_interval|. Otherwise, including the file
-\lstinline|__fc_builtin.h| is sufficient.
 
 Note that reads of volatile variables also return a non-deterministic
 value.