Addresses Julien's review on the doc:

- BTS #!1354 is actually not yet fixed
- Logic functions and logic global variables are not yet supported
- Better description of features that are not yet implemented
- Add missing \cinput files

src/plugins/e-acsl/doc/Changelog

@@ -20,7 +20,6 @@
 ###############################################################################
 
 -* E-ACSL       [2018/10/04] Support for \at on purely logic variables.
-                Fix bug #2354 about undeclared variables when using \at.
                 Fix bug #1762 about out-of-scope variables when using \old.
 *  E-ACSL       [2018/10/02] Fix bug #2305 about taking the address of a
                 bitfield.

src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c

+main(void) {
+  int m = 2;
+  int n = 7;;
+  K: ;
+  n = 875;
+  /*@ assert
+      \let k = 3;
+      \exists integer u; 9 <= u < 21 &&
+      \forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
+        \at(n + u + v > 0, K); */ ;
+  return 0;
+}

src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c

+/*@ ensures \forall int i; 0 <= i < n-1 ==> \old(t[i]) == t[i+1]; */
+void reverse(int *t, int n) { }

src/plugins/e-acsl/doc/refman/speclang_modern.tex

@@ -523,14 +523,14 @@ The \verb|\at| construct of the following example is supported.
 
 
 \begin{notimplementedenv}
-However, quantified variables and let-binded variables that use C variables in
-their definition are not yet supported. Also, uses of formal variables of
-logic functions and global logic variables are not yet supported.
+However, quantified variables that use C variables in their bounds and
+let-binded variables that use C variables in their definition
+are not yet supported.
 
 \begin{example}
 The \verb|\at| construct of the following example is \emph{not yet} supported
-since the let-binded variable \verb|w| uses C variables, namely \verb|m| and
-\verb|n|, in its definition.
+since the quantified variable \verb|i| uses the C variable \verb|n| in the
+definition of its upper bound.
 \cinput{at_on-purely-logic-variables_not-yet.c}
 
 \end{example}