[WP] add missing ACSL floating-point comparison operators

src/plugins/wp/Cmath.ml

@@ -82,6 +82,41 @@ let builtin_truncate f e =
       end
   | Fun( f , [e] ) when f == f_real_of_int -> e
   | _ -> raise Not_found
+(* -------------------------------------------------------------------------- *)
+(* --- Float comparisons                                                  --- *)
+(* -------------------------------------------------------------------------- *)
+
+let f_lt_float = f_builtin ~library:"cfloat" ~result:Prop "\\lt_float"
+let f_gt_float =
+  generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\gt_float"
+let () =
+  LogicBuiltins.(
+    add_builtin "\\gt_float" [F Ctypes.Float32; F Ctypes.Float32] f_gt_float)
+let builtin_gt_float x y = e_fun f_lt_float [y; x]
+
+let f_le_float = f_builtin ~library:"cfloat" ~result:Prop "\\le_float"
+let f_ge_float =
+  generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\ge_float"
+let () =
+  LogicBuiltins.(
+    add_builtin "\\ge_float" [F Ctypes.Float32; F Ctypes.Float32] f_ge_float)
+let builtin_ge_float x y = e_fun f_le_float [y; x]
+
+let f_lt_double = f_builtin ~library:"cfloat" ~result:Prop "\\lt_double"
+let f_gt_double =
+  generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\gt_double"
+let () =
+  LogicBuiltins.(
+    add_builtin "\\gt_double" [F Ctypes.Float64; F Ctypes.Float64] f_gt_double)
+let builtin_gt_double x y = e_fun f_lt_double [y; x]
+
+let f_le_double = f_builtin ~library:"cfloat" ~result:Prop "\\le_double"
+let f_ge_double =
+  generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\ge_double"
+let () =
+  LogicBuiltins.(
+    add_builtin "\\ge_double" [F Ctypes.Float64; F Ctypes.Float64] f_ge_double)
+let builtin_ge_double x y = e_fun f_le_double [y; x]
 
 (* -------------------------------------------------------------------------- *)
 (* --- Conversions                                                        --- *)
@@ -347,6 +382,11 @@ let () =
 let () = Context.register
     begin fun () ->
 
+      F.set_builtin_2 f_gt_float builtin_gt_float;
+      F.set_builtin_2 f_ge_float builtin_ge_float;
+      F.set_builtin_2 f_gt_double builtin_gt_double;
+      F.set_builtin_2 f_ge_double builtin_ge_double;
+
       F.set_builtin_1 f_real_of_int builtin_real_of_int ;
       F.set_builtin_1 f_truncate (builtin_truncate f_truncate) ;
       F.set_builtin_1 f_ceil (builtin_truncate f_ceil) ;

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

@@ -9,3 +9,15 @@
       \is_finite(x) && \is_finite(y) ==> \le_double(x,y) ==>
          \lt_double(x,y) || \eq_double(x,y);
 */
+
+/*@ lemma test_float_compare_greater:
+      \forall float x,y;
+      \is_finite(x) && \is_finite(y) ==>
+      \ge_float(x,y) ==> \gt_float(x,y) || \eq_float(x,y);
+*/
+
+/*@ lemma test_double_compare_greater:
+      \forall double x,y;
+      \is_finite(x) && \is_finite(y) ==> \ge_double(x,y) ==>
+         \gt_double(x,y) || \eq_double(x,y);
+*/

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

@@ -13,8 +13,23 @@ Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_double x_0 y_0)
 
 ------------------------------------------------------------
 
+Lemma test_double_compare_greater:
+Assume: 'test_float_compare_greater' 'test_double_compare'
+  'test_float_compare'
+Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_double y_0 x_0)
+       -> ((\lt_double y_0 x_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))
 
 ------------------------------------------------------------
+
+Lemma test_float_compare_greater:
+Assume: 'test_double_compare' 'test_float_compare'
+Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_float y_0 x_0)
+       -> ((\lt_float y_0 x_0) \/ (\eq_float x_0 y_0))
+
+------------------------------------------------------------