From b9db0c620c8863f4cdd99fa63fef021131a34f68 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 21 Sep 2020 16:57:19 +0200
Subject: [PATCH] [wp] Update test oracle
---
.../wp/tests/wp_acsl/oracle/base_offset.res.oracle | 8 +++++---
.../wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle | 8 ++++----
2 files changed, 9 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
index 436b0b25bcc..fcc2455baea 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
@@ -17,13 +17,15 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/base_offset.i, line 15) in 'f':
-Let x = p.offset.
+Let x = p.base.
+Let x_1 = base_offset_table(x).
+Let x_2 = p.offset.
Assume {
(* Heap *)
- Type: region(p.base) <= 0.
+ Type: region(x) <= 0.
(* Goal *)
When: (0 <= i) /\ (i <= i_1) /\ (i_1 <= 3).
}
-Prove: base_offset(1 + i + x) <= base_offset(1 + i_1 + x).
+Prove: base_offset(x_1, 1 + i + x_2) <= base_offset(x_1, 1 + i_1 + x_2).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
index a8fdef13518..8b29211f4ec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
@@ -5,11 +5,11 @@
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_ensures : Valid
[wp] [Qed] Goal typed_f_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_f_ensures_3 : Unsuccess
-[wp] Proved goals: 2 / 3
+[wp] [Alt-Ergo] Goal typed_f_ensures_3 : Valid
+[wp] Proved goals: 3 / 3
Qed: 2
- Alt-Ergo: 0 (unsuccess: 1)
+ Alt-Ergo: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- f 2 - 3 66.7%
+ f 2 1 3 100%
------------------------------------------------------------
--
GitLab