From 00894adf6fc11f4336a3ece0c347676bbf0b4c11 Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire <Benjamin.Gregoire@inria.fr>
Date: Thu, 26 Mar 2015 19:00:00 +0100
Subject: allows the vm to deal with inductive type with 8388607 constant
 constructors and 8388851 non-constant constructor.

---
 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 52dc49bf8..f1f9c9215 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 & 0xFFFF;
-      block_size = sizes >> 16;
+      const_size = sizes & 0x7FFFFF;
+      block_size = sizes >> 23;
       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 d74affdea..df71f4585 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 & 0xFFFF);
+	print_int(sizes & 0x7FFFFF);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
 	  print_int(index);
-	  pc += pc[(sizes & 0xFFFF) + index];
+	  pc += pc[(sizes & 0xFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
-- 
cgit v1.2.3