From 1ea7fbeaab845a14b4df803b791e0fc81f61ff9d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 21 Aug 2014 14:09:09 +0000 Subject: Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Machregs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm/Machregs.v') diff --git a/arm/Machregs.v b/arm/Machregs.v index 791ccbb6..f373b434 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -97,7 +97,7 @@ Definition destroyed_by_jumptable: list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with - | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil + | EF_memcpy sz al => if zle sz 32 then F7 :: nil else R2 :: R3 :: R12 :: nil | _ => nil end. -- cgit