[wp] naming pre-conditions

with associated variable renaming

src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle

@@ -10,7 +10,11 @@ Goal Post-condition 'qed_ok' in 'f':
 Assume {
   Type: is_sint32(x) /\ is_sint32(y).
   (* Pre-condition *)
-  Have: (0 <= x) /\ (0 <= y) /\ (x <= 10) /\ (y <= 10) /\ P_Q(y, x).
+  Have: P_Q(y, x).
+  (* Pre-condition *)
+  Have: (0 <= x) /\ (x <= 10).
+  (* Pre-condition *)
+  Have: (0 <= y) /\ (y <= 10).
 }
 Prove: P_Q(1 + y, 1 + x).
 
@@ -20,17 +24,20 @@ Prove: P_Q(1 + y, 1 + x).
 ------------------------------------------------------------
 
 Goal Post-condition 'qed_ok' in 'g':
-Let x = Mint_0[u].
-Let x_1 = Mint_0[v].
-Let m = Mint_0[u <- 1 + x].
+Let x = Mint_0[v].
+Let x_1 = Mint_0[u].
+Let m = Mint_0[u <- 1 + x_1].
 Let x_2 = m[v].
 Assume {
-  Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
+  Type: is_sint32(x_1) /\ is_sint32(x) /\ is_sint32(x_2).
   (* Heap *)
   Type: (region(u.base) <= 0) /\ (region(v.base) <= 0).
   (* Pre-condition *)
-  Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 10) /\ (x_1 <= 10) /\
-      P_P(Mint_0, u, v).
+  Have: P_P(Mint_0, u, v).
+  (* Pre-condition *)
+  Have: (0 <= x_1) /\ (x_1 <= 10).
+  (* Pre-condition *)
+  Have: (0 <= x) /\ (x <= 10).
 }
 Prove: P_P(m[v <- 1 + x_2], u, v).
 
@@ -49,7 +56,7 @@ Assume {
   Type: is_sint32(x).
   (* Heap *)
   Type: is_sint32(y).
-  (* Pre-condition *)
+  (* Pre-condition 'H' *)
   Have: P_f /\ P_g(x) /\ P_h(y, x) /\ P_w(y, x).
 }
 Prove: P_g(1 + x).
@@ -61,7 +68,7 @@ Assume {
   Type: is_sint32(x).
   (* Heap *)
   Type: is_sint32(y).
-  (* Pre-condition *)
+  (* Pre-condition 'H' *)
   Have: P_f /\ P_g(x) /\ P_h(y, x) /\ P_w(y, x).
 }
 Prove: P_h(y, 1 + x).
@@ -73,7 +80,7 @@ Assume {
   Type: is_sint32(x).
   (* Heap *)
   Type: is_sint32(y).
-  (* Pre-condition *)
+  (* Pre-condition 'H' *)
   Have: P_f /\ P_g(x) /\ P_h(y, x) /\ P_w(y, x).
 }
 Prove: P_w(y, 1 + x).
@@ -98,7 +105,7 @@ Assume {
   Type: is_sint32(y).
   (* Heap *)
   Type: is_sint32(x).
-  (* Pre-condition *)
+  (* Pre-condition 'H' *)
   Have: P_f /\ P_g(x) /\ P_h(y, x) /\ P_w(y, x).
 }
 Prove: P_h(1 + y, x).
@@ -110,7 +117,7 @@ Assume {
   Type: is_sint32(y).
   (* Heap *)
   Type: is_sint32(x).
-  (* Pre-condition *)
+  (* Pre-condition 'H' *)
   Have: P_f /\ P_g(x) /\ P_h(y, x) /\ P_w(y, x).
 }
 Prove: P_w(1 + y, x).