diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 2ea2ab6df824ed0be52537143ac8cf2c5634a23f..fb644a0f70ca24b7b1714e2611c9087bb86abb3f 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2701,7 +2701,8 @@ struct
TUnOp (BNot, t), logic_arithmetic_promotion t.term_type
| PLunop (Uminus, t) ->
let t = type_num_term ctxt env t in
- TUnOp (Neg, t), logic_arithmetic_promotion t.term_type
+ let ty = logic_arithmetic_promotion t.term_type in
+ TUnOp (Neg, mk_cast t ty), ty
| PLunop (Ustar, t) ->
check_current_label loc env;
(* memory access need a current label to have some semantics *)
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 04ccb8f815113a5a3d9fb346bcac84af4a2f55b3..27904b616258b6a4b9830974c0a6dee8cc32b874 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -405,12 +405,17 @@ let () = Context.register
(* --- Models --- *)
(* -------------------------------------------------------------------------- *)
-let register_c_acsl_builtin name lfun ft =
+let hack_sqrt_builtin ft =
+ let choose xs =
+ match Context.get model with
+ | Real -> F.e_fun ~result:t_real Cmath.f_sqrt xs
+ | Float -> F.e_fun ~result:(ftau ft) (f_sqrt ft) xs
+ in
let name = match ft with
- | Float32 -> name ^ "f"
- | Float64 -> name
+ | Float32 -> "sqrtf"
+ | Float64 -> "sqrt"
in
- LogicBuiltins.add_builtin name [F ft] (lfun ft)
+ LogicBuiltins.hack name choose
let () =
let open LogicBuiltins in
@@ -418,7 +423,7 @@ let () =
add_builtin "\\model" [F ft] (f_model ft) ;
add_builtin "\\delta" [F ft] (f_delta ft) ;
add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
- register_c_acsl_builtin "sqrt" f_sqrt ft
+ hack_sqrt_builtin ft
in
register_builtin Float32 ;
register_builtin Float64
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..546f84fc3366d621e3b9a07d038c3439a0842160
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.0.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function test_sqrt
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 25):
+Assume { (* Call 'sqrt' *) Have: .0 <= of_f64(sqrt_f64(q)). }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function test_sqrtf
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 16):
+Assume { (* Call 'sqrtf' *) Have: .0 <= of_f32(sqrt_f32(q)). }
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..21bd47ad8f8b27896414422ee164c0ba892fb82f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sqrt_builtins.1.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function test_sqrt
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 25):
+Assume { (* Call 'sqrt' *) Have: .0 <= sqrt(q). }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function test_sqrtf
+------------------------------------------------------------
+
+Goal Assertion 'KO' (file tests/wp_acsl/sqrt_builtins.i, line 16):
+Assume { (* Call 'sqrtf' *) Have: .0 <= sqrt(q). }
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..93fd64a1995782645dac1594db41018934c5e65e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.0.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_test_sqrtf_assert_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_test_sqrt_assert_KO : Unsuccess
+[wp] Proved goals: 0 / 2
+ Alt-Ergo: 0 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ test_sqrtf - - 1 0.0%
+ test_sqrt - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bd5e2fe0f922aad64e35d47cdb5963c8bec5cb50
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sqrt_builtins.1.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing tests/wp_acsl/sqrt_builtins.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_real_test_sqrtf_assert_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_real_test_sqrt_assert_KO : Unsuccess
+[wp] Proved goals: 0 / 2
+ Alt-Ergo: 0 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ test_sqrtf - - 1 0.0%
+ test_sqrt - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/sqrt_builtins.i b/src/plugins/wp/tests/wp_acsl/sqrt_builtins.i
new file mode 100644
index 0000000000000000000000000000000000000000..a19b233d84f3f9f05c74ece32334fe7365bab66e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/sqrt_builtins.i
@@ -0,0 +1,26 @@
+/* run.config
+ OPT:
+ OPT: -wp-model real
+*/
+/* run.config_qualif
+ OPT:
+ OPT: -wp-model real
+*/
+
+/*@ assigns \nothing;
+ ensures -0. <= sqrtf(x); */
+void sqrtf(float x);
+
+void test_sqrtf(float q){
+ sqrtf(q);
+ /*@ assert KO: \false; */
+}
+
+/*@ assigns \nothing;
+ ensures -0. <= sqrt(x); */
+void sqrt(double x);
+
+void test_sqrt(double q){
+ sqrt(q);
+ /*@ assert KO: \false; */
+}
diff --git a/tests/spec/float-acsl.i b/tests/spec/float-acsl.i
index 41ef751a5c4be79fe7cdd8b12d24b6fd927896b7..8aa4081d0234c937e256ac53c1f7b79177c15468 100644
--- a/tests/spec/float-acsl.i
+++ b/tests/spec/float-acsl.i
@@ -36,3 +36,9 @@ void main() {
float monef = minus_onef();
}
+/*@ requires 0. == -f;
+ requires 0. == f + (-f);
+ requires 0. == -d;
+ requires 0. == d + (-d);
+*/
+void unop_coerce(float f, double d);
diff --git a/tests/spec/oracle/float-acsl.res.oracle b/tests/spec/oracle/float-acsl.res.oracle
index 8073bef4e574f3d166e4f8735853336b0b3c56d0..64f2c44da2b9dd5a2142a61c4631c0cccfbf29b7 100644
--- a/tests/spec/oracle/float-acsl.res.oracle
+++ b/tests/spec/oracle/float-acsl.res.oracle
@@ -42,4 +42,11 @@ void main(void)
return;
}
+/*@ requires 0. ≡ -(â„)f;
+ requires 0. ≡ (â„)f + -(â„)f;
+ requires 0. ≡ -(â„)d;
+ requires 0. ≡ (â„)d + -(â„)d;
+ */
+void unop_coerce(float f, double d);
+