From a3616e895d21c43d8d3031529eb390cefb3c9379 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 26 Mar 2020 18:17:14 +0100
Subject: [PATCH] [wp] fix sub-float operation
---
src/plugins/wp/Cfloat.ml | 9 ++++++---
src/plugins/wp/Cfloat.mli | 1 +
src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw | 9 +++++++--
.../wp/tests/wp_plugin/oracle/float_real.1.res.oracle | 4 ++--
4 files changed, 16 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 39c437ff77f..24d629f9c2c 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -91,6 +91,7 @@ type op =
| NE
| NEG
| ADD
+ | SUB
| MUL
| DIV
| REAL
@@ -105,6 +106,7 @@ let op_name = function
| NE -> "ne"
| NEG -> "neg"
| ADD -> "add"
+ | SUB -> "sub"
| MUL -> "mul"
| DIV -> "div"
| REAL -> "of"
@@ -275,6 +277,7 @@ let compute_float op ulp xs =
match op , xs with
| NEG , [ x ] -> qmake ulp (Q.neg (exact x))
| ADD , [ x ; y ] -> qmake ulp (Q.add (exact x) (exact y))
+ | SUB , [ x ; y ] -> qmake ulp (Q.sub (exact x) (exact y))
| MUL , [ x ; y ] -> qmake ulp (Q.mul (exact x) (exact y))
| DIV , [ x ; y ] ->
let res = match Q.div (exact x) (exact y) with
@@ -293,6 +296,7 @@ let compute_real op xs =
match op , xs with
| NEG , [ x ] -> F.e_opp x
| ADD , [ x ; y ] -> F.e_add x y
+ | SUB , [ x ; y ] -> F.e_sub x y
| MUL , [ x ; y ] -> F.e_mul x y
| DIV , [ x ; y ] -> F.e_div x y
| (ROUND|REAL) , [ x ] -> x
@@ -350,6 +354,7 @@ let flt_le ft = Compute.get (Context.get model, ft, LE) |> fst
let flt_lt ft = Compute.get (Context.get model, ft, LT) |> fst
let flt_neg ft = Compute.get (Context.get model, ft, NEG) |> fst
let flt_add ft = Compute.get (Context.get model, ft, ADD) |> fst
+let flt_sub ft = Compute.get (Context.get model, ft, SUB) |> fst
let flt_mul ft = Compute.get (Context.get model, ft, MUL) |> fst
let flt_div ft = Compute.get (Context.get model, ft, DIV) |> fst
let flt_of_real ft = Compute.get (Context.get model, ft, ROUND) |> fst
@@ -435,16 +440,14 @@ let fcmp rop fop f x y =
| Float -> p_call (fop f) [x;y]
let fadd = fbinop e_add flt_add
+let fsub = fbinop e_sub flt_sub
let fmul = fbinop e_mul flt_mul
let fdiv = fbinop e_div flt_div
-
let fopp f x =
match Context.get model with
| Real -> e_opp x
| Float -> e_fun ~result:(ftau f) (flt_neg f) [x]
-let fsub f x y = fadd f x (fopp f y)
-
let flt = fcmp p_lt flt_lt
let fle = fcmp p_leq flt_le
let feq = fcmp p_equal flt_eq
diff --git a/src/plugins/wp/Cfloat.mli b/src/plugins/wp/Cfloat.mli
index 344ddbc093e..c685e9139ea 100644
--- a/src/plugins/wp/Cfloat.mli
+++ b/src/plugins/wp/Cfloat.mli
@@ -50,6 +50,7 @@ type op =
| NE
| NEG
| ADD
+ | SUB
| MUL
| DIV
| REAL
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 3cfc3d7f07f..3f1bc5eb1b7 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
@@ -145,10 +145,15 @@ theory Cfloat
function add_f32 (x:f32) (y:f32) : f32 = F32.(.+) x y
function add_f64 (x:f64) (y:f64) : f64 = F64.(.+) x y
+ (* Substraction *)
+
+ function sub_f32 (x:f32) (y:f32) : f32 = F32.(.-) x y
+ function sub_f64 (x:f64) (y:f64) : f64 = F64.(.-) x y
+
(* Multiplication *)
- function mul_f32 (x:f32) (y:f32) : f32 = F32.(.-) x y
- function mul_f64 (x:f64) (y:f64) : f64 = F64.(.-) x y
+ function mul_f32 (x:f32) (y:f32) : f32 = F32.(.*) x y
+ function mul_f64 (x:f64) (y:f64) : f64 = F64.(.*) x y
(* Division *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
index bd279cccc87..4249f034461 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
@@ -13,11 +13,11 @@
Goal Post-condition (file tests/wp_plugin/float_real.i, line 14) in 'dequal':
Assume {
Type: is_sint32(dequal_0).
- If lt_f64(add_f64(x, neg_f64(y)),
+ If lt_f64(sub_f64(x, y),
to_f64((5902958103587057.0/590295810358705651712)))
Then {
If lt_f64(to_f64((-5902958103587057.0/590295810358705651712)),
- add_f64(x, neg_f64(y)))
+ sub_f64(x, y))
Then { (* Return *) Have: dequal_0 = 1. }
Else { (* Return *) Have: dequal_0 = 0. }
}
--
GitLab