diff options
| author | Pierre Roux | 2019-04-04 11:07:14 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-30 08:22:19 +0200 |
| commit | d2bbd834841ba3c8b2b482a02489bd4fac19f0fb (patch) | |
| tree | efdfff3fd4088174ee8edaf3b557dd68dac7d81b | |
| parent | fcba5e87be13bc5a5374fe274476cd4d5c45f058 (diff) | |
[vm] x86_64 registers
Backport
https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376
from OCaml VM
| -rw-r--r-- | kernel/byterun/coq_interp.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 2293ae9dfd..e838519fe4 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -159,6 +159,11 @@ if (sp - num_args < coq_stack_threshold) { \ #define ACCU_REG asm("38") #define JUMPTBL_BASE_REG asm("39") #endif +#ifdef __x86_64__ +#define PC_REG asm("%r15") +#define SP_REG asm("%r14") +#define ACCU_REG asm("%r13") +#endif #endif #define CheckInt1() do{ \ |