From 61ce82b2ebd2a368cd77cfea5256d879afb20797 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:06:09 +0100
Subject: [PATCH] [wp] useless side-behaviors for smoke tests
---
.../tests/wp_plugin/oracle/doomed.1.res.oracle | 18 ++++++++----------
1 file changed, 8 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle
index 07bf46ceb48..3d1765dc886 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle
@@ -37,11 +37,9 @@ Goal Wp_smoke_default_requires in 'foo':
Assume {
Type: is_sint32(x).
(* Pre-condition *)
- Have: (x < 0) /\ P_REQUIRES(0, x).
- (* Pre-condition for 'A' *)
- Have: (P_ASSUMES(1, x) -> ((3 <= x) /\ P_REQUIRES(1, x))).
- (* Pre-condition for 'B' *)
- Have: (P_ASSUMES(2, x) -> P_REQUIRES(2, x)).
+ Have: P_REQUIRES(0, x).
+ (* Pre-condition *)
+ Have: x < 0.
}
Prove: false.
@@ -62,13 +60,13 @@ Goal Wp_smoke_B_requires in 'foo':
Assume {
Type: is_sint32(x).
(* Pre-condition *)
- Have: (x < 0) /\ P_REQUIRES(0, x).
- (* Pre-condition for 'A' *)
- Have: (P_ASSUMES(1, x) -> ((3 <= x) /\ P_REQUIRES(1, x))).
- (* Pre-condition for 'B' *)
- Have: P_REQUIRES(2, x).
+ Have: P_REQUIRES(0, x).
+ (* Pre-condition *)
+ Have: x < 0.
(* Pre-condition for 'B' *)
Have: P_ASSUMES(2, x).
+ (* Pre-condition for 'B' *)
+ Have: P_REQUIRES(2, x).
}
Prove: false.
--
GitLab