diff options
| author |  bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-15 08:06:37 +0000 |
|---|---|---|
| committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-15 08:06:37 +0000 |
| commit | 151b4d87bafdf2b89e6d25c02ac63cd6a1d484c9 (patch) | |
| tree | bc9908c528fc91a2dfe4490e8fb1f95d838fd35a | |
| parent | 2dbe106c09b60690b87e31e58d505b1f4e05b57f (diff) | |
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
| -rw-r--r-- | .depend.camlp4 | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/.depend.camlp4 b/.depend.camlp4 index cd9399563..482cc8786 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 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; } |