diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-24 10:03:17 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-24 10:03:17 +0100 |
| commit | 989553966c7ba1a2cc23fd10fc2633dcb0f98648 (patch) | |
| tree | fa19d67b2fcee5b987fa1f7d2b582b9ca1df17f1 /kernel/byterun | |
| parent | a277da239514ad3bcabc7933a14cfcdc46f272e5 (diff) | |
Fix incorrect long multiplication in the VM.
If the result had its 30th bit set, then all the high part of the result
on a 64-bit architecture would end up being set, thus breaking subsequent
computations.
This patch also fixes the incorrectly parenthesized definition of
uint32_of_value, which by luck was never misused.
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 792a311fc..47df22807 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,7 +23,7 @@ #include "coq_values.h" /* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) (((uint32_t)val >> 1)) +#define uint32_of_value(val) ((uint32_t)(val) >> 1) #define value_of_uint32(i) ((value)(((uint32_t)(i) << 1) | 1)) #define UI64_of_uint32(lo) ((uint64_t)(lo)) #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) @@ -1206,7 +1206,7 @@ value coq_interprete Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ /*unsigned shift*/ Field(accu, 0) = (value)((p >> 31)|1) ; /*higher part*/ - Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/ + Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/ } Next; } |