diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-26 09:51:48 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-30 09:44:24 +0200 |
commit | 415c1dae83891f217952941b6bae3e0c7b027c76 (patch) | |
tree | ccd040387eeb0ca1066d2c6a3c2aa12ad56ad4c4 | |
parent | 74f6c8c40942d57ea66d9f28bd15309ce59438b6 (diff) |
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.
-rw-r--r-- | kernel/byterun/coq_memory.c | 8 |
1 files changed, 6 insertions, 2 deletions
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 */ |