diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-26 10:02:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-30 09:44:24 +0200 |
| commit | 5c0b2171844cee7a5344c535c2793e362d925e0c (patch) | |
| tree | 07d05457fcbd0f2d7013f87d5379464a0b711652 /kernel/byterun | |
| parent | 415c1dae83891f217952941b6bae3e0c7b027c76 (diff) | |
Adapt the VM GC hook to handle the no-naked-pointers option flag.
The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers
to C-allocated strings standing for VM bytecode. If the the no-naked-pointers
option is set, we perform the check that a stack value lives on the OCaml heap
ourselves.
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_memory.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 3cf5fc092..542a05fd2 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -11,6 +11,7 @@ #include <stdio.h> #include <string.h> #include <caml/alloc.h> +#include <caml/address_class.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -61,6 +62,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { +#ifdef NO_NAKED_POINTERS + /* The VM stack may contain C-allocated bytecode */ + if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; +#endif (*action) (*i, i); }; /* Hook */ |