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

with also variable renaming
---
 .../tests/wp_plugin/oracle/flash.0.res.oracle | 69 +++++++++++--------
 .../tests/wp_plugin/oracle/flash.1.res.oracle | 69 +++++++++++--------
 2 files changed, 84 insertions(+), 54 deletions(-)

diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
index d987807fecd..f10a2975696 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
@@ -27,16 +27,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 2.
+Let x_6 = RD_time_0 - 2.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\
-      is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
+      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
       is_sint32(x_1) /\ is_sint32(x_2).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\
-      (L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = L_INDEX_init.
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
@@ -71,16 +74,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 2.
+Let x_6 = RD_time_0 - 2.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\
-      is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
+      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
       is_sint32(x_1) /\ is_sint32(x_2).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\
-      (L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = L_INDEX_init.
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
@@ -115,16 +121,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 3.
+Let x_6 = RD_time_0 - 3.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
       is_sint32(x) /\ is_sint32(x_1).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\
-      (L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = L_INDEX_init.
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
@@ -159,16 +168,19 @@ 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, L_RD_access(L_INDEX_init, a)).
-Let x_7 = OBSERVER_time_0 - 3.
-Let x_8 = RD_time_0 - 3.
+Let x_7 = RD_time_0 - 3.
+Let x_8 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_8) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_8) /\ is_sint32(x_7) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
       is_sint32(x) /\ is_sint32(x_1).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\
-      (L_OBSERVER(x_7) = nil) /\ (L_RD_current(x_8) = L_INDEX_init).
+  Have: L_OBSERVER(x_8) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_7) = L_INDEX_init.
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((x_6 + L_RD_value(a_2, L_RD_access(a_7, a_2)))
@@ -203,16 +215,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 3.
+Let x_6 = RD_time_0 - 3.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
       is_sint32(x) /\ is_sint32(x_1).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\
-      (L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = L_INDEX_init.
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
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 31d6bb17966..c950a9aa736 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
@@ -29,16 +29,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 2.
+Let x_6 = RD_time_0 - 2.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\
-      is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
+      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
       is_sint32(x_1) /\ is_sint32(x_2).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\
-      (L_RD_current(x_7) = const(0)).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = const(0).
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
@@ -72,16 +75,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 2.
+Let x_6 = RD_time_0 - 2.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\
-      is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
+      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
       is_sint32(x_1) /\ is_sint32(x_2).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\
-      (L_RD_current(x_7) = const(0)).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = const(0).
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
@@ -115,16 +121,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 3.
+Let x_6 = RD_time_0 - 3.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
       is_sint32(x) /\ is_sint32(x_1).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\
-      (L_RD_current(x_7) = const(0)).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = const(0).
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
@@ -158,16 +167,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_8 = RD_time_0 - 3.
+Let x_7 = RD_time_0 - 3.
+Let x_8 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_8) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_8) /\ is_sint32(x_7) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
       is_sint32(x) /\ is_sint32(x_1).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_7) = nil) /\
-      (L_RD_current(x_8) = const(0)).
+  Have: L_OBSERVER(x_8) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_7) = const(0).
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((x_6 + L_RD_value(a_2, (a_7)[a_2])) = L_WR_value(a_2, (const(0))[a_2])).
@@ -200,16 +212,19 @@ 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 = OBSERVER_time_0 - 3.
-Let x_7 = RD_time_0 - 3.
+Let x_6 = RD_time_0 - 3.
+Let x_7 = OBSERVER_time_0 - 3.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
       is_sint32(x) /\ is_sint32(x_1).
   (* Pre-condition *)
-  Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\
-      (L_RD_current(x_7) = const(0)).
+  Have: L_OBSERVER(x_7) = nil.
+  (* Pre-condition *)
+  Have: L_RD_current(x_6) = const(0).
+  (* Pre-condition *)
+  Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
       ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_7)[a_2]))
-- 
GitLab