diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-15 09:03:23 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-15 09:03:23 +0000 |
commit | 88e55a6729b58cfc2ce32ed526dfd3c9cdf4feef (patch) | |
tree | 0c1ea9073439e16173f8ba53cc68650dd83a6f4c /powerpc | |
parent | c4877832826fa26aea9c236f16bdc2de16c98150 (diff) | |
download | compcert-kvx-88e55a6729b58cfc2ce32ed526dfd3c9cdf4feef.tar.gz compcert-kvx-88e55a6729b58cfc2ce32ed526dfd3c9cdf4feef.zip |
Cosmetic cleanups.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1793 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/PrintAsm.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index d79735a6..1ce95f2b 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -375,7 +375,7 @@ let print_builtin_memcpy oc sz al args = (* Handling of volatile reads and writes *) -let print_builtin_vload_shared oc chunk base offset res = +let print_builtin_vload_common oc chunk base offset res = match chunk, res with | Mint8unsigned, IR res -> fprintf oc " lbz %a, %a(%a)\n" ireg res constant offset ireg base @@ -399,7 +399,7 @@ let print_builtin_vload oc chunk args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; begin match args with | [IR addr] -> - print_builtin_vload_shared oc chunk addr (Cint Integers.Int.zero) res + print_builtin_vload_common oc chunk addr (Cint Integers.Int.zero) res | _ -> assert false end; @@ -409,10 +409,10 @@ let print_builtin_vload_global oc chunk id ofs args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; fprintf oc " addis %a, %a, %a\n" ireg GPR11 ireg_or_zero GPR0 constant (Csymbol_high(id, ofs)); - print_builtin_vload_shared oc chunk GPR11 (Csymbol_low(id, ofs)) res; + print_builtin_vload_common oc chunk GPR11 (Csymbol_low(id, ofs)) res; fprintf oc "%s end builtin __builtin_volatile_read\n" comment -let print_builtin_vstore_shared oc chunk base offset src = +let print_builtin_vstore_common oc chunk base offset src = match chunk, src with | (Mint8signed | Mint8unsigned), IR src -> fprintf oc " stb %a, %a(%a)\n" ireg src ireg base constant offset @@ -432,7 +432,7 @@ let print_builtin_vstore oc chunk args = fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; begin match args with | [IR addr; src] -> - print_builtin_vstore_shared oc chunk addr (Cint Integers.Int.zero) src + print_builtin_vstore_common oc chunk addr (Cint Integers.Int.zero) src | _ -> assert false end; @@ -445,7 +445,7 @@ let print_builtin_vstore_global oc chunk id ofs args = let tmp = if src = IR GPR11 then GPR12 else GPR11 in fprintf oc " addis %a, %a, %a\n" ireg tmp ireg_or_zero GPR0 constant (Csymbol_high(id, ofs)); - print_builtin_vstore_shared oc chunk tmp (Csymbol_low(id, ofs)) src + print_builtin_vstore_common oc chunk tmp (Csymbol_low(id, ofs)) src | _ -> assert false end; |