aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--aarch64/Machregs.v2
-rw-r--r--aarch64/TargetPrinter.ml4
2 files changed, 3 insertions, 3 deletions
diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v
index 3d27f48f..bfe23e83 100644
--- a/aarch64/Machregs.v
+++ b/aarch64/Machregs.v
@@ -158,7 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
match ef with
| EF_memcpy sz al => R15 :: R17 :: R29 :: nil
| EF_inline_asm txt sg clob => destroyed_by_clobber clob
- | EF_profiling _ _ => R15 :: R17 :: nil
+ | EF_profiling _ _ => R15 :: R17 :: R29 :: nil
| _ => nil
end.
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index 9ec1d563..53959152 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -231,8 +231,8 @@ module Target (*: TARGET*) =
fprintf oc "%s:\n" lbl;
fprintf oc " ldaxr x17, [x15]\n";
fprintf oc " add x17, x17, 1\n";
- fprintf oc " stlxr w17, x17, [x15]\n";
- fprintf oc " cbnz w17, %s\n" lbl;
+ fprintf oc " stlxr w29, x17, [x15]\n";
+ fprintf oc " cbnz w29, %s\n" lbl;
fprintf oc "%s end profiling %a %d\n" comment
Profilingaux.pp_id id kind;;