aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-24 10:03:17 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-24 10:03:17 +0100
commit989553966c7ba1a2cc23fd10fc2633dcb0f98648 (patch)
treefa19d67b2fcee5b987fa1f7d2b582b9ca1df17f1
parenta277da239514ad3bcabc7933a14cfcdc46f272e5 (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.
-rw-r--r--kernel/byterun/coq_interp.c4
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;
}