From 89185b3e5cac81a75bab55ca3cbe882650670a7b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 15 Feb 2019 16:51:16 +0100
Subject: [PATCH] [WP] add bindings for some ACSL floating-point comparisons

---
 src/plugins/wp/share/wp.driver                |  8 ++++++++
 src/plugins/wp/tests/wp_acsl/float_compare.i  | 11 ++++++++++
 .../wp_acsl/oracle/float_compare.res.oracle   | 20 +++++++++++++++++++
 3 files changed, 39 insertions(+)
 create mode 100644 src/plugins/wp/tests/wp_acsl/float_compare.i
 create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle

diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 7dd358acc69..b46c539ca51 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -105,6 +105,14 @@ predicate "\\is_plus_infinity"(float32) = "is_positive_infinite_f32";
 predicate "\\is_plus_infinity"(float64) = "is_positive_infinite_f64";
 predicate "\\is_minus_infinity"(float32) = "is_negative_infinite_f32";
 predicate "\\is_minus_infinity"(float64) = "is_negative_infinite_f64";
+predicate "\\le_float"(float32,float32) = "le_f32";
+predicate "\\lt_float"(float32,float32) = "lt_f32";
+predicate "\\eq_float"(float32,float32) = "eq_f32";
+predicate "\\ne_float"(float32,float32) = "ne_f64";
+predicate "\\le_double"(float64,float64) = "le_f64";
+predicate "\\lt_double"(float64,float64) = "lt_f64";
+predicate "\\eq_double"(float64,float64) = "eq_f64";
+predicate "\\ne_double"(float64,float64) = "ne_f64";
 logic bool "\\round_float"(rounding_mode,real) = "round_float";
 logic bool "\\round_double"(rounding_mode,real) = "round_double";
 
diff --git a/src/plugins/wp/tests/wp_acsl/float_compare.i b/src/plugins/wp/tests/wp_acsl/float_compare.i
new file mode 100644
index 00000000000..733948471e9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i
@@ -0,0 +1,11 @@
+/*@ lemma test_float_compare:
+      \forall float x,y;
+      \is_finite(x) && \is_finite(y) ==>
+      \le_float(x,y) ==> \lt_float(x,y) || \eq_float(x,y);
+*/
+
+/*@ lemma test_double_compare:
+      \forall double x,y;
+      \is_finite(x) && \is_finite(y) ==> \le_double(x,y) ==>
+         \lt_double(x,y) || \eq_double(x,y);
+*/
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
new file mode 100644
index 00000000000..ddab6355e44
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma test_double_compare:
+Assume: 'test_float_compare'
+Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_double x_0 y_0)
+       -> ((\lt_double x_0 y_0) \/ (\eq_double x_0 y_0))
+
+------------------------------------------------------------
+
+Lemma test_float_compare:
+Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_float x_0 y_0)
+       -> ((\lt_float x_0 y_0) \/ (\eq_float x_0 y_0))
+
+------------------------------------------------------------
-- 
GitLab