On 06/15/10 23:30, piotrm wrote:
That explains most of it. Thanks!
The man page suggest that the restore and set rounding mode are to be used merely if one relies on some rounding mode. I'm not interested in particular rounding modes. I am, however, interested in floats printed in such a way that they can be scanned back in as floats, and "0.:00000" is not an example of such a float. I did notice that restoring rounding mode lets one print floats "correctly" but I'm skeptical that restore/set rounding mode before / after printing things is the intended usage of ppl.
Indeed. But the problem is that you stumbled upon a bug in the implementation of printf(). Apparently, the implementation you are using does weird things when invoked on a non-default rounding mode (notice that ':' is ASCII 3A, one more than ASCII 39, which corresponds to '9').
Unfortunately, if you approach the authors of your printf() and try to convince them that there is a problem, they will react badly (been there, done that). This is the reason why in the PPL we have our own input and output routines. All the best,
Roberto