From 76b5af6d9b448334cd2036729e0eae4f98072621 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 19 Feb 2021 10:46:17 +0100
Subject: [PATCH] [wp] naming pre-conditions

---
 .../wp/tests/wp_plugin/oracle/copy.res.oracle |  24 ++-
 .../wp/tests/wp_plugin/oracle/loop.res.oracle |  24 ++-
 .../tests/wp_plugin/oracle/repeat.res.oracle  |  20 ++-
 .../wp_plugin/oracle/sequence.res.oracle      |  10 +-
 .../wp_plugin/oracle/string_c.res.oracle      | 165 ++++++++++--------
 .../tests/wp_plugin/oracle/unroll.res.oracle  |   2 +-
 .../wp_store/oracle/nonaliasing.res.oracle    |  28 ++-
 7 files changed, 173 insertions(+), 100 deletions(-)

diff --git a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
index 2df09a43e2a..0198e43bea6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
@@ -17,7 +17,9 @@ Assume {
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < n).
   (* Pre-condition *)
-  Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: separated(a_1, n, shift_sint32(b, 0), n).
   (* Invariant 'Copy' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
@@ -41,7 +43,9 @@ Assume {
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 <= i).
   (* Pre-condition *)
-  Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: separated(a_1, n, shift_sint32(b, 0), n).
   (* Invariant 'Copy' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
@@ -74,7 +78,9 @@ Assume {
   (* Heap *)
   Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
   (* Pre-condition *)
-  Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: separated(a_1, n, shift_sint32(b, 0), n).
   (* Invariant 'Copy' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       (a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
@@ -109,7 +115,9 @@ Assume {
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < i).
   (* Pre-condition *)
-  Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: separated(a_1, n, shift_sint32(b, 0), n).
   (* Invariant 'Copy' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
@@ -134,7 +142,9 @@ Assume {
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < i).
   (* Pre-condition *)
-  Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: separated(a_1, n, shift_sint32(b, 0), n).
   (* Invariant 'Copy' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
@@ -174,7 +184,9 @@ Assume {
   (* Goal *)
   When: !invalid(Malloc_0, a_3, 1).
   (* Pre-condition *)
-  Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: separated(a_1, n, shift_sint32(b, 0), n).
   (* Invariant 'Copy' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       (a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
index 42f63d8aedb..3c8dd80d459 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
@@ -17,7 +17,9 @@ Assume {
   (* Goal *)
   When: (i_1 <= b) /\ (a <= i_1) /\ is_sint32(i_1).
   (* Pre-condition *)
-  Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
+  Have: valid_rw(Malloc_0, a_1, 1 + b - a).
+  (* Pre-condition *)
+  Have: a <= b.
   (* Invariant 'qed_ok' *)
   Have: forall i_2 : Z. ((a <= i_2) -> ((i_2 < i) ->
       (a_2[shift_sint32(t, i_2)] = e))).
@@ -39,7 +41,9 @@ Assume {
   (* Heap *)
   Type: (region(t.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
-  Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
+  Have: valid_rw(Malloc_0, a_1, 1 + b - a).
+  (* Pre-condition *)
+  Have: a <= b.
   (* Invariant 'qed_ok' *)
   Have: forall i_1 : Z. ((a <= i_1) -> ((i_1 < i) ->
       (havoc(Mint_undef_0, Mint_0, a_1, i - a)[shift_sint32(t, i_1)] = e))).
@@ -58,7 +62,9 @@ Assume {
   (* Heap *)
   Type: (region(t.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
-  Have: (a <= b) /\ valid_rw(Malloc_0, shift_sint32(t, a), 1 + b - a).
+  Have: valid_rw(Malloc_0, shift_sint32(t, a), 1 + b - a).
+  (* Pre-condition *)
+  Have: a <= b.
 }
 Prove: a <= (1 + b).
 
@@ -75,7 +81,9 @@ Assume {
   (* Goal *)
   When: (a <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
   (* Pre-condition *)
-  Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
+  Have: valid_rw(Malloc_0, a_1, 1 + b - a).
+  (* Pre-condition *)
+  Have: a <= b.
   (* Invariant 'qed_ok' *)
   Have: forall i_2 : Z. ((a <= i_2) -> ((i_2 < i) ->
       (a_2[shift_sint32(t, i_2)] = e))).
@@ -116,7 +124,9 @@ Assume {
   (* Goal *)
   When: !invalid(Malloc_0, a_2, 1).
   (* Pre-condition *)
-  Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
+  Have: valid_rw(Malloc_0, a_1, 1 + b - a).
+  (* Pre-condition *)
+  Have: a <= b.
   (* Invariant 'qed_ok' *)
   Have: forall i_1 : Z. ((a <= i_1) -> ((i_1 < i) ->
       (havoc(Mint_undef_0, Mint_0, a_1, i - a)[shift_sint32(t, i_1)] = e))).
@@ -140,7 +150,9 @@ Assume {
   (* Heap *)
   Type: (region(t.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
-  Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
+  Have: valid_rw(Malloc_0, a_1, 1 + b - a).
+  (* Pre-condition *)
+  Have: a <= b.
 }
 Prove: i <= (1 + b).
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
index 02280de6dca..c7250d7a7f3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
@@ -20,7 +20,9 @@ Assume {
   (* Heap *)
   Type: is_sint32(calls_0).
   (* Pre-condition *)
-  Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: L_sequence(calls_0) = nil.
   (* Invariant *)
   Have: ([ 1, 2 ] *^ i) = a.
   (* Invariant *)
@@ -51,7 +53,9 @@ Assume {
   (* Heap *)
   Type: is_sint32(calls_1).
   (* Pre-condition *)
-  Have: (L_sequence(calls_1) = nil) /\ (0 <= n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: L_sequence(calls_1) = nil.
   (* Invariant *)
   Have: (a_2 *^ i) = a.
   (* Invariant *)
@@ -124,7 +128,9 @@ Assume {
   (* Heap *)
   Type: is_sint32(calls_0).
   (* Pre-condition *)
-  Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: L_sequence(calls_0) = nil.
   (* Call 'f' *)
   Have: L_sequence(calls_1) = [ 1 ].
   (* Invariant *)
@@ -147,7 +153,9 @@ Assume {
   (* Heap *)
   Type: is_sint32(calls_0).
   (* Pre-condition *)
-  Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: L_sequence(calls_0) = nil.
   (* Call 'f' *)
   Have: L_sequence(calls_1) = [ 1 ].
   (* Invariant *)
@@ -180,7 +188,9 @@ Assume {
   (* Heap *)
   Type: is_sint32(calls_0).
   (* Pre-condition *)
-  Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
+  Have: 0 <= n.
+  (* Pre-condition *)
+  Have: L_sequence(calls_0) = nil.
   (* Call 'f' *)
   Have: L_sequence(calls_1) = [ 1 ].
   (* Invariant *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
index 62b9c9001fa..1fd2d32b881 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
@@ -278,7 +278,7 @@ Goal Post-condition 'ok,m2' in 'no_calls':
 Assume {
   (* Heap *)
   Type: is_sint32(call_seq_0).
-  (* Pre-condition *)
+  (* Pre-condition 'init' *)
   Have: L_call_obs(call_seq_0) = nil.
 }
 Prove: length(L_call_nil) = 0.
@@ -294,7 +294,7 @@ Goal Post-condition 'ok,n2' in 'no_calls':
 Assume {
   (* Heap *)
   Type: is_sint32(call_seq_0).
-  (* Pre-condition *)
+  (* Pre-condition 'init' *)
   Have: L_call_obs(call_seq_0) = nil.
 }
 Prove: L_call_nil = nil.
@@ -305,7 +305,7 @@ Goal Post-condition 'ok,n3' in 'no_calls':
 Assume {
   (* Heap *)
   Type: is_sint32(call_seq_0).
-  (* Pre-condition *)
+  (* Pre-condition 'init' *)
   Have: L_call_obs(call_seq_0) = nil.
 }
 Prove: L_call_nil = nil.
@@ -319,7 +319,7 @@ Assume {
   Type: is_sint32(call_seq_0).
   (* Goal *)
   When: 0 <= a.
-  (* Pre-condition *)
+  (* Pre-condition 'init' *)
   Have: L_call_obs(call_seq_0) = nil.
 }
 Prove: (L_call_nil = nil) \/ (a <= 0).
@@ -336,7 +336,7 @@ Assume {
   Type: is_sint32(a).
   (* Heap *)
   Type: is_sint32(call_seq_0).
-  (* Pre-condition *)
+  (* Pre-condition 'init' *)
   Have: L_call_obs(call_seq_0) = nil.
 }
 Prove: (L_call_nil = nil) \/ (a <= 0).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index 1774140d9e3..4ec695d3836 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -11,10 +11,12 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n) /\
-      separated(a, n, shift_sint8(src_0, 0), n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'separation' *)
+  Have: separated(a, n, shift_sint8(src_0, 0), n).
   (* Invariant 'no_eva' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       (a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
@@ -41,10 +43,12 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n) /\
-      separated(a, n, shift_sint8(src_0, 0), n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'separation' *)
+  Have: separated(a, n, shift_sint8(src_0, 0), n).
   (* Invariant 'no_eva' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       (a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
@@ -63,10 +67,12 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n) /\
-      separated(shift_sint8(dest_0, 0), n, shift_sint8(src_0, 0), n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'separation' *)
+  Have: separated(shift_sint8(dest_0, 0), n, shift_sint8(src_0, 0), n).
 }
 Prove: 0 <= n.
 
@@ -83,10 +89,12 @@ Assume {
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n) /\
-      separated(a, n, shift_sint8(src_0, 0), n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'separation' *)
+  Have: separated(a, n, shift_sint8(src_0, 0), n).
   (* Invariant 'no_eva' *)
   Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
       (a_1[shift_sint8(src_0, i_2)] = a_1[shift_sint8(dest_0, i_2)]))).
@@ -127,10 +135,12 @@ Assume {
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: !invalid(Malloc_0, a_2, 1).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n) /\
-      separated(a, n, shift_sint8(src_0, 0), n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'separation' *)
+  Have: separated(a, n, shift_sint8(src_0, 0), n).
   (* Invariant 'no_eva' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       (a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
@@ -157,10 +167,12 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n) /\
-      separated(a, n, shift_sint8(src_0, 0), n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'separation' *)
+  Have: separated(a, n, shift_sint8(src_0, 0), n).
   (* Invariant 'no_eva' *)
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
       (a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
@@ -185,9 +197,10 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   If n = 0
   Then { Have: Mchar_1 = Mchar_0. }
   Else {
@@ -256,9 +269,10 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -291,9 +305,10 @@ Assume {
   Type: is_sint32(memoverlap_0) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, s, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, s, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -320,9 +335,10 @@ Assume {
       sconst(Mchar_0).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, s, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, s, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -366,9 +382,10 @@ Assume {
       sconst(Mchar_0).
   (* Goal *)
   When: (i_1 < n) /\ (to_uint64(1 + i) <= i_1).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, s, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, s, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -408,9 +425,10 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -443,9 +461,10 @@ Assume {
   Type: is_sint32(memoverlap_0) /\ is_uint64(n).
   (* Heap *)
   Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, s, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, s, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -472,9 +491,10 @@ Assume {
       sconst(Mchar_0).
   (* Goal *)
   When: (i_1 < n) /\ (to_uint64(i - 1) < i_1).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, s, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, s, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -511,9 +531,10 @@ Assume {
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: (i < n) /\ (to_uint64(n - 1) < i).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -541,9 +562,10 @@ Assume {
       sconst(Mchar_0).
   (* Goal *)
   When: (0 <= i_1) /\ (i_1 <= to_uint64(i - 1)).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, s, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, s, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -598,9 +620,10 @@ Assume {
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: !invalid(Malloc_0, a_3, 1).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -650,9 +673,10 @@ Assume {
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: !invalid(Malloc_0, a_3, 1).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -724,9 +748,10 @@ Assume {
       linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: !invalid(Malloc_0, a, 1).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, d, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, d, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -767,9 +792,10 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
@@ -809,9 +835,10 @@ Assume {
   (* Heap *)
   Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
       linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
-      P_valid_read_or_empty(Malloc_0, src_0, n).
+  (* Pre-condition 'valid_dest' *)
+  Have: P_valid_or_empty(Malloc_0, dest_0, n).
+  (* Pre-condition 'valid_src' *)
+  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
   (* Else *)
   Have: n != 0.
   (* Call 'memoverlap' *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
index 6dc9e4477f0..01b0645e877 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
@@ -13,7 +13,7 @@ Let a = shift_uint32(t, 0).
 Assume {
   (* Heap *)
   Type: (region(t.base) <= 0) /\ linked(Malloc_0).
-  (* Pre-condition *)
+  (* Pre-condition 'access' *)
   Have: valid_rw(Malloc_0, a, 16).
 }
 Prove: P_zeroed(Mint_0[a <- 0][shift_uint32(t, 1) <- 0][shift_uint32(t, 2)
diff --git a/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle b/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle
index 0850a3c16ed..a4e64eb82be 100644
--- a/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle
@@ -22,8 +22,11 @@ Assume {
   (* Goal *)
   When: q != p.
   (* Pre-condition *)
-  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
-      valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
+  Have: valid_rw(Malloc_0, p, 1).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, q, 1).
+  (* Pre-condition *)
+  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
 }
 Prove: x_5 = x_2.
 
@@ -43,8 +46,11 @@ Assume {
   (* Goal *)
   When: q != p.
   (* Pre-condition *)
-  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
-      valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
+  Have: valid_rw(Malloc_0, p, 1).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, q, 1).
+  (* Pre-condition *)
+  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
 }
 Prove: x_2 = x_1.
 
@@ -64,8 +70,11 @@ Assume {
   (* Heap *)
   Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
-  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
-      valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
+  Have: valid_rw(Malloc_0, p, 1).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, q, 1).
+  (* Pre-condition *)
+  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
 }
 Prove: x_5 = x_2.
 
@@ -83,8 +92,11 @@ Assume {
   (* Heap *)
   Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
-  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
-      valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
+  Have: valid_rw(Malloc_0, p, 1).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, q, 1).
+  (* Pre-condition *)
+  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
 }
 Prove: x_2 = x_1.
 
-- 
GitLab