Merge branch 'feature/blanchard/wp/float-missing-bindings' into 'master'

Fixes float missing bindings

See merge request frama-c/frama-c!2595

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)

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";

src/plugins/wp/tests/wp_plugin/float_driver.i

+/* 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;
+}
+

src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle

+# 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))).
+
+------------------------------------------------------------