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