[Ada] Fix another error in multi-precision division used in ELIMINATED mode

Message ID 20121106100117.GA8927@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Nov. 6, 2012, 10:01 a.m.
The ELIMINATED overlow mode uses a multi-precision integer arithmetic package
that depends on algorithm D from Knuth for multi-precision division. This
algorithm was recently corrected for an overflow problem, applying a patch from
1995. This version still had a bug, which was corrected in 2005. This patch
applies this correction (see code of Div_Rem in s-bignum for details).

Tested on x86_64-pc-linux-gnu, committed on trunk

2012-11-06  Yannick Moy  <moy@adacore.com>

	* s-bignum.adb (Div_Rem): Fix another bug in step D3.


Index: s-bignum.adb
--- s-bignum.adb	(revision 193217)
+++ s-bignum.adb	(working copy)
@@ -859,6 +859,8 @@ 
             --  This had a bug not discovered till 1995, see Vol 2 errata:
             --  http://www-cs-faculty.stanford.edu/~uno/err2-2e.ps.gz. Under
             --  rare circumstances the expression in the test could overflow.
+            --  This version was further corrected in 2005, see Vol 2 errata:
+            --  http://www-cs-faculty.stanford.edu/~uno/all2-pre.ps.gz.
             --  The code below is the fixed version of this step.
             --  D3. [Calculate qhat.] Set qhat to (uj,uj+1)/v1 and rhat to
@@ -868,13 +870,13 @@ 
             qhat := temp / DD (v1);
             rhat := temp mod DD (v1);
-            --  D3 (continued). Now test if qhat = b or v2*qhat > (rhat,uj+2):
+            --  D3 (continued). Now test if qhat >= b or v2*qhat > (rhat,uj+2):
             --  if so, decrease qhat by 1, increase rhat by v1, and repeat this
             --  test if rhat < b. [The test on v2 determines at at high speed
             --  most of the cases in which the trial value qhat is one too
             --  large, and eliminates all cases where qhat is two too large.]
-            while qhat = b
+            while qhat >= b
               or else DD (v2) * qhat > LSD (rhat) & u (j + 2)
                qhat := qhat - 1;