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 /vernac/comDefinition.ml | |
| 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 'vernac/comDefinition.ml')
0 files changed, 0 insertions, 0 deletions