From ad6228ad7050802ea9ab85a4b79115f5e34e440e Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 6 Oct 2020 14:15:16 +0200
Subject: [PATCH] [eacsl:doc] Update reference and implementation manual
---
src/plugins/e-acsl/doc/refman/intro_modern.tex | 1 -
src/plugins/e-acsl/doc/refman/memory.tex | 2 +-
src/plugins/e-acsl/doc/refman/speclang_modern.tex | 3 +--
3 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index ef546063d84..a8514fc0dd9 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -55,7 +55,6 @@ currently implemented into the \framac's \eacsl plug-in.
& exclusive or operator \\ % \lstinline|^^|
& let bindings \\
& quantifications over non-integer types \\
- & \lstinline|\\separated| \\
& \lstinline|\\specified|
\\
\hline
diff --git a/src/plugins/e-acsl/doc/refman/memory.tex b/src/plugins/e-acsl/doc/refman/memory.tex
index 7626c08e864..c12a065c89a 100644
--- a/src/plugins/e-acsl/doc/refman/memory.tex
+++ b/src/plugins/e-acsl/doc/refman/memory.tex
@@ -10,7 +10,7 @@
| { "\fresh" two-labels? "(" term, term ")" };
| "\valid" { one-label? } "(" location-address ")" ;
| "\valid_read" { one-label? } "(" location-address ")";
- | { "\separated" "(" location-address "," location-addresses ")" };
+ | "\separated" "(" location-address "," location-addresses ")";
\
{ one-label } ::= { "{" id "}" } ;
\
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 686b9c95d32..261843a3906 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -721,8 +721,7 @@ predicates which are related to memory location.
\subsection{Separation}\label{sec:separation}
\nodiff
-\difficultswhy{\notimplemented{\lstinline|\\separated|}}{the implementation of a
- memory model}
+\difficultwhy{\lstinline|\\separated|}{the implementation of a memory model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
--
GitLab