[wp] fix sub-float operation

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

src/plugins/wp/Cfloat.mli

@@ -50,6 +50,7 @@ type op =
   | NE
   | NEG
   | ADD
+  | SUB
   | MUL
   | DIV
   | REAL

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 *)
 

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. }
   }