From 596a4a5251cc50f50bd6d25e36c81341bf65cfed Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire <Benjamin.Gregoire@inria.fr>
Date: Mon, 30 Mar 2015 10:47:12 +0200
Subject: fix code and bound for SWITCH instruction.

---
 kernel/byterun/coq_fix_code.c | 4 ++--
 kernel/byterun/coq_interp.c   | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index f1f9c9215..1be3e6511 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -150,8 +150,8 @@ value coq_tcode_of_code (value code, value size) {
       uint32_t i, sizes, const_size, block_size;
       COPY32(q,p); p++;
       sizes=*q++;
-      const_size = sizes & 0x7FFFFF;
-      block_size = sizes >> 23;
+      const_size = sizes & 0xFFFFFF;
+      block_size = sizes >> 24;
       sizes = const_size + block_size;
       for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
     } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index df71f4585..0ab9f89ff 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -791,12 +791,12 @@ value coq_interprete
       Instruct(SWITCH) {
 	uint32_t sizes = *pc++;
 	print_instr("SWITCH");
-	print_int(sizes & 0x7FFFFF);
+	print_int(sizes & 0xFFFFFF);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
 	  print_int(index);
-	  pc += pc[(sizes & 0xFFFFF) + index];
+	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
-- 
cgit v1.2.3