Consider the following code:
System.out.printf("%f%n", 123456796f);
This prints 123456800
on my system, so the value was rounded up by 4. Is rounding up mandated in this situation, or could the compiler have decided to round down by 4 just as well, yielding 123456792
?