[WP] Builtin \sign(float64) is not defined
Description
Built-in \sign is not defined in WP.
Builtin \sign(float64) not defined
[wp] Failure: Logic type 'sign' undefined
Steps To Reproduce
Run: frama-c -wp -wp-out . -wp-prover coq -wp-model +float -wp-interactive update just_sign.c
Where just_sign.c
is:
#include <math.h>
/*@
predicate is_same_sign(double X, double Y) = \sign(X) == \sign(Y);
*/
/*@
ensures (is_same_sign(a_double, \result)) ;
assigns \nothing;
*/
double dummy (double a_double) {
return a_double;
}
I got the following output:
[wp] Warning: Missing RTE guards
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] 2 goals scheduled
[wp] Failure: Logic type 'sign' undefined
Expected behaviour
Expected a definition for \sign.
Actual behaviour
WP reports:
[wp] Failure: Logic type 'sign' undefined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0, 25.0 (Manganese), 26.0+dev (Iron) (I tried Several versions)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04 LTS