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; */
+}