From 2fbb761bb2f8bcdcabc0d2785b1c5801c9376179 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Jan 2022 13:48:55 +0100
Subject: [PATCH] [wp] Update test oracles

---
 .../wp_plugin/oracle/dynamic.0.res.oracle     |   4 +-
 .../tests/wp_plugin/oracle/flash.1.res.oracle | 116 +++++++++---------
 .../wp_plugin/oracle/float_real.0.res.oracle  |   2 +-
 .../wp_plugin/oracle/float_real.1.res.oracle  |   2 +-
 .../wp/tests/wp_plugin/oracle/math.res.oracle |   2 +-
 5 files changed, 63 insertions(+), 63 deletions(-)

diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle
index 9d876e37568..2f88edb1b06 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle
@@ -23,7 +23,7 @@ Assume {
   (* Heap *)
   Type: (region(closure_0.base) <= 0) /\ framed(Mptr_0).
   (* Pre-condition *)
-  Have: (a = a_1) \/ ((a = a_2) /\ (abs_int(x) <= 5)).
+  Have: (a = a_1) \/ ((a = a_2) /\ (IAbs.abs(x) <= 5)).
 }
 Prove: (a = a_2) \/ (a = a_1).
 
@@ -50,7 +50,7 @@ Assume {
   (* Heap *)
   Type: (region(closure_0.base) <= 0) /\ framed(Mptr_0).
   (* Pre-condition *)
-  Have: abs_int(x) <= 5.
+  Have: IAbs.abs(x) <= 5.
   (* Instance of 'f1' *)
   (* Call point f1 f2 *)
   Have: Mptr_0[shiftfield_F1_S_f(closure_0)] = global(G_f1_22).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
index 4ec72a463c8..77857dc55d0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
@@ -19,21 +19,21 @@ Let a_1 = C_RdAt_int(a).
 Let a_2 = global(G_b_65).
 Let a_3 = C_RdAt_int(a_2).
 Let a_4 = C_WrAt_int(a_2).
-Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
-Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
-Let a_7 = ((a_6)[(a) <- (a_6)[a]+1]).
+Let a_5 = Flash.update(Flash.init, a).
+Let a_6 = Flash.update(a_5, a_2).
+Let a_7 = Flash.update(a_6, a).
 Let x_1 = 1 + RD_time_0.
 Let x_2 = 1 + WR_time_0.
 Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 1.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, (const(0))[a]).
-Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
+Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
 Let x_8 = RD_time_0 - 2.
 Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
-Let x_11 = L_RD_value(a, (a_6)[a]).
+Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
+Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
       is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
@@ -44,22 +44,22 @@ Assume {
   (* Pre-condition *)
   Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_8) = const(0).
