From 0f324bf5b98829d654e8a6cf0a6a5e5d19365d09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 May 2020 10:00:41 +0200
Subject: [PATCH] [wp] fix oracles wrt to upgraded float driver
---
.../wp_plugin/oracle/float_driver.res.oracle | 58 +++++++------------
1 file changed, 20 insertions(+), 38 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
index a0099411079..f193a1188d9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
@@ -31,8 +31,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t.
- eq_f64 (add_f64 f (0x1.0000000000000p0:t)) (round_double RTP (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTP (of_f64 f))
end
[wp:print-generated]
theory WP1
@@ -61,8 +60,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t.
- eq_f64 (add_f64 f (0x1.0000000000000p0:t)) (round_double RTZ (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTZ (of_f64 f))
end
[wp:print-generated]
theory WP2
@@ -91,8 +89,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t.
- eq_f64 (add_f64 f (0x1.0000000000000p0:t)) (round_double RNA (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RNA (of_f64 f))
end
[wp:print-generated]
theory WP3
@@ -121,8 +118,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t.
- eq_f64 (add_f64 f (0x1.0000000000000p0:t)) (round_double RNE (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RNE (of_f64 f))
end
[wp:print-generated]
theory WP4
@@ -150,7 +146,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal : forall f:t. is_NaN_f64 (add_f64 f (0x1.0000000000000p0:t))
+ goal wp_goal : forall f:t. is_NaN_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
theory WP5
@@ -178,8 +174,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal :
- forall f:t. is_infinite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ goal wp_goal : forall f:t. is_infinite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
theory WP6
@@ -207,8 +202,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal :
- forall f:t. is_finite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ goal wp_goal : forall f:t. is_finite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
theory WP7
@@ -237,8 +231,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t.
- eq_f64 (add_f64 f (0x1.0000000000000p0:t)) (round_double RTN (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTN (of_f64 f))
end
[wp:print-generated]
theory WP8
@@ -268,8 +261,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
- (round_float RNA1 (of_f32 f))
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RNA1 (of_f32 f))
end
[wp:print-generated]
theory WP9
@@ -299,8 +291,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
- (round_float RNE1 (of_f32 f))
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RNE1 (of_f32 f))
end
[wp:print-generated]
theory WP10
@@ -328,8 +319,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal :
- forall f:t. is_negative_infinite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ goal wp_goal : forall f:t. is_negative_infinite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
theory WP11
@@ -357,8 +347,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal :
- forall f:t. is_positive_infinite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ goal wp_goal : forall f:t. is_positive_infinite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
theory WP12
@@ -386,8 +375,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal :
- forall f:t1. is_finite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ goal wp_goal : forall f:t1. is_finite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
theory WP13
@@ -417,8 +405,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
- (round_float RTN1 (of_f32 f))
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTN1 (of_f32 f))
end
[wp:print-generated]
theory WP14
@@ -448,8 +435,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
- (round_float RTP1 (of_f32 f))
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTP1 (of_f32 f))
end
[wp:print-generated]
theory WP15
@@ -479,8 +465,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
- (round_float RTZ1 (of_f32 f))
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTZ1 (of_f32 f))
end
[wp:print-generated]
theory WP16
@@ -509,8 +494,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
goal wp_goal :
- forall f:t1.
- is_negative_infinite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ forall f:t1. is_negative_infinite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
theory WP17
@@ -539,8 +523,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
goal wp_goal :
- forall f:t1.
- is_positive_infinite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ forall f:t1. is_positive_infinite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
theory WP18
@@ -568,7 +551,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal : forall f:t1. is_NaN_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ goal wp_goal : forall f:t1. is_NaN_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
theory WP19
@@ -596,8 +579,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal :
- forall f:t1. is_infinite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ goal wp_goal : forall f:t1. is_infinite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp] 20 goals generated
------------------------------------------------------------
--
GitLab