Skip to content
Snippets Groups Projects
Commit 0f324bf5 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] fix oracles wrt to upgraded float driver

parent 8741df1a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
+ 20
− 38
View file @ 0f324bf5
......@@ -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
------------------------------------------------------------
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment