From 468f0c4407895557ca8089430f894a85f06afe97 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 17:46:58 +0000 Subject: Add __builtin_bswap16 and __builtin_bswap32 to all ports. Remove __builtin_{read,write}_reversed from IA32 and ARM ports. Machregs: tighten destroyed_by_builtin Packedstructs: use bswap if read/write-reversed not available. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2208 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Machregs.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'arm/Machregs.v') diff --git a/arm/Machregs.v b/arm/Machregs.v index 4906eb0..50535f0 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -104,7 +104,9 @@ 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 - | _ => R12 :: F6 :: nil + | EF_vstore Mfloat32 => F6 :: nil + | EF_vstore_global Mfloat32 _ _ => F6 :: nil + | _ => nil end. Definition destroyed_at_function_entry: list mreg := -- cgit v1.2.3