[Doc] Eva manual: add reference to quick guide annex, and to ACSL reference

doc/value/biblio.bib

@@ -133,4 +133,14 @@
  acmid = {1275501},
  publisher = {ACM},
  address = {New York, NY, USA},
-} 
\ No newline at end of file
+}
+
+@manual{acsl,
+  author = {Baudin, Patrick and Cuoq, Pascal and Filli\^{a}tre, Jean-Christophe and
+            March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
+            Prevosto, Virgile},
+  month = jun,
+  note = {Available at \url{https://frama-c.com/download/acsl.pdf}}},
+  title = {{ACSL: ANSI/ISO C Specification Language. Version 1.17}},
+  year = {2021}
+}

doc/value/main.tex

@@ -4795,6 +4795,12 @@ be of service to or be checked by the \Eva{} plug-in.}
 
 \vspace{2cm}
 
+If you are not familiar with ACSL, consider reading the
+{\em ACSL Quick Guide for Eva}, in Appendix~\ref{sec:acsl-quick-guide}.
+It contains a brief introduction to ACSL, targeted towards Eva users.
+Even if you already know some ACSL, it contains a few Eva-related remarks
+and tips related to specific warnings, which might be useful.
+
 \section{Preconditions, postconditions and assertions}
 \label{prepostasserts}
 
@@ -5992,6 +5998,7 @@ getting the text to where it is today.
 
 \appendix
 \chapter{ACSL Quick Guide for Eva}
+\label{sec:acsl-quick-guide}
 
 \Eva{} users are often required to read and write some amount of ACSL
 annotations: alarms generated by \Eva{}, library function specifications,
@@ -6002,6 +6009,9 @@ for \Eva{} analyses, intended for complete ACSL beginners.
 It focuses on the specific subset of ACSL that is mostly useful for \Eva{}, with
 some examples based on ACSL specifications from the \FramaC standard library.
 
+For more details about the terms described here, and for the full
+ACSL reference documentation, consult~\cite{acsl}.
+
 \section{Basic Syntax}
 
 ACSL annotations are C comments; they are ignored by most tools, but parsed