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 --- kernel/byterun/coq_interp.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index c3072dc72..e7eb1bc8d 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