From 30b40154d288b55a89e7cf7a9b8d171087498c7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Mon, 13 Jan 2025 16:33:23 +0100
Subject: [PATCH] [wp] havoc/copied: +changelog +doc:-wp-havoc
---
src/plugins/wp/Changelog | 1 +
src/plugins/wp/doc/manual/wp_plugin.tex | 21 +++++++++++++++++++++
2 files changed, 22 insertions(+)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index ff972427bcc..dabbfb8fb8a 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
Plugin WP <next-release>
###############################################################################
+- WP [2025-01-13] Add option -wp-havoc
- Gui [2024-12-20] Ivette can start interactive provers
###############################################################################
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index d92bc1af04b..9f6608fe5a1 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1100,6 +1100,27 @@ weakest precondition calculus.
it is generally not necessary and it can generates a large number of
verifications for structures with many (nested) fields. \texttt{-1} enables
full unfolding.
+\item[\tt -wp-(no-)havoc] selects the behavior of the copy of compounds (default is \texttt{yes}).\\
+ Starting from version \dots, \texttt{havoc}\footnote{it copies of a memory
+ segment from a source map \texttt{msrc} to a target map \texttt{mtgt},
+ starting at the same location \texttt{loc} of size \texttt{length}, it is
+ mainly used with a fresh source map in the context of an \texttt{assign}.}
+ has been replaced by \texttt{memcpy}\footnote{it copies of a memory segment
+ from a source map \texttt{msrc} at a source location \texttt{lsrc} to a target
+ map \texttt{mtgt} at a target location \texttt{ltgt} of size \texttt{length}.}.\\
+ Originally, the operation \texttt{havoc} was exclusively used instead of
+ \texttt{memcpy}, where the main difference lies in the possibility to
+ specify different locations as source and target.\\
+ When this option is set as \texttt{yes}, the semantics of replacing \texttt{havoc}
+ by \texttt{memcpy} is unchanged. The copy of compounds still interprets as a
+ load from the source followed by a store on a fresh map that is then assumed
+ to be equal to the target. \\
+ When this option is set as \texttt{no}, the semantics of the copy of compounds
+ is a direct \texttt{memcpy} from source map/location to target map/location.
+ Therefore, it no longer uses an intermediate fresh map and lemmas expliciting
+ equality between the modified pre map and the post map.
+
+
\item[\tt -wp-(no)-variant-with-terminates] prove \texttt{loop variant} under
the termination hypothesis (thus, under a
\texttt{terminates \textbackslash{}false}, any loop variant proof is trivial)
--
GitLab