diff options
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 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 := |