diff options
| author | Guillaume Melquiond | 2019-11-12 10:57:23 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2019-12-22 17:20:15 +0400 |
| commit | a028a97005b88a66a9d6dbaa4f0ade38859beffb (patch) | |
| tree | 96fe1ddb998dc0316a75247e1ca0d9d25535d0cc /kernel/byterun/coq_interp.c | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
Use the Alloc_small macro from the OCaml runtime rather than our own.
We cannot use caml_alloc_small because the macros Setup_for_gc and
Restore_after_gc are still relevant (and critical). This means defining
the CAML_INTERNALS macro, but it is a legit use and actually documented
in the OCaml manual.
This will help with forward compatibility with OCaml compilers, e.g.,
issue #10603. Unfortunately, it also means that we can no longer use #9914
to prevent memory corruption.
The old macro is still used for OCaml versions prior to 4.10, as the
upstream macro might process Ctrl+C when it is called.
Diffstat (limited to 'kernel/byterun/coq_interp.c')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 606cce0127..c30648197f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,17 +16,35 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <math.h> + +#define CAML_INTERNALS #include <caml/memory.h> #include <caml/signals.h> #include <caml/version.h> -#include <math.h> -#include "coq_gc.h" + #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" #include "coq_float64.h" +#if OCAML_VERSION < 41000 +#undef Alloc_small +#define Alloc_small(result, wosize, tag) do{ \ + young_ptr -= Bhsize_wosize (wosize); \ + if (young_ptr < young_limit){ \ + young_ptr += Bhsize_wosize (wosize); \ + Setup_for_gc; \ + minor_collection (); \ + Restore_after_gc; \ + young_ptr -= Bhsize_wosize (wosize); \ + } \ + Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \ + (result) = Val_hp (young_ptr); \ + }while(0) +#endif + #ifdef ARCH_SIXTYFOUR #include "coq_uint63_native.h" #else |