aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-26 10:02:54 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-30 09:44:24 +0200
commit5c0b2171844cee7a5344c535c2793e362d925e0c (patch)
tree07d05457fcbd0f2d7013f87d5379464a0b711652 /kernel/byterun
parent415c1dae83891f217952941b6bae3e0c7b027c76 (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.c5
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 */