diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 17:46:58 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 17:46:58 +0000 |
| commit | 468f0c4407895557ca8089430f894a85f06afe97 (patch) | |
| tree | 76d4d5bb302da822797ccbbecd8f4cfd935bf938 /arm/Machregs.v | |
| parent | 600e5f3be65eeffc80d5c4cad800121fe521a1aa (diff) | |
| download | compcert-kvx-468f0c4407895557ca8089430f894a85f06afe97.tar.gz compcert-kvx-468f0c4407895557ca8089430f894a85f06afe97.zip | |
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
Diffstat (limited to 'arm/Machregs.v')
| -rw-r--r-- | arm/Machregs.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/arm/Machregs.v b/arm/Machregs.v index 4906eb0b..50535f0b 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 := |