From 151b4d87bafdf2b89e6d25c02ac63cd6a1d484c9 Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Tue, 15 May 2007 08:06:37 +0000
Subject: corrections bug dans l'implem de int31

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9822 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 .depend.camlp4              | 2 +-
 kernel/byterun/coq_interp.c | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.depend.camlp4 b/.depend.camlp4
index cd93995630..482cc87865 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -10,7 +10,7 @@ contrib/romega/g_romega.ml: parsing/grammar.cma
 contrib/ring/g_quote.ml: parsing/grammar.cma
 contrib/ring/g_ring.ml: parsing/grammar.cma
 contrib/dp/g_dp.ml: parsing/grammar.cma
-contrib/setoid_ring/newring.ml: parsing/grammar.cma
+contrib/setoid_ring/newring.ml: 
 contrib/field/field.ml: parsing/grammar.cma
 contrib/fourier/g_fourier.ml: parsing/grammar.cma
 contrib/extraction/g_extraction.ml: parsing/grammar.cma
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index c3072dc726..e7eb1bc8d7 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -30,8 +30,8 @@
 
 /* spiwack: I append here a few macros for value/number manipulation */
 #define uint32_of_value(val) (((uint32)val >> 1))
-#define value_of_uint32(i)   ((value)(((uint32)i << 1) | 1))
-#define UI64_of_uint32(i)  ((uint64)I64_literal(0,i))
+#define value_of_uint32(i)   ((value)(((uint32)(i) << 1) | 1))
+#define UI64_of_uint32(lo)  ((uint64)(I64_literal(0,(uint32)(lo))))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
 /* /spiwack */
 
@@ -1234,7 +1234,7 @@ value coq_interprete
         /* *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 | ((*sp++) >> (31-shiftby)))|1);
+        accu = (value)((accu | (((uint32)(*sp++)) >> (31-shiftby)))|1);
         Next;
       }
 
-- 
cgit v1.2.3