🐛 Printing floats/doubles with "printf" does not work

[stnolting]

I was playing around with printf to output some floating-point numbers. Unfortunately, this does not work.

Regardless of the value passed to printf, "0.000000" is always output. In addition, the entire output is corrupted if floats are used with additional format specifiers. For example:

printf("%d, %f", 123, 4.567f);

I have tested several versions of printf:

• the default one, i.e. #include <stdio.h> (newlib)
• optimized versions for embedded applications:
  • https://github.com/mpaland/printf
  • https://github.com/eyalroz/printf
• CoreMark's printf (using HAS_FLOAT)

They all show the same error.

printf makes use of variadic functions. The special thing here is that there is an implicit promotion, e.g. float is automatically promoted to double. However, this seems to break the stack (which is used to pass the variadic arguments). I assume this is because double is 64-bit wide. I carry out further investigations.