From ba2d8db96bbf84d07474e2c1cc1af6c91e5d444a 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:23:45 +0100
Subject: [PATCH] [wp] behaviors ordering

---
 .../tests/wp/oracle/wp_behavior.0.res.oracle  | 52 +++++++++----------
 .../tests/wp/oracle/wp_behavior.1.res.oracle  | 28 +++++-----
 2 files changed, 40 insertions(+), 40 deletions(-)

diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
index c377eb93bf7..641adaa8192 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
@@ -67,12 +67,12 @@ Goal Post-condition for 'X' (file tests/wp/wp_behavior.i, line 28) in 'behaviors
 Assume {
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'Y' *)
-  Have: (P_CY -> P_RY).
-  (* Pre-condition for 'X' *)
-  Have: P_RX.
   (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
+  (* Pre-condition for 'Y' *)
+  Have: (P_CY -> P_RY).
   (* Assertion *)
   Have: P_Q.
 }
@@ -91,12 +91,12 @@ Assume {
   When: !invalid(Malloc_0, px_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'Y' *)
-  Have: (P_CY -> P_RY).
-  (* Pre-condition for 'X' *)
-  Have: P_RX.
   (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
+  (* Pre-condition for 'Y' *)
+  Have: (P_CY -> P_RY).
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -116,12 +116,12 @@ Assume {
   When: !invalid(Malloc_0, py_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'Y' *)
-  Have: (P_CY -> P_RY).
-  (* Pre-condition for 'X' *)
-  Have: P_RX.
   (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
+  (* Pre-condition for 'Y' *)
+  Have: (P_CY -> P_RY).
   (* Assertion *)
   Have: P_Q.
 }
@@ -136,12 +136,12 @@ Goal Post-condition for 'Y' (file tests/wp/wp_behavior.i, line 33) in 'behaviors
 Assume {
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'X' *)
-  Have: (P_CX -> P_RX).
-  (* Pre-condition for 'Y' *)
-  Have: P_RY.
   (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
+  (* Pre-condition for 'X' *)
+  Have: (P_CX -> P_RX).
   (* Assertion *)
   Have: P_Q.
 }
@@ -160,12 +160,12 @@ Assume {
   When: !invalid(Malloc_0, px_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'X' *)
-  Have: (P_CX -> P_RX).
-  (* Pre-condition for 'Y' *)
-  Have: P_RY.
   (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
+  (* Pre-condition for 'X' *)
+  Have: (P_CX -> P_RX).
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -185,12 +185,12 @@ Assume {
   When: !invalid(Malloc_0, py_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'X' *)
-  Have: (P_CX -> P_RX).
-  (* Pre-condition for 'Y' *)
-  Have: P_RY.
   (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
+  (* Pre-condition for 'X' *)
+  Have: (P_CX -> P_RX).
   (* Assertion *)
   Have: P_Q.
 }
@@ -321,9 +321,9 @@ Assume {
   (* Pre-condition for 'X' *)
   Have: P_CX.
   (* Pre-condition for 'X' *)
-  Have: P_RX1.
-  (* Pre-condition for 'X' *)
   Have: P_RX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX1.
 }
 Prove: q = p.
 
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
index 8d98a45587a..96a885bba32 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
@@ -38,9 +38,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'X' *)
-  Have: P_RX.
-  (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
   (* Assertion *)
   Have: P_Q.
 }
@@ -60,9 +60,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'X' *)
-  Have: P_RX.
-  (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -83,9 +83,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'X' *)
-  Have: P_RX.
-  (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
   (* Assertion *)
   Have: P_Q.
 }
@@ -101,9 +101,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'Y' *)
-  Have: P_RY.
-  (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
   (* Assertion *)
   Have: P_Q.
 }
@@ -123,9 +123,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'Y' *)
-  Have: P_RY.
-  (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -146,9 +146,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'Y' *)
-  Have: P_RY.
-  (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
   (* Assertion *)
   Have: P_Q.
 }
@@ -279,9 +279,9 @@ Assume {
   (* Pre-condition for 'X' *)
   Have: P_CX.
   (* Pre-condition for 'X' *)
-  Have: P_RX1.
-  (* Pre-condition for 'X' *)
   Have: P_RX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX1.
 }
 Prove: q = p.
 
-- 
GitLab