+  Have: L_RD_current(x_8) = Flash.init.
   (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = const(0).
+  Have: L_WR_current(WR_time_0) = Flash.init.
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
-  Have: (L_WR_current(x_2) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
+  Have: (L_WR_current(x_2) = Flash.update(Flash.init, a_2)) /\
       (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
   (* Call 'RD' *)
   Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
       (a_7 = L_RD_current(x_1)).
 }
-Prove: (a_7)[a] = 2.
+Prove: Flash.get(a_7, a) = 2.
 
 ------------------------------------------------------------
 
@@ -70,21 +70,21 @@ Let a_1 = C_RdAt_int(a).
 Let a_2 = global(G_b_65).
 Let a_3 = C_RdAt_int(a_2).
 Let a_4 = C_WrAt_int(a_2).
-Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
-Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
-Let a_7 = ((a_6)[(a) <- (a_6)[a]+1]).
+Let a_5 = Flash.update(Flash.init, a).
+Let a_6 = Flash.update(a_5, a_2).
+Let a_7 = Flash.update(a_6, a).
 Let x_1 = 1 + RD_time_0.
 Let x_2 = 1 + WR_time_0.
 Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 1.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, (const(0))[a]).
-Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
+Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
 Let x_8 = RD_time_0 - 2.
 Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
-Let x_11 = L_RD_value(a, (a_6)[a]).
+Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
+Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
       is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
@@ -95,22 +95,22 @@ Assume {
   (* Pre-condition *)
   Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_8) = const(0).
+  Have: L_RD_current(x_8) = Flash.init.
   (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = const(0).
+  Have: L_WR_current(WR_time_0) = Flash.init.
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
-  Have: (L_WR_current(x_2) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
+  Have: (L_WR_current(x_2) = Flash.update(Flash.init, a_2)) /\
       (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
   (* Call 'RD' *)
   Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
       (a_7 = L_RD_current(x_1)).
 }
-Prove: (a_7)[a_2] = 1.
+Prove: Flash.get(a_7, a_2) = 1.
 
 ------------------------------------------------------------
 
@@ -121,21 +121,21 @@ Let a_1 = C_RdAt_int(a).
 Let a_2 = global(G_b_65).
 Let a_3 = C_RdAt_int(a_2).
 Let a_4 = C_WrAt_int(a_2).
-Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
-Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
+Let a_5 = Flash.update(Flash.init, a).
+Let a_6 = Flash.update(a_5, a_2).
 Let x_1 = 1 + WR_time_0.
-Let a_7 = ((const(0))[(a_2) <- (const(0))[a_2]+1]).
+Let a_7 = Flash.update(Flash.init, a_2).
 Let x_2 = RD_time_0 - 1.
 Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 2.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, (const(0))[a]).
-Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
+Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
 Let x_8 = RD_time_0 - 3.
 Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
-Let x_11 = L_RD_value(a, (a_6)[a]).
+Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
+Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
       is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
@@ -145,12 +145,12 @@ Assume {
   (* Pre-condition *)
   Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_8) = const(0).
+  Have: L_RD_current(x_8) = Flash.init.
   (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = const(0).
+  Have: L_WR_current(WR_time_0) = Flash.init.
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -158,9 +158,9 @@ Assume {
       (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
   (* Call 'RD' *)
   Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (((a_6)[(a) <- (a_6)[a]+1]) = L_RD_current(RD_time_0)).
+      (Flash.update(a_6, a) = L_RD_current(RD_time_0)).
 }
-Prove: (a_7)[a_2] = 1.
+Prove: Flash.get(a_7, a_2) = 1.
 
 ------------------------------------------------------------
 
@@ -171,20 +171,20 @@ Let a_1 = C_RdAt_int(a).
 Let a_2 = global(G_b_65).
 Let a_3 = C_RdAt_int(a_2).
 Let a_4 = C_WrAt_int(a_2).
-Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
-Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
+Let a_5 = Flash.update(Flash.init, a).
+Let a_6 = Flash.update(a_5, a_2).
 Let x_1 = 1 + WR_time_0.
 Let x_2 = RD_time_0 - 1.
 Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 2.
 Let a_7 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, (const(0))[a]).
-Let x_7 = x_6 + L_RD_value(a_2, (a_7)[a_2]).
+Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_7, a_2)).
 Let x_8 = RD_time_0 - 3.
 Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
-Let x_11 = L_RD_value(a, (a_6)[a]).
+Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
+Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
 Let x_12 = x_6 + x_10 + x_11.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
@@ -195,20 +195,20 @@ Assume {
   (* Pre-condition *)
   Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_8) = const(0).
+  Have: L_RD_current(x_8) = Flash.init.
   (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = const(0).
+  Have: L_WR_current(WR_time_0) = Flash.init.
   (* Call 'RD' *)
   Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
-  Have: (L_WR_current(x_1) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
+  Have: (L_WR_current(x_1) = Flash.update(Flash.init, a_2)) /\
       (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
   (* Call 'RD' *)
   Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (((a_6)[(a) <- (a_6)[a]+1]) = L_RD_current(RD_time_0)).
+      (Flash.update(a_6, a) = L_RD_current(RD_time_0)).
 }
 Prove: x_12 = (L_RD_value(a, 0) + L_RD_value(a, 1) + L_RD_value(a_2, 0)).
 
@@ -221,20 +221,20 @@ Let a_1 = C_RdAt_int(a).
 Let a_2 = global(G_b_65).
 Let a_3 = C_RdAt_int(a_2).
 Let a_4 = C_WrAt_int(a_2).
-Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
-Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
+Let a_5 = Flash.update(Flash.init, a).
+Let a_6 = Flash.update(a_5, a_2).
 Let x_1 = 1 + WR_time_0.
 Let x_2 = RD_time_0 - 1.
 Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 2.
 Let a_7 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, (const(0))[a]).
-Let x_7 = x_6 + L_RD_value(a_2, (a_7)[a_2]).
+Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_7, a_2)).
 Let x_8 = RD_time_0 - 3.
 Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
-Let x_11 = L_RD_value(a, (a_6)[a]).
+Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
+Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
       is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
@@ -244,20 +244,20 @@ Assume {
   (* Pre-condition *)
   Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_8) = const(0).
+  Have: L_RD_current(x_8) = Flash.init.
   (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = const(0).
+  Have: L_WR_current(WR_time_0) = Flash.init.
   (* Call 'RD' *)
   Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
-  Have: (L_WR_current(x_1) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
+  Have: (L_WR_current(x_1) = Flash.update(Flash.init, a_2)) /\
       (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
   (* Call 'RD' *)
   Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (((a_6)[(a) <- (a_6)[a]+1]) = L_RD_current(RD_time_0)).
+      (Flash.update(a_6, a) = L_RD_current(RD_time_0)).
 }
 Prove: (L_RD_value(a, 0) + L_RD_value(a_2, 0)) = L_WR_value(a_2, 0).
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
index 588faa27370..bfaa684d056 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
@@ -20,6 +20,6 @@ Assume {
   }
   Else { Have: dequal_0 = 0. }
 }
-Prove: (abs_real(x - y) < (1.0/100000)) <-> (dequal_0 != 0).
+Prove: (RAbs.abs(x - y) < (1.0/100000)) <-> (dequal_0 != 0).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
index 263fd5d0c43..03a072084a9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
@@ -22,6 +22,6 @@ Assume {
   }
   Else { Have: dequal_0 = 0. }
 }
-Prove: (abs_real(of_f64(x) - of_f64(y)) < (1.0/100000)) <-> (dequal_0 != 0).
+Prove: (RAbs.abs(of_f64(x) - of_f64(y)) < (1.0/100000)) <-> (dequal_0 != 0).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle
index cdc664a97ca..a6ca689bc81 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle
@@ -231,7 +231,7 @@ Prove: exp(log(r)) = r.
 ------------------------------------------------------------
 
 Goal Post-condition 'min_plus_distrib' in 'ok':
-Prove: (r + min_real(r_1, r_2)) = min_real(r_1 + r, r_2 + r).
+Prove: (r + Rg.min(r_1, r_2)) = Rg.min(r_1 + r, r_2 + r).
 
 ------------------------------------------------------------
 
-- 
GitLab