[PPL-devel] floating point behaviour

[Roberto Bagnara]

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

-- 
Prof. Roberto Bagnara
Applied Formal Methods Laboratory
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it