From 989553966c7ba1a2cc23fd10fc2633dcb0f98648 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 24 Nov 2016 10:03:17 +0100 Subject: 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. --- kernel/byterun/coq_interp.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/byterun') 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; } -- cgit v1.2.3