From 4d463015a18bd757a9e6f37cd892a20cecb778b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 18 Sep 2020 14:14:36 +0200
Subject: [PATCH] [wp] reverted post-validity

---
 .../wp/tests/wp_plugin/oracle/post_assigns.res.oracle       | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
index 356a117f24e..0a5c1608e7c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
@@ -34,5 +34,9 @@ Prove: true.
 
 ------------------------------------------------------------
 [wp] Warning: Memory model hypotheses for function 'receive':
-  /*@ behavior typed: requires \separated(&size,message+(..)); */
+  /*@
+     behavior typed:
+       requires \separated(message + (..), &size);
+       requires \separated(message + (0 .. \at(size,Post)), &size);
+     */
   void receive(int n, char *message);
-- 
GitLab