diff options
Diffstat (limited to 'powerpc/Machregs.v')
| -rw-r--r-- | powerpc/Machregs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index e7c8758b..9967bbae 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -166,7 +166,7 @@ Definition destroyed_by_op (op: operation): list mreg := | Ofloatconst _ => R12 :: nil | Osingleconst _ => R12 :: nil | Olongconst _ => R12 :: nil - | Ointoffloat | Ointuoffloat => F13 :: nil + | Ointoffloat => F13 :: nil | Olongoffloat => F13 :: nil | Oaddlimm _ => R12 :: nil | Oandlimm _ => R12 :: nil @@ -232,7 +232,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list | EF_builtin id sg => if string_dec id "__builtin_atomic_exchange" then ((Some R3)::(Some R4)::(Some R5)::nil,nil) else if string_dec id "__builtin_sync_fetch_and_add" then ((Some R4)::(Some R5)::nil,(Some R3)::nil) - else if string_dec id "___builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil) + else if string_dec id "__builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil) else (nil, nil) | _ => (nil, nil) end. |