Support floating-point printing using the "%a" specifier

[eyalroz]

The C standard library printf()-family functions support an %a specifier, which takes a double value and prints it with perfect accuracy in exponent notation with hexadecimal digits. We should support this (although with an option to not-compile this support, like we have for other floating-point capabilities.