From d779872dd54a73c07d27e62672e8cca75c2fd90c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 19 Feb 2021 10:50:43 +0100
Subject: [PATCH] [wp] duplicated returns
---
.../wp/tests/wp_plugin/oracle/float_real.0.res.oracle | 6 +++---
.../wp/tests/wp_plugin/oracle/float_real.1.res.oracle | 6 +++---
src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle | 3 +--
3 files changed, 7 insertions(+), 8 deletions(-)
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 39e9f3d8359..7925fe574f9 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
@@ -15,10 +15,10 @@ Assume {
If x < ((1.0/100000) + y)
Then {
If y < ((1.0/100000) + x)
- Then { (* Return *) Have: dequal_0 = 1. }
- Else { (* Return *) Have: dequal_0 = 0. }
+ Then { Have: dequal_0 = 1. }
+ Else { Have: dequal_0 = 0. }
}
- Else { (* Return *) Have: dequal_0 = 0. }
+ Else { Have: dequal_0 = 0. }
}
Prove: (abs_real(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 acae1296cda..fcf6b168255 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
@@ -17,10 +17,10 @@ Assume {
Then {
If lt_f64(to_f64((-5902958103587057.0/590295810358705651712)),
sub_f64(x, y))
- Then { (* Return *) Have: dequal_0 = 1. }
- Else { (* Return *) Have: dequal_0 = 0. }
+ Then { Have: dequal_0 = 1. }
+ Else { Have: dequal_0 = 0. }
}
- Else { (* Return *) Have: dequal_0 = 0. }
+ Else { Have: dequal_0 = 0. }
}
Prove: (abs_real(of_f64(x) - of_f64(y)) < (1.0/100000)) <-> (dequal_0 != 0).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
index 0697c55a730..f921ae4ce12 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
@@ -34,10 +34,9 @@ Assume {
Have: i_1 = i.
(* Then *)
Have: Mint_0[shift_sint32(q, j)] <= x.
- (* Return *)
Have: diag_0 = 0.
}
- Else { (* Return *) Have: diag_0 = 1. }
+ Else { Have: diag_0 = 1. }
}
Prove: (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < n) ->
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 < m) ->
--
GitLab