From 415c1dae83891f217952941b6bae3e0c7b027c76 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 26 Mar 2018 09:51:48 +0200 Subject: Make the VM accumulator look like an OCaml block. We allocate an additional header so that the accumulator is not a naked pointer. Indeed, it is contained in accumulator blocks which are scanned by the GC as their tags is 0. --- kernel/byterun/coq_memory.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 9102af702..3cf5fc092 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -99,8 +99,12 @@ value init_coq_vm(value unit) /* ML */ /* Initialing the interpreter */ init_coq_interpreter(); - /* Some predefined pointer code */ - accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t)); + /* Some predefined pointer code. + * It is typically contained in accumlator blocks whose tag is 0 and thus + * scanned by the GC, so make it look like an OCaml block. */ + value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); + Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ + accumulate = (code_t) Val_hp(accu_block); *accumulate = VALINSTR(ACCUMULATE); /* Initialize GC */ -- cgit v1.2.3