Merge branch 'feature/wp/float-sign' into 'master'

[wp] add float ACSL sign function

Closes #2636

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

nix/internal-tests.nix

@@ -118,7 +118,11 @@ stdenvNoCC.mkDerivation rec {
     make tools/ptests/wtests.exe
   '';
 
-  wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git";
+  wp_cache = fetchGit {
+           url = "git@git.frama-c.com:frama-c/wp-cache.git" ;
+           ref = "master" ;
+           shallow = true ;
+         };
 
   doCheck = true;
   preCheck = ''

nix/mk_plugin.nix

@@ -88,7 +88,11 @@ stdenv.mkDerivation {
 
   wp_cache =
     if has-wp-proofs
-    then fetchGit "git@git.frama-c.com:frama-c/wp-cache.git"
+    then fetchGit {
+           url = "git@git.frama-c.com:frama-c/wp-cache.git" ;
+           ref = "master" ;
+           shallow = true ;
+         }
     else "" ;
 
   doCheck = true;

nix/mk_tests.nix

@@ -61,7 +61,11 @@ stdenvNoCC.mkDerivation {
 
   wp_cache =
     if has-wp-proofs
-    then fetchGit "git@git.frama-c.com:frama-c/wp-cache.git"
+    then fetchGit {
+           url = "git@git.frama-c.com:frama-c/wp-cache.git" ;
+           ref = "master" ;
+           shallow = true ;
+         }
     else "" ;
 
   preBuild =

src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw

@@ -39,6 +39,7 @@ theory Cfloat
 
   type f32 = F32.t (* single precision IEEE *)
   type f64 = F64.t (* double precision IEEE *)
+  type sign = Positive | Negative
 
   (* C-Float Conversion *)
 
@@ -175,4 +176,20 @@ theory Cfloat
   function delta_f64 (f:f64) : real = abs( of_f64 f -. model_f64 f )
   function error_f64 (f:f64) : real = (delta_f64 f) /. (abs (model_f64 f))
 
+  (* Sign *)
+
+  function sign_f32 (f: f32) : sign
+
+  axiom positive_f32_sign:
+    forall f:f32. F32.is_positive f <-> sign_f32 f = Positive
+  axiom negative_f32_sign:
+    forall f:f32. F32.is_negative f <-> sign_f32 f = Negative
+
+  function sign_f64 (f: f64) : sign
+
+  axiom positive_f64_sign:
+    forall f:f64. F64.is_positive f <-> sign_f64 f = Positive
+  axiom negative_f64_sign:
+    forall f:f64. F64.is_negative f <-> sign_f64 f = Negative
+
 end

src/plugins/wp/share/wp.driver

@@ -73,6 +73,11 @@ predicate "\\is_minus_infinity"(float32) = "is_negative_infinite_f32";
 predicate "\\is_minus_infinity"(float64) = "is_negative_infinite_f64";
 logic float32 "\\round_float"(rounding_mode,real) = "round_float";
 logic float64 "\\round_double"(rounding_mode,real) = "round_double";
+type "sign" = "sign";
+ctor "\\Positive" = "Positive";
+ctor "\\Negative" = "Negative";
+logic sign "\\sign"(float32) = "sign_f32";
+logic sign "\\sign"(float64) = "sign_f64";
 
 library vset:
 type set = "set";

src/plugins/wp/tests/wp_acsl/float_sign.i

+/*@ predicate is_same_sign_d(double X, double Y) = \sign(X) == \sign(Y);
+    predicate is_same_sign_f(float  X, float  Y) = \sign(X) == \sign(Y);
+*/
+
+/*@ ensures is_same_sign_d(a_double, \result) ; */
+double d (double a_double) {
+  return a_double;
+}
+
+/*@ ensures is_same_sign_f(a_float , \result) ; */
+float  f (float  a_float ) {
+  return a_float ;
+}

src/plugins/wp/tests/wp_acsl/oracle/float_sign.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing float_sign.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function d
+------------------------------------------------------------
+
+Goal Post-condition (file float_sign.i, line 5) in 'd':
+Prove: P_is_same_sign_d(d, d).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f
+------------------------------------------------------------
+
+Goal Post-condition (file float_sign.i, line 10) in 'f':
+Prove: P_is_same_sign_f(f, f).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/float_sign.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing float_sign.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Valid] typed_d_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] typed_f_ensures (Alt-Ergo) (Cached)
+[wp] Proved goals:    2 / 2
+  Alt-Ergo:        2
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  d                         -        1        1       100%
+  f                         -        1        1       100%
+------------------------------------------------------------