From 7da8f87b3fac6ab9ff619a0d4f30776b0b330215 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 15 Feb 2021 16:51:44 +0100
Subject: [PATCH] [wp] requires ordering
---
src/plugins/wp/tests/wp/oracle/sharing.res.oracle | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index 1a343c63052..66a855de8d7 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -85,9 +85,12 @@ Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 9).
(* Pre-condition *)
- Have: (0 <= x) /\ (x <= 9) /\ valid_rw(Malloc_0, a, 10) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
- (0 <= Mint_0[shift_sint32(t, i_1)])))).
+ Have: valid_rw(Malloc_0, a, 10).
+ (* Pre-condition *)
+ Have: (0 <= x) /\ (x <= 9).
+ (* Pre-condition *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
+ (0 <= Mint_0[shift_sint32(t, i_1)]))).
}
Prove: 0 <= m_3[shift_sint32(t, 4) <- m_3[a_1]][shift_sint32(t, i)].
--
GitLab