C front-end: fix signbit(float) behaviour

GCC's __builtin_signbit is type-generic, and therefore does not entail a
cast from float to double. Such a cast would not necessarily preserve
the sign in case of NaN.

Author: tautschnig

regression/cbmc-library/__signbitd-01/main.c

@@ -1,9 +1,14 @@
 #include <assert.h>
 #include <math.h>
 
+int __signbitd(double);
+int __signbitf(float);
+
 int main()
 {
-  __signbitd();
-  assert(0);
+  float f;
+  double df = (double)f;
+  __CPROVER_assert(
+    isnan(f) || __signbitd(df) == __signbitf(f), "cast preserves sign");
   return 0;
 }

regression/cbmc-library/__signbitd-01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

src/ansi-c/compiler_headers/gcc_builtin_headers_math.h

@@ -339,7 +339,7 @@ long double __builtin_scalblnl(long double, long);
 double __builtin_scalbn(double, int);
 float __builtin_scalbnf(float, int);
 long double __builtin_scalbnl(long double, int);
-int __builtin_signbit(double);
+int __builtin_signbit(); // this is type-generic
 int __builtin_signbitf(float);
 int __builtin_signbitl(long double);
 double __builtin_significand(double);

src/ansi-c/library/math.c

@@ -2400,7 +2400,7 @@ float fabsf (float d);
 
 float copysignf(float x, float y)
 {
-  float abs = fabs(x);
+  float abs = fabsf(x);
   return (signbit(y)) ? -abs : abs;
 }