patch for C code of addmuldiv31

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10593 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 0 deletions

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;
       }