diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex index 6f6cfd4dc34282925ea1d95bf711f8021078bd04..f17d7f9fb6fe2828c316d127a1c22c34236f37e2 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.