diff --git a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
index aaedd4489efc3d61a0113eca8f6e2a3265efe616..3cfc3d7f07f7a38907537385c65ad9b590d72ee1 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
@@ -76,6 +76,19 @@ theory Cfloat
axiom to_f64_minus_infinity: forall x. x <. -. F64.max_real -> is_negative_infinite_f64 (to_f64 x)
axiom to_f64_plus_infinity: forall x. x >. F64.max_real -> is_positive_infinite_f64 (to_f64 x)
+ (* Note: This is OK as we have in Why3 ieee_float:
+
+ axiom Round_idempotent :
+ forall m1 m2:mode, x:real. round m1 (round m2 x) = round m2 x
+
+ So we can round RNE (to_f32/64 behavior) after any rounding.
+ *)
+ function round_float (m: Rounding.mode) (r: real) : f32 =
+ to_f32 (F32.round m r)
+
+ function round_double (m: Rounding.mode) (r: real) : f64 =
+ to_f64 (F64.round m r)
+
(* Take care of +0/-0 *)
axiom is_zero_to_f32_zero: F32.is_zero (to_f32 0.0)
axiom is_zero_to_f64_zero: F64.is_zero (to_f64 0.0)
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index a45458db4a8e2e45fad08bb5e3f95c4aa16a51fd..2fb2f16fed142915eca73e2608c793101ca59cf3 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -96,12 +96,12 @@ coq.file += "coqwp:real/Abs.v";
coq.file += "coqwp/Cfloat.v";
why3.import += "frama_c_wp.cfloat.Cfloat";
altergo.file += "ergo/Cfloat.mlw";
-type "rounding_mode" = "rounding_mode";
-ctor "\\Up"() = "Up";
-ctor "\\Down"() = "Down";
-ctor "\\ToZero"() = "ToZero";
-ctor "\\NearestAway"() = "NearestTiesToAway";
-ctor "\\NearestEven"() = "NearestTiesToEven";
+type "rounding_mode" = "Rounding.mode";
+ctor "\\Up"() = "Rounding.RTP";
+ctor "\\Down"() = "Rounding.RTN";
+ctor "\\ToZero"() = "Rounding.RTZ";
+ctor "\\NearestAway"() = "Rounding.RNA";
+ctor "\\NearestEven"() = "Rounding.RNE";
predicate "\\is_finite"(float32) = "is_finite_f32";
predicate "\\is_finite"(float64) = "is_finite_f64";
predicate "\\is_NaN"(float32) = "is_NaN_f32";
@@ -112,8 +112,8 @@ predicate "\\is_plus_infinity"(float32) = "is_positive_infinite_f32";
predicate "\\is_plus_infinity"(float64) = "is_positive_infinite_f64";
predicate "\\is_minus_infinity"(float32) = "is_negative_infinite_f32";
predicate "\\is_minus_infinity"(float64) = "is_negative_infinite_f64";
-logic bool "\\round_float"(rounding_mode,real) = "round_float";
-logic bool "\\round_double"(rounding_mode,real) = "round_double";
+logic float32 "\\round_float"(rounding_mode,real) = "round_float";
+logic float64 "\\round_double"(rounding_mode,real) = "round_double";
library vset:
type set = "set";
diff --git a/src/plugins/wp/tests/wp_plugin/float_driver.i b/src/plugins/wp/tests/wp_plugin/float_driver.i
new file mode 100644
index 0000000000000000000000000000000000000000..da87cc93b3693ebfeb808388eec1d2a9fb17654f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/float_driver.i
@@ -0,0 +1,39 @@
+/* run.config
+ OPT:-wp -wp-gen -wp-prover why3 -wp-msg-key="print-generated"
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+/*@
+ ensures DBL_RNE: \eq_double(\result,\round_double(\NearestEven, x));
+ ensures DBL_RNA: \eq_double(\result,\round_double(\NearestAway, x));
+ ensures DBL_RTZ: \eq_double(\result,\round_double(\ToZero, x));
+ ensures DBL_RTP: \eq_double(\result,\round_double(\Up, x));
+ ensures DBL_RTN: \eq_double(\result,\round_double(\Down, x));
+ ensures DBL_FIN: \is_finite(\result);
+ ensures DBL_INF: \is_infinite(\result);
+ ensures DBL_NAN: \is_NaN(\result);
+ ensures DBL_PINF: \is_plus_infinity(\result);
+ ensures DBL_MINF: \is_minus_infinity(\result);
+*/
+double for_double(double x) {
+ return x+1.0;
+}
+
+/*@
+ ensures FLT_RNE: \eq_float(\result,\round_float(\NearestEven, x));
+ ensures FLT_RNA: \eq_float(\result,\round_float(\NearestAway, x));
+ ensures FLT_RTZ: \eq_float(\result,\round_float(\ToZero, x));
+ ensures FLT_RTP: \eq_float(\result,\round_float(\Up, x));
+ ensures FLT_RTN: \eq_float(\result,\round_float(\Down, x));
+ ensures FLT_FIN: \is_finite(\result);
+ ensures FLT_INF: \is_infinite(\result);
+ ensures FLT_NAN: \is_NaN(\result);
+ ensures FLT_PINF: \is_plus_infinity(\result);
+ ensures FLT_MINF: \is_minus_infinity(\result);
+*/
+float for_float(float x) {
+ return x+1.0f;
+}
+
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
new file mode 100644
index 0000000000000000000000000000000000000000..a009941107964a0ccc1ad2a87153709a0fe5fba2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
@@ -0,0 +1,708 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/float_driver.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 20 goals scheduled
+[wp:print-generated]
+ theory WP
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* 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))
+ end
+[wp:print-generated]
+ theory WP1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* 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))
+ end
+[wp:print-generated]
+ theory WP2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* 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))
+ end
+[wp:print-generated]
+ theory WP3
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* 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))
+ end
+[wp:print-generated]
+ theory WP4
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal : forall f:t. is_NaN_f64 (add_f64 f (0x1.0000000000000p0:t))
+ end
+[wp:print-generated]
+ theory WP5
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t. is_infinite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ end
+[wp:print-generated]
+ theory WP6
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t. is_finite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ end
+[wp:print-generated]
+ theory WP7
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* 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))
+ end
+[wp:print-generated]
+ theory WP8
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ (round_float RNA1 (of_f32 f))
+ end
+[wp:print-generated]
+ theory WP9
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ (round_float RNE1 (of_f32 f))
+ end
+[wp:print-generated]
+ theory WP10
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t. is_negative_infinite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ end
+[wp:print-generated]
+ theory WP11
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t. is_positive_infinite_f64 (add_f64 f (0x1.0000000000000p0:t))
+ end
+[wp:print-generated]
+ theory WP12
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1. is_finite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ end
+[wp:print-generated]
+ theory WP13
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ (round_float RTN1 (of_f32 f))
+ end
+[wp:print-generated]
+ theory WP14
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ (round_float RTP1 (of_f32 f))
+ end
+[wp:print-generated]
+ theory WP15
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ (round_float RTZ1 (of_f32 f))
+ end
+[wp:print-generated]
+ theory WP16
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ is_negative_infinite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ end
+[wp:print-generated]
+ theory WP17
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ is_positive_infinite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ end
+[wp:print-generated]
+ theory WP18
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal : forall f:t1. is_NaN_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ end
+[wp:print-generated]
+ theory WP19
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1. is_infinite_f32 (add_f32 f (0x1.0000000000000p0:t1))
+ end
+[wp] 20 goals generated
+------------------------------------------------------------
+ Function for_double
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_RNE' in 'for_double':
+Prove: eq_f64(add_f64(x, to_f64(1.0)), round_double(Rounding.RNE, of_f64(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_RNA' in 'for_double':
+Prove: eq_f64(add_f64(x, to_f64(1.0)), round_double(Rounding.RNA, of_f64(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_RTZ' in 'for_double':
+Prove: eq_f64(add_f64(x, to_f64(1.0)), round_double(Rounding.RTZ, of_f64(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_RTP' in 'for_double':
+Prove: eq_f64(add_f64(x, to_f64(1.0)), round_double(Rounding.RTP, of_f64(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_RTN' in 'for_double':
+Prove: eq_f64(add_f64(x, to_f64(1.0)), round_double(Rounding.RTN, of_f64(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_FIN' in 'for_double':
+Prove: is_finite_f64(add_f64(x, to_f64(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_INF' in 'for_double':
+Prove: is_infinite_f64(add_f64(x, to_f64(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_NAN' in 'for_double':
+Prove: is_NaN_f64(add_f64(x, to_f64(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_PINF' in 'for_double':
+Prove: is_positive_infinite_f64(add_f64(x, to_f64(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'DBL_MINF' in 'for_double':
+Prove: is_negative_infinite_f64(add_f64(x, to_f64(1.0))).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function for_float
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_RNE' in 'for_float':
+Prove: eq_f32(add_f32(x, to_f32(1.0)), round_float(Rounding.RNE, of_f32(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_RNA' in 'for_float':
+Prove: eq_f32(add_f32(x, to_f32(1.0)), round_float(Rounding.RNA, of_f32(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_RTZ' in 'for_float':
+Prove: eq_f32(add_f32(x, to_f32(1.0)), round_float(Rounding.RTZ, of_f32(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_RTP' in 'for_float':
+Prove: eq_f32(add_f32(x, to_f32(1.0)), round_float(Rounding.RTP, of_f32(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_RTN' in 'for_float':
+Prove: eq_f32(add_f32(x, to_f32(1.0)), round_float(Rounding.RTN, of_f32(x))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_FIN' in 'for_float':
+Prove: is_finite_f32(add_f32(x, to_f32(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_INF' in 'for_float':
+Prove: is_infinite_f32(add_f32(x, to_f32(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_NAN' in 'for_float':
+Prove: is_NaN_f32(add_f32(x, to_f32(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_PINF' in 'for_float':
+Prove: is_positive_infinite_f32(add_f32(x, to_f32(1.0))).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FLT_MINF' in 'for_float':
+Prove: is_negative_infinite_f32(add_f32(x, to_f32(1.0))).
+
+------------------------------------------------------------