Merge branch '898-wp-incorrect-sorting-for-float-builtins' into 'master'

Resolve "[wp] incorrect sorting for float builtins"

Closes #898

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

bin/wp-qualif.sh

+export FRAMAC_WP_CACHE=update
+export FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE)

src/plugins/wp/Lang.ml

@@ -165,8 +165,8 @@ let ext_compare a b = Datatype.Int.compare a.ext_id b.ext_id
 
 let sort_of_object = function
   | C_int _ -> Logic.Sint
-  | C_float _ -> Logic.Sreal
   | C_pointer _ | C_comp _ | C_array _ -> Logic.Sdata
+  | C_float f -> Qed.Kind.of_tau (Context.get floats f)
 
 let init_sort_of_object = function
   | C_int _ | C_float _ | C_pointer _ -> Logic.Sbool

src/plugins/wp/Makefile.in

@@ -174,10 +174,6 @@ wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
 	FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
 	  ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
 
-wp-qualif-env:
-	echo "FRAMAC_WP_CACHE=update"
-	echo "FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE)"
-
 wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
 	@echo "[CACHE] pull cache"
 	@echo "[CACHE] $(WP_QUALIF_CACHE)"

src/plugins/wp/tests/README.md

@@ -105,11 +105,10 @@ environment. To run individual tests, you may now use:
     $ export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
     $ ./bin/ptests.opt src/plugins/wp/tests/xxx/yyy.i -config qualif [-show|-update]
 
-The necessary environment variables can also be displayed by the makefile:
+An utility script is provided to export the necessary environment variables
+(dont forget the `.` to execute the script in the current shell environment):
 
-    $ make wp-qualif-env
-    FRAMAC_WP_CACHE=update
-    FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
+    $ . bin/wp_qualif.sh
 
 As mentionned above, it is _not_ recommanded to globally set the
 `FRAMAC_WP_XXX` variables in your default shell environment, because WP will

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 a = job_0.F1_S_value.
+Assume { (* Pre-condition *) Have: is_finite_f64(a). }
+Prove: eq_f64(a, a).
+
+------------------------------------------------------------
+
+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 : Valid
+[wp] [Qed] Goal typed_job_assigns : Valid
+[wp] Proved goals:    2 / 2
+  Qed:             1 
+  Alt-Ergo:        1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job                       1        1        2       100%
+------------------------------------------------------------