From c24fc1d964d992de9100e5ed1953f2f8504fa965 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 30 Sep 2020 10:56:16 +0200
Subject: [PATCH] [wp] Update tests oracles
---
src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle | 2 +-
src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle | 4 ++++
src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle | 4 ++++
3 files changed, 9 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 fc860528300..45299879b14 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
@@ -36,6 +36,6 @@ Prove: true.
/*@
behavior typed:
requires \separated(message + (..), &size);
- requires \separated(message + (0 .. \at(size,Post)), &size);
+ ensures \separated(message + (0 .. \at(size,Post)), &size);
*/
void receive(int n, char *message);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
index d2e3f2a9cd7..498ce46ee4c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
@@ -59,3 +59,7 @@ Assume {
Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'h':
+ /*@ behavior typed:
+ ensures \separated(\result, &x); */
+ int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
index 115e7900443..9bc96f2981d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
@@ -59,3 +59,7 @@ Assume {
Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'h':
+ /*@ behavior typed_ref:
+ ensures \separated(\result, &x); */
+ int *h(int x);
--
GitLab