From 06c5aa28e290a3ec9c0d9a8804540e3a3dfe5044 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 24 Nov 2021 13:25:51 +0100
Subject: [PATCH] [Doc] Eva manual: add reference to quick guide annex, and to
ACSL reference
---
doc/value/biblio.bib | 12 +++++++++++-
doc/value/main.tex | 10 ++++++++++
2 files changed, 21 insertions(+), 1 deletion(-)
diff --git a/doc/value/biblio.bib b/doc/value/biblio.bib
index d284b32a7af..177f91a81a8 100644
--- a/doc/value/biblio.bib
+++ b/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}
+}
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 99a1b53c5cd..848066a7e06 100644
--- a/doc/value/main.tex
+++ b/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
--
GitLab