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 a009941107964a0ccc1ad2a87153709a0fe5fba2..f193a1188d9c4316d1ed482ea3b61d2409b14336 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 ------------------------------------------------------------