diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 0e1f27f8fe7c6c7af264b8131476e2b94af8bb58..716760c0caa9fb48ea24edb8ae13124af93932a4 100644
--- a/nix/internal-tests.nix
+++ b/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 = ''
diff --git a/nix/mk_plugin.nix b/nix/mk_plugin.nix
index 86f1499b69f58016451c24b626b36c636b124ca3..c23ad7e3ac944389e498ac56fea9f3d7db8a9b40 100644
--- a/nix/mk_plugin.nix
+++ b/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;
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index 42f7f396a65cdd2d1f48be36b34d858594f0f4d8..1d76bcf7b822b2174b8805e970d2b4aad8ebefbf 100644
--- a/nix/mk_tests.nix
+++ b/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 =
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
index 4de6bfa872659e98575205b36f6f48e77b2a10f4..181209ac30564df3cf6de4ae48557a32651b92b6 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/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
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index cc9d793793878964707a957cad0e44a44ae56065..461b0b48a332e060ce989c63a9902c8747f92ebd 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/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";
diff --git a/src/plugins/wp/tests/wp_acsl/float_sign.i b/src/plugins/wp/tests/wp_acsl/float_sign.i
new file mode 100644
index 0000000000000000000000000000000000000000..fbe5dfb1ddf2e14173c8ee8df3a9e882464a17fe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_sign.i
@@ -0,0 +1,13 @@
+/*@ 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 ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_sign.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_sign.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dc6f2e327a1edf3c5411403348faccddf5cc0351
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_sign.res.oracle
@@ -0,0 +1,20 @@
+# 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).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_sign.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_sign.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4e83275b930dde89c53ebe852a27cfc1e372a209
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_sign.res.oracle
@@ -0,0 +1,14 @@
+# 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%
+------------------------------------------------------------