From 9ba680540592515cf10725f4450f12abd6a89953 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 23 Jan 2025 07:46:46 +0100
Subject: [PATCH] [wp] manual typo
---
src/plugins/wp/doc/manual/wp_intro.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex
index 6f6cfd4dc34..f17d7f9fb6f 100644
--- a/src/plugins/wp/doc/manual/wp_intro.tex
+++ b/src/plugins/wp/doc/manual/wp_intro.tex
@@ -414,7 +414,7 @@ which is actually used internally to manage the scope of local variables.
However, \textsf{ACSL} clauses for specifying allocation and deallocation
are not implemented yet (\textit{medium}).
\item[Assigns.]
-The WP strategy for proving assign clauses is a based on a sound but incomplete verification: we check that side effects
+The WP strategy for proving assign clauses is based on a sound but incomplete verification: we check that side effects
(writes and called assigns) are \emph{included} in specified assigns, which
is a sufficient but not necessary condition. The known workaround is to
specify larger assigns and to add the missing equalities to contracts.
--
GitLab