Some of GCC's builtin functions handle floating-point values: http://gcc.gnu.org/onlinedocs/gcc-4.2.4/gcc/Other-Builtins.html
Since the Linux kernel doesn't support floating-point operations by default, would this mean I cannot use these builtin GCC functions within a Linux kernel module?
Would I be able to use them if I did something to this effect (assuming I'm on an x86 system):
kernel_fpu_begin();
float x = 3.14;
x = __builtin_ceil(x);
kernel_fpu_end();