diff --git a/Makefile b/Makefile
index 9883857d274a05aa0f238c61c5062ee35edcde2f..1668a9d2777578fe6d3149774945eaedd101e369 100644
--- a/Makefile
+++ b/Makefile
@@ -1423,9 +1423,9 @@ $(foreach file,$(LONELY_TESTS_ML_FILES),\
$(foreach file,$(LONELY_TESTS_ML_FILES),\
$(eval $(file:%.ml=%.cmxs): OFLAGS+=-I $(dir $(file))))
.PRECIOUS: $(LONELY_TESTS_ML_FILES:%.ml=%.cmx) \
- $(LONELY_TESTS_DYN_FILES:%.ml=%.cmxs) \
- $(LONELY_TESTS_BYTE_FILES:%.ml=%.cmo) \
- $(LONELY_TESTS_BYTE_FILES:%.ml=%.cmi)
+ $(LONELY_TESTS_ML_FILES:%.ml=%.cmxs) \
+ $(LONELY_TESTS_ML_FILES:%.ml=%.cmo) \
+ $(LONELY_TESTS_ML_FILES:%.ml=%.cmi)
bin/ocamldep_transitive_closure: devel_tools/ocamldep_transitive_closure.ml
$(OCAMLOPT) -package ocamlgraph -package str -linkpkg -o $@ $<
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 92b4d3ab5e75686733875057db959303dcc38b51..918ca0447b734454367bde0b04082b03bec3ff96 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1694,7 +1694,8 @@ struct
- let conditional_conversion loc env t1 t2 =
+ let conditional_conversion loc env rel t1 t2 =
+ let is_rel = Extlib.has_some rel in
(* a comparison is mainly a function of type 'a -> 'a -> Bool/Prop.
performs the needed unifications on both sides.*)
let var = fresh_type_var "cmp" in
@@ -1710,10 +1711,10 @@ struct
in
let rec aux lty1 lty2 =
match (unroll_type lty1), (unroll_type lty2) with
- | t1, t2 when is_same_type t1 t2 -> t1
| Ctype ty1, Ctype ty2 ->
if isIntegralType ty1 && isIntegralType ty2 then
- if (isSignedInteger ty1) <> (isSignedInteger ty2) then
+ if is_same_type lty1 lty2 then lty1
+ else if (isSignedInteger ty1) <> (isSignedInteger ty2) then
(* in ACSL, the comparison between 0xFFFFFFFF seen as int and
unsigned int is not true: we really have to operate at
the integer level.
@@ -1725,9 +1726,25 @@ struct
else if is_enum_cst t1 lty2 then lty2
else if is_enum_cst t2 lty1 then lty1
else Ctype (C.conditionalConversion ty1 ty2)
- else if isArithmeticType ty1 && isArithmeticType ty2 then
- Lreal
- else if is_same_ptr_type ty1 ty2 || is_same_array_type ty1 ty2 then
+ else if isArithmeticType ty1 && isArithmeticType ty2 then begin
+ if is_same_type lty1 lty2 then begin
+ if is_rel then begin
+ let rel = Extlib.the rel in
+ let kind =
+ match Cil.unrollType ty1 with
+ | TFloat (FFloat,_) -> "float"
+ | TFloat (FDouble,_) -> "double"
+ | TFloat (FLongDouble,_) -> "long double"
+ | _ -> Kernel.fatal "floating point type expected"
+ in
+ let source = fst loc in
+ Kernel.warning ~source ~wkey:Kernel.wkey_acsl_float_compare
+ "comparing two %s values as real values. You might \
+ want to use \\%s_%s instead" kind rel kind;
+ Lreal
+ end else lty1
+ end else Lreal
+ end else if is_same_ptr_type ty1 ty2 || is_same_array_type ty1 ty2 then
Ctype (C.conditionalConversion ty1 ty2)
else if
(isPointerType ty1 || isArrayType ty1) &&
@@ -1760,6 +1777,7 @@ struct
(* implicit conversion to set *)
| Ltype ({lt_name = "set"} as lt,[t1]), t2
| t1, Ltype({lt_name="set"} as lt,[t2]) -> Ltype(lt,[aux t1 t2])
+ | t1, t2 when is_same_type t1 t2 -> t1
| _ ->
C.error loc "types %a and %a are not convertible"
Cil_printer.pp_logic_type lty1 Cil_printer.pp_logic_type lty2
@@ -2736,7 +2754,7 @@ struct
let t2 = term env t2 in
let t3 = term env t3 in
let env,ty,ty2,ty3 =
- conditional_conversion loc env t2 t3 in
+ conditional_conversion loc env None t2 t3 in
let t2 = { t2 with term_type = instantiate env t2.term_type } in
let _,t2 =
implicit_conversion
@@ -2977,7 +2995,6 @@ struct
and type_relation:
'a. _ -> _ -> (_ -> _ -> _ -> _ -> 'a) -> _ -> _ -> _ -> 'a =
fun ctxt env f t1 op t2 ->
- let module C = struct end in
let loc1 = t1.lexpr_loc in
let loc2 = t2.lexpr_loc in
let loc = loc_join t1.lexpr_loc t2.lexpr_loc in
@@ -2985,9 +3002,17 @@ struct
let ty1 = t1.term_type in
let t2 = ctxt.type_term ctxt env t2 in
let ty2 = t2.term_type in
+ let rel = match op with
+ | Eq -> "eq"
+ | Neq -> "ne"
+ | Le -> "le"
+ | Lt -> "lt"
+ | Ge -> "ge"
+ | Gt -> "gt"
+ in
let conditional_conversion t1 t2 =
let env,t,ty1,ty2 =
- conditional_conversion loc env t1 t2
+ conditional_conversion loc env (Some rel) t1 t2
in
let t1 = { t1 with term_type = instantiate env t1.term_type } in
let _,t1 =
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 5063b344f1198a3ea61441f44345d12062bb7e8b..9c0399ad475d798fd4f968f5fae4bf5175b29eb7 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -131,6 +131,9 @@ let dkey_visitor = register_category "visitor"
let wkey_annot_error = register_warn_category "annot-error"
let () = set_warn_status wkey_annot_error Log.Wabort
+let wkey_acsl_float_compare = register_warn_category "acsl-float-compare"
+let () = set_warn_status wkey_acsl_float_compare Log.Winactive
+
let wkey_drop_unused = register_warn_category "linker:drop-conflicting-unused"
let wkey_implicit_conv_void_ptr =
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index a5d8940582debc50495088b2b85b87e2610f9678..bc130617463ae326596dafb96a28133d71449c03 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -128,6 +128,8 @@ val dkey_visitor: category
val wkey_annot_error: warn_category
(** error in annotation. If only a warning, annotation will just be ignored. *)
+val wkey_acsl_float_compare: warn_category
+
val wkey_drop_unused: warn_category
val wkey_implicit_conv_void_ptr: warn_category
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 81842f01a2eb694506b55e6640baba76d03a7870..a62ca61f74f49ede1bd466217377af4d37ba2a55 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -45,9 +45,8 @@ let ftau = function
| Float32 -> t32
| Float64 -> t64
-let pp_suffix fmt = function
- | Float32 -> Format.pp_print_string fmt "f32"
- | Float64 -> Format.pp_print_string fmt "f64"
+let ft_suffix = function Float32 -> "f32" | Float64 -> "f64"
+let pp_suffix fmt ft = Format.pp_print_string fmt (ft_suffix ft)
let link phi = Lang.infoprover (Qed.Engine.F_call phi)
@@ -135,15 +134,16 @@ let fmake ulp value = match ulp with
| Float64 -> F.e_fun fq64 [F.e_float value]
let qmake ulp q = fmake ulp (Transitioning.Q.to_float q)
-let mantissa = "\\([-+]?[0-9]*\\)"
-let comma = "\\(.\\(\\(0*[1-9]\\)*\\)0*\\)?"
-let exponent = "\\([eE]\\([-+]?[0-9]*\\)\\)?"
-let suffix = "\\([flFL]\\)?"
-let real = Str.regexp (mantissa ^ comma ^ exponent ^ suffix ^ "$")
+let re_mantissa = "\\([-+]?[0-9]*\\)"
+let re_comma = "\\(.\\(\\(0*[1-9]\\)*\\)0*\\)?"
+let re_exponent = "\\([eE]\\([-+]?[0-9]*\\)\\)?"
+let re_suffix = "\\([flFL]\\)?"
+let re_real =
+ Str.regexp (re_mantissa ^ re_comma ^ re_exponent ^ re_suffix ^ "$")
let parse_literal ~model v r =
try
- if Str.string_match real r 0 then
+ if Str.string_match re_real r 0 then
let has_suffix =
try ignore (Str.matched_group 7 r) ; true
with Not_found -> false in
@@ -217,19 +217,52 @@ let make_pred_float name op ft =
Lang.F.set_builtin phi (compute op ft) ;
REGISTRY.define phi (op,ft) ; phi
-let register = Ctypes.f_memo
+let f_memo = Ctypes.f_memo
-let real_of_flt = register (make_fun_float ~result:Logic.Real "of" REAL)
-let flt_of_real = register (make_fun_float "to" ROUND)
-let flt_add = register (make_fun_float "add" ADD)
-let flt_mul = register (make_fun_float "mul" MUL)
-let flt_div = register (make_fun_float "div" DIV)
-let flt_neg = register (make_fun_float "neg" NEG)
+let real_of_flt = f_memo (make_fun_float ~result:Logic.Real "of" REAL)
+let flt_of_real = f_memo (make_fun_float "to" ROUND)
+let flt_add = f_memo (make_fun_float "add" ADD)
+let flt_mul = f_memo (make_fun_float "mul" MUL)
+let flt_div = f_memo (make_fun_float "div" DIV)
+let flt_neg = f_memo (make_fun_float "neg" NEG)
-let flt_lt = register (make_pred_float "lt" LT)
-let flt_eq = register (make_pred_float "eq" EQ)
-let flt_le = register (make_pred_float "le" LE)
-let flt_neq = register (make_pred_float "ne" NE)
+let flt_lt = f_memo (make_pred_float "lt" LT)
+let flt_eq = f_memo (make_pred_float "eq" EQ)
+let flt_le = f_memo (make_pred_float "le" LE)
+let flt_neq = f_memo (make_pred_float "ne" NE)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Builtins --- *)
+(* -------------------------------------------------------------------------- *)
+
+let register_builtin_comparison suffix ft =
+ begin
+ let open Qed.Logic in
+ let params = [Sdata;Sdata] in
+ let sort = Sprop in
+ let gt = generated_f ~params ~sort "\\gt_%s" suffix in
+ let ge = generated_f ~params ~sort "\\ge_%s" suffix in
+ let open LogicBuiltins in
+ let signature = [F ft;F ft] in
+ add_builtin ("\\eq_" ^ suffix) signature (flt_eq ft) ;
+ add_builtin ("\\ne_" ^ suffix) signature (flt_neq ft) ;
+ add_builtin ("\\lt_" ^ suffix) signature (flt_lt ft) ;
+ add_builtin ("\\le_" ^ suffix) signature (flt_le ft) ;
+ add_builtin ("\\gt_" ^ suffix) signature gt ;
+ add_builtin ("\\ge_" ^ suffix) signature ge ;
+ Context.register
+ begin fun () ->
+ let compute phi x y = e_fun phi [y;x] in
+ Lang.F.set_builtin_2 gt (compute (flt_lt ft)) ;
+ Lang.F.set_builtin_2 ge (compute (flt_le ft)) ;
+ end
+ end
+
+let () =
+ begin
+ register_builtin_comparison "float" Float32 ;
+ register_builtin_comparison "double" Float64 ;
+ end
(* -------------------------------------------------------------------------- *)
(* --- Models --- *)
@@ -238,13 +271,13 @@ let flt_neq = register (make_pred_float "ne" NE)
let () =
begin
let open LogicBuiltins in
- let register ft =
+ let register_builtin ft =
add_builtin "\\model" [F ft] (f_model ft) ;
add_builtin "\\delta" [F ft] (f_delta ft) ;
add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
in
- register Float32 ;
- register Float64 ;
+ register_builtin Float32 ;
+ register_builtin Float64 ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cmath.mli b/src/plugins/wp/Cmath.mli
index e27a286e076c264de3d18f930b477a3019700f5c..7c1510ffdc31ba5d0463ffb389a324544528f07e 100644
--- a/src/plugins/wp/Cmath.mli
+++ b/src/plugins/wp/Cmath.mli
@@ -34,3 +34,5 @@ val f_real_of_int : lfun
val f_iabs : lfun
val f_rabs : lfun
val f_sqrt : lfun
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 1e20d51a4afe8ec605a214a06beb1a050d16bfce..a34105fae018047c8194da662cbf79aa356b8e41 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -214,7 +214,7 @@ let add_logic ~source result name kinds ~library ?category ~link () =
let add_predicate ~source name kinds ~library ~link () =
let params = List.map skind kinds in
- let lfun = Lang.extern_fp ~library ~params ~link name in
+ let lfun = Lang.extern_fp ~library ~params ~link link.altergo in
register ~source name kinds (LFUN lfun)
let add_ctor ~source name kinds ~library ~link () =
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 60c0efae3922f9f7c5b7ae12876965847cd93b65..8f0c5dd0358b15a7b63d478b793b41a13013ee51 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -579,7 +579,11 @@ struct
| L_cint _ ->
L.map Cint.to_integer (C.logic env t)
| L_integer -> C.logic env t
- | L_cfloat _|L_bool|L_pointer _|L_array _ ->
+ | L_cfloat f ->
+ L.map
+ (fun x -> Cmath.int_of_real (Cfloat.real_of_float f x))
+ (C.logic env t)
+ | L_bool|L_pointer _|L_array _ ->
Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
Printer.pp_logic_type src_ltype Printer.pp_logic_type Linteger
diff --git a/src/plugins/wp/doc/manual/wp_builtins.tex b/src/plugins/wp/doc/manual/wp_builtins.tex
index 8b4a2563ac94faa87c2ef0895be5eb693ffebdf0..a556ab01a823cbaf618c55adf9d5bf414628c671 100644
--- a/src/plugins/wp/doc/manual/wp_builtins.tex
+++ b/src/plugins/wp/doc/manual/wp_builtins.tex
@@ -235,6 +235,20 @@ polar coordinates. Definitions imported from the reference implementation of
%---------------------------------------------------------------------------------------------
+\vskip 1em
+\hrule
+\label{builtin-fpcmp}
+\paragraph{$\builtin{le\_float}(x,y)$, $\builtin{ge\_float}(x,y)$,
+$\builtin{lt\_float}(x,y)$, $\builtin{gt\_float}(x,y)$, $\builtin{eq\_float}(x,y)$,
+$\builtin{ne\_float}(x,y)$, $\builtin{le\_double}(x,y)$,
+$\builtin{ge\_double}(x,y)$, $\builtin{lt\_double}(x,y)$,
+$\builtin{gt\_double}(x,y)$, $\builtin{eq\_double}(x,y)$, and
+$\builtin{ne\_double}(x,y)$} for dealing with floating point
+comparisons. They are similar to comparisons over the real numbers if both
+$x$ and $y$ are finite, but obey IEEE semantics for infinities and NaNs
+
+%---------------------------------------------------------------------------------------------
+
\section{Custom Extensions}
As explained in Section~\ref{drivers}, it is possible to extend all the properties mentioned
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 0000000000000000000000000000000000000000..3e039b2cb13d4b139990011bfb807323d54d3c8f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i
@@ -0,0 +1,23 @@
+/*@ 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);
+*/
+
+/*@ 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);
+*/
diff --git a/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json b/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
new file mode 100644
index 0000000000000000000000000000000000000000..8ab9ce87bfcce6699c3d4d058f75fa169519f276
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
@@ -0,0 +1,39 @@
+{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 8 },
+ "wp:main": { "total": 4, "valid": 4, "rank": 8 } },
+ "wp:axiomatics": { "": { "lemma_test_float_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_float_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "wp:section": { "alt-ergo": { "total": 4,
+ "valid": 4,
+ "rank": 8 },
+ "wp:main": { "total": 4,
+ "valid": 4,
+ "rank": 8 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
index c376b86e98ce5ec321a21c7b88f978e7d29d847d..8ce615934da8264b474018856ccfe959b005583b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
@@ -8,17 +8,17 @@
Lemma InfN_not_finite:
Assume: 'InfP_not_finite' 'NaN_not_finite'
-Prove: (not (\is_finite x_0)) \/ (not (\is_minus_infinity x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_negative_infinite_f64 x_0))
------------------------------------------------------------
Lemma InfP_not_finite:
Assume: 'NaN_not_finite'
-Prove: (not (\is_finite x_0)) \/ (not (\is_plus_infinity x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_positive_infinite_f64 x_0))
------------------------------------------------------------
Lemma NaN_not_finite:
-Prove: (not (\is_finite x_0)) \/ (not (\is_NaN x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_NaN_f64 x_0))
------------------------------------------------------------
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 0000000000000000000000000000000000000000..a31e1893ff76431ccf8b5d83313080b8d476d614
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
@@ -0,0 +1,35 @@
+# 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_f64 x_0) -> (is_finite_f64 y_0) -> (le_f64 x_0 y_0)
+ -> ((eq_f64 x_0 y_0) \/ (lt_f64 x_0 y_0))
+
+------------------------------------------------------------
+
+Lemma test_double_compare_greater:
+Assume: 'test_float_compare_greater' 'test_double_compare'
+ 'test_float_compare'
+Prove: (is_finite_f64 x_0) -> (is_finite_f64 y_0) -> (le_f64 y_0 x_0)
+ -> ((eq_f64 x_0 y_0) \/ (lt_f64 y_0 x_0))
+
+------------------------------------------------------------
+
+Lemma test_float_compare:
+Prove: (is_finite_f32 x_0) -> (is_finite_f32 y_0) -> (le_f32 x_0 y_0)
+ -> ((eq_f32 x_0 y_0) \/ (lt_f32 x_0 y_0))
+
+------------------------------------------------------------
+
+Lemma test_float_compare_greater:
+Assume: 'test_double_compare' 'test_float_compare'
+Prove: (is_finite_f32 x_0) -> (is_finite_f32 y_0) -> (le_f32 y_0 x_0)
+ -> ((eq_f32 x_0 y_0) \/ (lt_f32 y_0 x_0))
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..828ad921cb7fc2d46ee73514a319c1d5d5330e5c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 4 goals scheduled
+[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare_greater : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare_greater : Valid
+[wp] Proved goals: 4 / 4
+ Qed: 0
+ Alt-Ergo: 4
+[wp] Report 'tests/wp_acsl/float_compare.i.0.report.json'
+-------------------------------------------------------------
+Axiomatics WP Alt-Ergo Total Success
+Lemma - 4 (28..40) 4 100%
+-------------------------------------------------------------
diff --git a/tests/spec/float-acsl.i b/tests/spec/float-acsl.i
index 3e33afc86d04a3296bb6b760d4d59b1f141bd06b..41ef751a5c4be79fe7cdd8b12d24b6fd927896b7 100644
--- a/tests/spec/float-acsl.i
+++ b/tests/spec/float-acsl.i
@@ -1,3 +1,7 @@
+/* run.config*
+STDOPT: +"-kernel-msg-key printer:logic-coercions" +"-kernel-warn-key acsl-float-compare=active"
+*/
+
/*@
assigns \result \from \nothing;
ensures \le_double(\result, (double)0.0);
@@ -21,6 +25,12 @@ double minus_one(void);
*/
float minus_onef(void);
+/*@ requires x <= y;
+ assigns \result \from x,y;
+ ensures x <= \result <= y;
+*/
+float test(float x, float y);
+
void main() {
double mone = minus_one();
float monef = minus_onef();
diff --git a/tests/spec/oracle/float-acsl.res.oracle b/tests/spec/oracle/float-acsl.res.oracle
index 5489ef5e7841f791f2fffeaa10f5492b5339e044..5ef02bf9f069b305eaa338251ce54fa1f4e16d12 100644
--- a/tests/spec/oracle/float-acsl.res.oracle
+++ b/tests/spec/oracle/float-acsl.res.oracle
@@ -1,4 +1,10 @@
[kernel] Parsing tests/spec/float-acsl.i (no preprocessing)
+[kernel:acsl-float-compare] tests/spec/float-acsl.i:28: Warning:
+ comparing two float values as real values. You might want to use \le_float instead
+[kernel:acsl-float-compare] tests/spec/float-acsl.i:30: Warning:
+ comparing two float values as real values. You might want to use \le_float instead
+[kernel:acsl-float-compare] tests/spec/float-acsl.i:30: Warning:
+ comparing two float values as real values. You might want to use \le_float instead
/* Generated by Frama-C */
/*@ ensures \le_double(\result, (double)0.0);
ensures \ge_double(\result, (double)(-1.0));
@@ -22,6 +28,17 @@ double minus_one(void);
*/
float minus_onef(void);
+/*@ requires
+ /* (coercion to:℠*/x/* ) */ ≤ /* (coercion to:℠*/y/* ) */;
+ ensures
+ /* (coercion to:℠*/\old(x)/* ) */ ≤
+ /* (coercion to:℠*/\result/* ) */ ≤
+ /* (coercion to:â„ */\old(y)/* ) */;
+ assigns \result;
+ assigns \result \from x, y;
+ */
+float test(float x, float y);
+
void main(void)
{
double mone = minus_one();