Author skrah
Recipients Amaury.Forgeot.d'Arc, amaury.forgeotdarc, brian.curtin, casevh, ced, eric.smith, eric.snow, haypo, jjconti, mark.dickinson, pitrou, rhettinger, skrah
Date 2012-02-23.17:33:52
SpamBayes Score 3.69352e-10
Marked as misclassified No
Message-id <1330018433.14.0.672501581514.issue7652@psf.upfronthosting.co.za>
In-reply-to
Content
Over the last two months I've done a full review of all files except
_decimal.c and mpdecimal.c.

I now have additional ACL2 proofs for a couple of functions in basearith.c
(some are partial proofs), a full proof for the special case (d = 10**19)
of Granlund/Montgomery's "Divide double word by constant" algorithm and a
full proof for the Chinese Remainder Theorem in crt.c.


I didn't find anything important. I found a couple of useless variable
initializations, missing comments etc.

There was one (deliberate) incompatibility in the format function:
If rounding lead to an Overflow, _decimal printed 'Infinity'.

_decimal can't read back numbers that are out of bounds, so this
was done to ensure that a roundtrip is always possible.


But I changed the function so _decimal now uses exactly the same algorithm
for formatting as decimal.py.
History
Date User Action Args
2012-02-23 17:33:53skrahsetrecipients: + skrah, rhettinger, amaury.forgeotdarc, mark.dickinson, pitrou, haypo, casevh, eric.smith, jjconti, ced, brian.curtin, Amaury.Forgeot.d'Arc, eric.snow
2012-02-23 17:33:53skrahsetmessageid: <1330018433.14.0.672501581514.issue7652@psf.upfronthosting.co.za>
2012-02-23 17:33:52skrahlinkissue7652 messages
2012-02-23 17:33:52skrahcreate