[wp] exhibit issue with float fields

src/plugins/wp/tests/wp_bts/issue_898.i

+struct S {
+  int valid;
+  double value;
+};
+
+/*@
+  requires \is_finite(val);
+  ensures \eq_double(\result.value,val);
+  assigns \nothing;
+*/
+struct S job(double val) {
+  struct S result = { 0, val };
+  return result;
+}

src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_898.i, line 8) in 'job':
+Let r = job_0.F1_S_value.
+Assume { (* Pre-condition *) Have: is_finite_f64(r). }
+Prove: eq_f64(r, r).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_job_ensures : Failed
+  [Why3 Error] Type mismatch between ieee_float.Float64.t and real
+[wp] [Qed] Goal typed_job_assigns : Valid
+[wp] Proved goals:    1 / 2
+  Qed:             1 
+  Alt-Ergo:        0  (failed: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job                       1        -        2      50.0%
+------------------------------------------------------------