diff options
| author | Michael Schmidt <github@mschmidt.me> | 2015-12-15 10:01:49 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2015-12-15 10:01:49 +0100 |
| commit | 00e3b7b59515c086fb92751c15d61b0352f9fde9 (patch) | |
| tree | ca4aa7fe1d11e1a10703f2c0e98bd31499b5b980 /powerpc/Machregs.v | |
| parent | 91029ac1749b8186c17c6cb14347066be8226434 (diff) | |
| download | compcert-kvx-00e3b7b59515c086fb92751c15d61b0352f9fde9.tar.gz compcert-kvx-00e3b7b59515c086fb92751c15d61b0352f9fde9.zip | |
bug 17752, add builtin64_set_spr and builtin64_get_spr for PowerPC
Diffstat (limited to 'powerpc/Machregs.v')
| -rw-r--r-- | powerpc/Machregs.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index b56812e5..7137bce2 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -163,7 +163,8 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin id sg => - if string_dec id "__builtin_atomic_exchange" then R10::nil + if string_dec id "__builtin64_set_spr" then R10::nil + else if string_dec id "__builtin_atomic_exchange" then R10::nil else if string_dec id "__builtin_atomic_compare_exchange" then R10::R11::nil else F13 :: nil | EF_vload _ => R11 :: nil |