From 7de4db13aee7d2d59125a7ac13ed073ec108c897 Mon Sep 17 00:00:00 2001
From: thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 27 Feb 2008 14:17:10 +0000
Subject: patch for C code of  addmuldiv31

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10593 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/byterun/coq_interp.c | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0dd3b653a..a2ece57c4 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1238,10 +1238,21 @@ value coq_interprete
         /* higher level shift (does shifts and cycles and such) */
         uint32 shiftby;
         shiftby = uint32_of_value(accu);
+        if (shiftby > 31) {
+          if (shiftby < 62) {
+            *sp++;
+	    accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1);
+          }
+          else {
+            accu = (value)(1);
+          }
+	}
+        else{
         /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
         accu = (value)(((*sp++)^1) << shiftby);
         /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
         accu = (value)((accu | (((uint32)(*sp++)) >> (31-shiftby)))|1);
+	}
         Next;
       }
 
-- 
cgit v1.2.3