1 files changed, 1 insertions, 0 deletions
diff --git a/arm/Machregs.v b/arm/Machregs.v
index ae0ff6bf..1ec8f0a1 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -153,6 +153,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al => R2 :: R3 :: R12 :: F7 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
+  | EF_profiling _ _ => R2 :: R3 :: R12 :: nil
   | _ => nil
   end.