Merge branch 'feature/andre/eva-manual-acsl-quick-guide' into 'stable/chromium'

[Doc] add a quick guide for ACSL for Eva

See merge request frama-c/frama-c!3359

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}
 
@@ -5990,6 +5996,609 @@ getting the text to where it is today.
 \bibliographystyle{alpha}
 \bibliography{biblio.bib}
 
+\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,
+user assertions; all of these require some basic ACSL knowledge.
+
+This quick guide should serve as a suitable introduction to ACSL specifications
+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
+by the \FramaC kernel.
+
+ACSL annotations begin with \texttt{//@} or \texttt{/*@}. No spaces are allowed
+before the '@'. Each single-line annotation (\texttt{//@}) is independent.
+
+ACSL clauses {\em always} terminate with a semicolon (\texttt{;}) character.
+Multiline annotations are then closed with \texttt{*/}.
+
+Function contracts are specified in a {\em single} annotation.
+This is {\em forbidden}:
+
+\begin{lstlisting}
+//@ requires a != 0; // error: this annotation is not attached to the function
+//@ ensures \result > 0;
+int f(int a);
+\end{lstlisting}
+
+Function contracts with several clauses are equivalent to a logical
+\textbf{and} (\&\&) between them.
+E.g., \verb+requires A; requires B;+ is equivalent to \verb+requires A && B;+.
+
+You can use all C operators (bitwise, arithmetic, etc.) in ACSL expressions,
+\textbf{except} those with side-effects (e.g. \texttt{i++}).
+
+Some mathematical Unicode characters are accepted:
+$\forall$, $\mathbb{Z}$, $\geq$, etc. All have equivalent ASCII notations
+(\verb+\forall+, \texttt{integer}, \texttt{>=}, etc).
+
+Numbers are, by default, {\em mathematical integers}, of type \texttt{integer}
+(\texttt{$\mathbb{Z}$}), or {\em real numbers}, of type
+\texttt{real} (\texttt{$\mathbb{R}$}). Casts can be used to convert them to
+C integers (\texttt{int}) or C floats (\texttt{double}).
+
+Predefined ACSL symbols are often prefixed by a backslash to avoid name
+clashing (e.g. the \verb+\valid+ predicate contains a
+backslash to avoid shadowing a possible C identifier \texttt{valid}).
+
+For \Eva{}, the main ACSL operators which are {\em not} present in C are:
+
+\begin{itemize}
+\item {\em range} operator (\texttt{..}): specifies an interval in memory
+  locations, e.g. \texttt{a[0 .. 7]} refers to all elements in \texttt{a}
+  between 0 and 7, {\em included}. This means you should not forget adding a
+  \texttt{-1} to many expressions when converting from C,
+  i.e. \verb+\valid(a[0 .. n-1])+ for an array of \texttt{n} elements.
+\item {\em forall} and {\em implies} operators (\verb+\forall+
+  and \texttt{==>}): used in a few logical formulas; \Eva{} currently only
+  interprets some specific patterns when these operators are used.
+  Also, note that most uses of \verb+\forall+ are subsumed by the {\em range}
+  operator.
+\end{itemize}
+
+Note that the range operator can be used either with parentheses
+(when referring to pointers) or with brackets. Also remember that arithmetic
+operations with ranges follow the same rules of pointer arithmetics:
+the offsets depend on the pointer type. See Section~\ref{sec:acsl-guide-faq}
+for an example syntax when dealing with pointers to type \texttt{void}.
+
+\paragraph{Special symbols}
+
+ACSL annotations are preprocessed by default. This means you can use
+definitions such as \verb+INT_MAX+, \verb+EOF+, etc.
+For null pointers, the ACSL term \verb+\null+ can be used, notably if macro 
+\verb+NULL+ is not available.
+
+\section{Kinds of clauses}
+
+The main kinds of clauses used by \Eva{} are:
+\begin{itemize}
+\item assertions (\texttt{assert}): associated with {\em C statements}
+  (in block scope, that is, non-global), you can think of them as some
+  fancy version of the libc \texttt{assert} macro, defined in
+  \texttt{assert.h}. They state properties which must hold at the program
+  point where they are written.
+\item preconditions (\texttt{requires}): part of function contracts
+  (can only be written before a function declaration), these clauses
+  act as assertions placed before each function call.
+\item postconditions (\texttt{ensures}): also part of function contracts,
+  \Eva{} uses them to {\em reduce} the state after the call, that is, they
+  improve precision of the analysis by discarding irrelevant states.
+  Note that there are two modes: if \Eva{} only has a specification for the
+  function, then \texttt{ensures} are {\em considered valid}; if the function
+  definition is also available, \Eva{} will check the \texttt{ensures}. If it
+  fails to prove them, it will generate alarms before reducing.
+\item assigns ... \textbackslash{}from (\texttt{assigns}): also part of function contracts,
+  they state all locations that are possibly modified by the function. For \Eva{},
+  the \verb+\from+ part of these clauses also tells, in the case of pointers,
+  where do the new values come from. Note that \verb+assigns+ means
+  {\em possibly} modified; you should read them as ``may assign''.
+\end{itemize}
+
+Other clauses which are often used by \Eva{} are function {\em behaviors}, for
+function contracts with multiple states. Inside behaviors, the {\em assumes}
+clause operates similarly to \texttt{requires}: it defines the behavior's
+preconditions.
+
+\paragraph{Examples}
+
+In the following code, we check that \texttt{malloc} did not return a null
+pointer:
+
+\begin{lstlisting}
+  int *p = malloc(4 * sizeof(int));
+  //@ assert p != \null;
+\end{lstlisting}
+
+If \Eva{} was called with option \texttt{-eva-no-alloc-returns-null},
+the assertion will be always true; otherwise, an alarm will be emitted,
+and only the states where \texttt{p} is non-null will continue.
+
+Another example:
+
+\begin{lstlisting}
+unsigned long long r = a << 32;
+//@ assert r >= INT_MAX + 1 && r < LLONG_MAX;
+\end{lstlisting}
+
+Here, we see why ACSL numbers are mathematical integers by default; otherwise,
+the expression \texttt{INT\_MAX + 1} might overflow, so we would need to use
+casts, making the expression harder to read and more error-prone.
+
+Here is an example of a function annotation (some predicates will be detailed
+later):
+
+\begin{lstlisting}
+/*@
+  requires \is_finite(x) && \valid(exp);
+  ensures \is_finite(\result);
+  ensures 0.5 <= \result < 1.0;
+  assigns \result, *exp \from x;
+ */
+double frexp(double x, int *exp);
+\end{lstlisting}
+
+This is a simplified version of the actual contract in \FramaC's standard
+library, in \texttt{math.h}. Function \texttt{frexp} converts a floating-point
+number (\texttt{x}) into a fractional part (the function result, between
+0.5 and 1.0) and an exponent (\texttt{exp}).
+The specification can be read as follows, from top to bottom, and from left
+to right:
+\begin{itemize}
+\item \texttt{x} must be a finite floating-point value, that is, neither
+  \texttt{inf}/\texttt{-inf} nor \texttt{NaN};
+\item \texttt{exp} must point to a valid and writable memory location;
+  in other words, assigning to \texttt{*exp} should be allowed;
+\item when the function returns, its result value will be finite;
+\item not only that, but the return value will be comprised between
+  0.5 (included) and 1.0 (excluded);
+\item the function may change the contents of the memory locations representing
+  its result value (this is always the case for non-void functions) and
+  \texttt{*exp} (hence why \texttt{exp} should point to a {\em writable}
+  location).
+\end{itemize}
+
+For the real \texttt{frexp} function, many refinements are possible: to handle
+the case when \texttt{x} is zero, we can add a different {\em behavior},
+in which the result is also zero. We can handle the cases when \texttt{x} is
+non-finite; we can improve the postcondition by giving the equivalent ACSL
+formula that establishes the mathematical relation between \texttt{x},
+\texttt{*exp} and \verb+\result+; etc.
+
+\section{Useful ACSL predicates}
+
+An ACSL {\em predicate} is a function returning a boolean value.
+Predicates are used as part of expressions, so they are often preceded
+by a backslash. By convention, {\em builtin} ACSL predicates start with
+a backslash, but {\em user-defined} ACSL predicates are not.
+
+The following predicates are abundantly used by \Eva{}:
+\begin{itemize}
+\item \verb+\valid(<locations>)+: expresses the fact that
+  the given <locations> can be {\em written} to; \textbf{note}: it is
+  a common mistake to use \verb+\valid+ when \verb+\valid_read+ is intended
+  (see below);
+\item \verb+\valid_read(<locations>)+: the given locations can be {\em read},
+  e.g. they point to a string literal, or to a location containing memory
+  properly allocated and not yet freed;
+\item \verb+\initialized(<locations>)+: the given locations have a properly
+  initialized value; this does not hold, for instance, for a freshly
+  malloc'ed block, or for uninitialized local variables.
+
+\end{itemize}
+
+\paragraph{Examples}
+
+A simplified version of the \texttt{strcat} specification in \FramaC's libc
+is presented below. As a reminder, \verb+strcat(d, s)+ appends the string
+\texttt{s} at the end of string \texttt{d}.
+
+\begin{lstlisting}
+/*@ requires valid_read_string(src);
+  @ requires valid_read_string(dest);
+  @ requires \valid(dest+(strlen(dest)..strlen(dest)+strlen(src)));
+  @ ensures \result == dest;
+  @ assigns dest[strlen(dest)..strlen(dest)+strlen(src)]
+  @     \from src[0..strlen(src)];
+  @ assigns \result \from dest;
+  @*/
+char *strcat(char *dest, const char *src);
+\end{lstlisting}
+
+Let us read this specification carefully:
+
+\begin{itemize}
+\item the string to be copied (\texttt{src}) must be a valid string,
+  that is, readable and nul-terminated;
+\item the destination string must {\em also} be a valid string
+  (since we are copying {\em after} this string, we need to know where it ends);
+\item there must be enough room, in the buffer pointed to by \texttt{dest},
+  {\em after} the length of \texttt{dest} itself, to store each of the characters
+  of \texttt{src}, including the terminating zero character;
+  this is described via the \verb+\valid+ predicate,
+  which imposes writability of its memory locations, and via a range operator,
+  which avoids having to use a \verb+\forall+ operator;
+\item the postcondition is trivial: it simply returns the destination pointer,
+  unchanged;
+\item there are two \texttt{assigns} clauses, because their \verb+\from+
+  clauses are distinct. The first one states that the function may modify the
+  memory at all locations between the end of the \texttt{dest} string
+  (including its terminating zero character, which is located at
+  \verb+dest[strlen(dest)]+) and \verb|dest[strlen(dest)+strlen(src)]|, which
+  is the end of the newly-concatenated string.
+  The second \texttt{assigns} clause simply states that the result value comes
+  from the pointer \texttt{dest}. This clause is essential, otherwise the
+  postcondition \verb+\result == dest+ cannot hold: in \Eva{}, pointer values
+  coming from specifications must be included in the locations indicated by
+  a \verb+\from+ clause.
+\end{itemize}
+
+Note that the specification above is missing some important points: first, we
+never specify that the bytes in the range
+\verb+dest[strlen(dest)+0..strlen(src)] are identical to those in
+  \verb+src[0..strlen(src)]+. Second, we omitted the fact that \texttt{src}
+  and \texttt{dest} must be {\em disjoint}: \texttt{strcat} does not accept
+  overlapping bytes between source and destination. In ACSL, this is specified
+  via the \verb+\separated(<locations>)+ predicate (see below). This predicate is essential
+  for WP, but in \Eva{} it is present much less often.
+  Third, we never stated that all of the modified bytes were {\em actually}
+  modified, that is: we are {\em certain} that their locations have been
+  written to, and are thus considered \verb+\initialized+.
+
+Finally, here is an example using the \verb+\initialized+ predicate:
+
+\begin{lstlisting}
+volatile time_t __fc_time;
+
+/*@
+  requires \valid(timer);
+  assigns *timer \from __fc_time;
+  ensures \initialized(timer);
+*/
+void time(time_t *timer);
+\end{lstlisting}
+
+This is a simple version of the libc's \texttt{time} function, which
+initializes the \texttt{timer} pointer with the value of the current system
+time (here, modeled by the global variable \verb+__fc_time+).
+
+The important point to notice is that, if we omit the \texttt{ensures} clause,
+the value of \texttt{timer} after the call will always include
+``or UNINITIALIZED'', leading to an alarm before its use.
+
+\section{(Optional) Other useful predicates}
+
+We present here a few more useful predicates, for reference. These are
+sometimes present in the \FramaC standard library specifications.
+
+\subsection*{\textbackslash{}separated}
+
+The \verb+\separated(<locations>)+ predicate states that a set of locations
+are {\em disjoint}, or {\em non-overlapping}, similar to the \texttt{restrict}
+qualifier in C.
+
+\paragraph{Example}
+
+The \texttt{strncpy} function requires source and destination to be
+non-overlapping. For a call to \verb+strncpy(d, s, n)+, this can be written as:
+
+\begin{lstlisting}
+  \separated(d + (0 .. n-1), s + (0 .. n-1));
+\end{lstlisting}
+
+Note that range operators are used to ensure that {\em all} bytes are
+non-overlapping; \verb+\separated(d, s)+ would have been incorrect, since it
+only considers the first byte in each string.
+
+\subsection*{\textbackslash{}subset as Eva-friendly alternative to \textbackslash{}exists}
+
+The \verb+\subset(elem, set)+ predicate is an ``\Eva{}-friendly'' alternative
+to the existential quantifier, \verb+\exists+. \Eva{} is often able to handle the
+former, but rarely the latter.
+
+\paragraph{Example}
+The C library function \texttt{strtod(p, *endp)} parses a floating-point number
+in string form (at \texttt{p}), returns it as a \texttt{double},
+and (optionally) stores the pointer to the string {\em after} the conversion in
+\texttt{endp}. As written in the Linux Programmer's Manual:
+
+\begin{quote}
+  A pointer to the character after the last character used in the conversion
+  is stored in the location referenced by \texttt{endptr}.
+\end{quote}
+
+Therefore, we know that \texttt{*endptr} is {\em somewhere} inside the
+\texttt{ptr} buffer. In ACSL, we can write this as:
+
+\begin{lstlisting}
+  ensures \subset(*endptr, ptr+(0..));
+\end{lstlisting}
+
+This style of writing allows \Eva{} to reduce the values of \texttt{*endptr},
+avoiding the creation of {\em garbled mix}.
+
+\section{Behaviors}
+
+Most C functions, especially those in the C standard library, have at least
+two distinct paths: the ``success'' path and the ``failure'' path.
+Allocating memory, reading a file, writing to a device, performing a
+complex operation... all of these may fail. Specifications for such functions
+may become very imprecise (``everything may happen, therefore any return value
+is possible''), or rely on too many logical implications (e.g.
+\verb+ensures p != \null ==> \result == 0+ \verb+&& p == \null ==> \result != 0;+).
+To help deal with such cases, ACSL has function {\em behaviors}, which allow
+splitting such sets of states, as in the following example of a floating-point
+\texttt{abs} (absolute value) function:
+
+\begin{lstlisting}
+/*@
+  assigns \result \from x;
+  behavior normal:
+    assumes finite_arg: \is_finite(x);
+    ensures res_finite: \is_finite(\result);
+    ensures positive_result: \result >= 0.;
+    ensures equal_magnitude_result: \result == x || \result == -x;
+  behavior infinity:
+    assumes infinite_arg: \is_infinite(x);
+    ensures infinite_result: \is_plus_infinity(\result);
+  behavior nan:
+    assumes nan_arg: \is_NaN(x);
+    ensures nan_result: \is_NaN(\result);
+  complete behaviors;
+  disjoint behaviors;
+*/
+double fabs(double x);
+\end{lstlisting}
+
+This is (or was) the actual, full specification of the function in \FramaC's
+standard library. It contains 3 behaviors, separated according to the
+finiteness of the input value: finite, infinite, or NaN ({\em not a number}).
+
+Each behavior has a named\footnote{Named predicates are an ACSL feature; names,
+or {\em ids}, are described in Section~\ref{sec:acsl-guide-complements},
+{\em ACSL ids}.} {\em assumes} clause, which is the precondition for
+that behavior to be {\em active}. ACSL allows several behaviors to be active
+at the same time, but in practice, having disjoint behaviors (at most one single
+behavior active at any time) simplifies reasoning. When behaviors are disjoint,
+the union of two \texttt{assumes} clauses is always empty.
+
+Ideally, behaviors should be {\em complete}: at least one of them should be
+active at any time\footnote{Hence, as is the case here, a complete and disjoint set
+of behaviors means that exactly one behavior is active at any time}.
+Incomplete behaviors may lead to loss of precision.
+
+Note that several ACSL floating-point predicates are used: \verb+\is_finite+,
+\verb+\is_infinite+, \verb+\is_plus_infinity+ and \verb+\is_NaN+. They are
+explained in Section~\ref{sec:acsl-guide-float}.
+
+\paragraph{(Optional) Assigns clauses in behaviors}
+
+One of the major pain points of ACSL behaviors (besides the size of the
+specification, in number of lines) is the \texttt{assigns} clause:
+they must have a ``default'' clause (one that is outside any behaviors)
+that is a superset of the \texttt{assigns} clauses of each behavior.
+For instance, if a behavior \texttt{a} has a clause \verb+assigns p;+
+and a behavior \texttt{b} has a clause \verb+assigns q;+, then the
+default \texttt{assigns} clause must contain (at least)
+\verb+assigns p, q;+.
+
+The above fact leads to seemingly redundant clauses in some specifications,
+but they are in fact needed.
+
+\section{Floating-point}
+\label{sec:acsl-guide-float}
+
+Floating-point specifications in ACSL contain {\em several} caveats.
+Historically, \Eva{} supported only {\em finite} floating-point numbers,
+thus requiring all specifications to include clauses such as
+\verb+requires \is_finite(x);+.
+
+Nowadays, with 3 different modes related to non-finite\footnote{%
+The distinction between {\em non-finite} and {\em infinite}
+(or {\em infinity}) is subtle: {\em non-finite} includes {\em both}
+positive and negative infinities, as well as NaNs; {\em infinite} only
+includes infinities. Hence why ACSL contains so many predicates.
+The negation of \texttt{\textbackslash{}is\_finite} is {\em not}
+\texttt{\textbackslash{}is\_infinite}!}
+floating-point values (defined by option \texttt{-warn-special-float}:
+\texttt{none}, \texttt{nan} and \texttt{non-finite}), specifications for
+functions in \texttt{math.h} usually should cover all three cases.
+
+By default, relational comparison operators are based on {\em real} numbers,
+not floating-point; many specifications require instead the use of
+predicates such as \verb+gt_double+ and \verb+lt_float+.
+
+Due to such complications, several expressions result in unintuitive behaviors;
+for instance, some specifications require an
+\verb+ensures \is_finite(\result);+ before a more specific ensures, such as
+\verb+ensures \result >= 0.0;+, otherwise \Eva{} is unable to reduce the interval,
+due to the presence of NaNs.
+
+For more complex examples using floats, take a look at the specifications in
+\texttt{math.h}, from the \FramaC standard library.
+
+\section{Dynamic memory allocation}
+
+ACSL has several elements to handle dynamic memory allocation: clauses
+\verb+allocates+ and \verb+frees+, as well as the \verb+\fresh+ predicate.
+Currently, \Eva{} does {\em not} interpret these elements. Instead, \Eva{} has a set
+of builtins and options to handle functions such as \texttt{malloc},
+\texttt{free}, \texttt{realloc}, \texttt{alloca} (non-standard), etc.
+These functions are handled in a special way; their ACSL specifications are not
+currently used by \Eva{}.
+
+Some POSIX functions, such as \texttt{strdup}, perform memory allocation and
+contain \texttt{allocates} clauses. Currently, \Eva{} whitelists the functions
+for which there are {\em implementations} in the \FramaC standard library,
+to ensure \Eva{} handles them correctly. If you want to use a function that
+allocates or frees dynamic memory, you will need to write it in C
+code\footnote{It suffices to write an abstract version of the code, using
+e.g. \FramaC builtins such as \texttt{Frama\_C\_interval}.}, not in ACSL.
+
+\section{Logic versus C}
+\label{sec:acsl-guide-logic}
+
+In ACSL, there is a ``higher level of abstraction'' that sits above the level
+of C constructs: the logic level. In many cases, it can be abstracted away,
+but it is important to remember that it exists.
+
+For instance, numbers (integers and reals) are almost always at the logic
+level, where there are no overflows and no rounding errors. Conversely,
+there are neither floating-point infinities nor NaNs. Take this into account
+when specifying mathematical functions.
+
+There are also logic identifiers which may resemble C library functions
+(e.g. \texttt{strlen}, \texttt{memcmp}, \texttt{pow}), but are defined
+as {\em logic functions}. We do not detail logic functions in this guide;
+just remember that, whenever you see a function name in ACSL,
+it {\em always} refers to a logic function; it is not possible to call
+a C function in an ACSL annotation.
+
+\section{(Optional) Syntax Complements}
+\label{sec:acsl-guide-complements}
+
+We present here a few more details about ACSL syntax; you may skip this until
+you are more familiar with the rest of the guide.
+
+\subsection*{Empty and unbounded ranges}
+
+A range \texttt{l .. u} where $l > u$ is an {\em empty} range; in some
+specifications, this can happen due to variable bounds
+(e.g. \texttt{a[0..n-1]} when \texttt{n} is 0).
+
+The bounds of the range operator (\texttt{l .. u}) are optional: you can write
+\texttt{b[0 ..]}, \texttt{b[.. 2]}, or even \texttt{b[..]}. A missing left
+bound means ``negative infinity'', and a missing right bound means
+``positive infinity''. For instance, \texttt{assigns b[0..]} is useful when
+the upper bound is unknown.
+
+\subsection*{Range tokenization: add spaces between bounds}
+
+An unfortunate combination of preprocessing and parsing of logical annotations
+can lead to unexpected parsing errors. Consider the following code using
+a range operator:
+
+\begin{lstlisting}
+#define N 10
+int main(void) {
+  int a[N] = {0};
+  //@ assert 0 \in a[0..N-1];
+}
+\end{lstlisting}
+
+Parsing the above code fails with
+\texttt{[kernel:annot-error] unbound logic variable N}.
+The issue is that, according to the C standard, \texttt{0..N} is a preprocessing token
+in itself, so that the preprocessor does not see \texttt{N} in isolation, and does not expand
+the macro. To fix this, simply add spaces between the bounds:
+\texttt{a[0 .. N-1]}.
+As a general rule, we recommend {\em always} adding spaces between the bounds.
+
+\subsection*{ACSL ids}
+
+Most ACSL constructs can have one or more {\em ids}, or {\em names}, which are
+C-like identifiers suffixed by a colon (\texttt{:}).
+Some have a semantic impact (e.g., \texttt{indirect} in \texttt{from} clauses,
+as seen in Section~\ref{sec:acsl-guide-indirect}),
+but they are mostly used as clause identifiers: either to
+provide some sort of description, or to help when pretty-printing.
+When a clause has names, they are used instead of printing the whole predicate.
+
+You can add several names by juxtaposing them, e.g.:
+
+\begin{lstlisting}
+  ensures exp_ok: initialization: \initialized(exp);
+\end{lstlisting}
+
+The above clause has two names: \verb+exp_ok+ and \verb+initialization+.
+
+Names are not required to be unique. Uniqueness is never checked.
+
+\section{Remarks concerning Eva}
+
+This section lists some uses and limitations of ACSL annotations that are
+specific to the \Eva{} plugin.
+
+\subsection*{Indirect 'from' clauses}
+\label{sec:acsl-guide-indirect}
+
+Section~\ref{annot_assigns} explains the difference between direct
+and indirect \verb+\from+ clauses. In a very briefly manner,
+\texttt{indirect} \verb+\from+s are more precise, but may result
+in unsound analyses, if the source location contains pointers
+(or parts of pointers).
+
+As a general rule of thumb, if you obtain garbled mix in non-pointer
+variables, in cases where that would have no practical sense, consider
+adding \texttt{indirect:} labels to \verb+\from+ clauses. The \FramaC
+libc can be a source of inspiration.
+
+\subsection*{Disjunctions versus intervals}
+
+In some cases, \Eva{} can obtain more precision from the use of explicit
+disjunctions instead of non-contiguous intervals. The canonical example
+is the suppression of a 0 from the middle of a interval; instead of writing
+this:
+
+\begin{lstlisting}
+  ensures nonzero_result: \result != 0;
+\end{lstlisting}
+
+It is often preferable to write this:
+
+\begin{lstlisting}
+  ensures nonzero_result: \result > 0 || \result < 0;
+\end{lstlisting}
+
+In the first case, unless the sign domain (option \texttt{-eva-domains sign})
+is enabled, there is little chance that \Eva{} will produce an interval without
+zero.
+
+In the second case, if there is enough slevel (or some other disjunction
+mechanism is enabled), \Eva{} will produce two separate states: one with
+\verb+\result > 0+ and another with \verb+\result < 0+,
+at least until both states have to be merged later.
+
+Separate behaviors also enable this kind of disjunctive reasoning.
+
+\section{FAQ / Troubleshooting / Common errors}
+\label{sec:acsl-guide-faq}
+
+This section lists some common error messages, and how to fix them.
+
+\paragraph{Error: cannot use a pointer to void here.}
+Pointer arithmetics in ACSL require non-void pointers. For instance,
+in the \texttt{memcpy} function, which accepts \texttt{void} pointers
+(instead of \texttt{char} pointers), the following is invalid:
+
+\begin{lstlisting}
+  assigns dest[0..n - 1] \from src[0..n-1];
+\end{lstlisting}
+
+You need to explicitly cast the pointers to \texttt{char*}, as in:
+
+\begin{lstlisting}
+  assigns ((char*)dest)[0..n - 1] \from ((char*)src)[0..n-1];
+\end{lstlisting}
+
+\paragraph{Completely invalid destination for assigns clause <A>. Ignoring.}
+This is not an error {\em per se}, but often associated with an incorrect
+\texttt{assigns} clause (e.g. a missing \texttt{\&}). The most common
+legitimate occurrence of this message is when a function has an
+optional outgoing parameter (i.e., ``if \texttt{old} is non-NULL, the previous
+value is saved in \texttt{old}'') and has been called with a null pointer.
+In this case, the message can be safely ignored.
 
 \end{document}