diff options
| author | Pierre Roux | 2019-04-05 12:37:03 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-30 08:22:19 +0200 |
| commit | 46896e9442e74cb78ad7396054cee76564f78ec3 (patch) | |
| tree | 9403ad49f9acdad4c7ba13ecc77e6fce6a5ca015 /kernel | |
| parent | d1905fbcde5905de640657a820e531929e23dd8a (diff) | |
[vm] ARM registers
Backport
https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928
from OCaml VM
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1925ef5932..9742768c5d 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -148,8 +148,9 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("a4") #define ACCU_REG asm("d7") #endif -#if defined(__arm__) && !defined(__thumb2__) -#define PC_REG asm("r9") +/* OCaml PR#4953: these specific registers not available in Thumb mode */ +#if defined(__arm__) && !defined(__thumb__) +#define PC_REG asm("r6") #define SP_REG asm("r8") #define ACCU_REG asm("r7") #endif |