diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-07-01 14:13:25 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-07-01 14:13:25 +0200 |
| commit | c94405f67ca18be997974f88ff91c072d8a5c0cb (patch) | |
| tree | 595ad6a85154f085b2622be979ffaea15cd4b11c /powerpc | |
| parent | fde847543e8169082db0138a9713a8c0ab0cc167 (diff) | |
| download | compcert-kvx-c94405f67ca18be997974f88ff91c072d8a5c0cb.tar.gz compcert-kvx-c94405f67ca18be997974f88ff91c072d8a5c0cb.zip | |
Fix typo in name of builtin function.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Machregs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index e7c8758b..07622a0e 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -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. |