From ff9f3714fcbaef1b2ddea3ba3ddde42c5d38014c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Jul 2012 21:07:20 +0000
Subject: Fixing unchecked overflow in sub_mult used for euclidian division
 over unbounded integers (thanks to L. Théry for pointing out the problem).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15637 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/bigint.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/lib/bigint.ml b/lib/bigint.ml
index ed854d7aa1..050046ec76 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -175,14 +175,18 @@ let rec can_divide k m d i =
   (m.(k+i) > d.(i)) or
   (m.(k+i) = d.(i) && can_divide k m d (i+1))
 
-(* computes m - d * q * base^(|m|-k) in-place on positive numbers *)
+(* computes m - d * q * base^(|m|-|d|-k) in-place on positive numbers *)
 let sub_mult m d q k =
   if q <> 0 then
   for i = Array.length d - 1 downto 0 do
     let v = d.(i) * q in
     m.(k+i) <- m.(k+i) - v mod base;
     if m.(k+i) < 0 then (m.(k+i) <- m.(k+i) + base; m.(k+i-1) <- m.(k+i-1) -1);
-    if v >= base then m.(k+i-1) <- m.(k+i-1) - v / base;
+    if v >= base then begin
+      m.(k+i-1) <- m.(k+i-1) - v / base;
+      if m.(k+i-1) < 0 then
+        (m.(k+i-1) <- m.(k+i-1) + base; m.(k+i-2) <- m.(k+i-2) -1)
+    end
   done
 
 let euclid m d =
-- 
cgit v1.2.3