The official SDCC manual is as follows
printf() The default printf() implementation in printf_large.c does not support float (except on
ds390), only <NO FLOAT> will be printed instead of the value. To enable floating point output, recompile it
with the option -DUSE_FLOATS=1 on the command line. Use --model-large for the mcs51 port, since this uses a
lot of memory. To enable float support for the pic16 targets, see 4.7.9.
I don t know how to correctly add the compilation flag