diff options
| author | Michael Schmidt <github@mschmidt.me> | 2015-12-15 09:17:07 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2015-12-15 09:17:07 +0100 |
| commit | 91029ac1749b8186c17c6cb14347066be8226434 (patch) | |
| tree | c4c1670c20a2cc12dfa08402a91e04e85fe45f74 /powerpc/TargetPrinter.ml | |
| parent | 67fda21314a577d6ae2bc9a5abf6df329b8ba85a (diff) | |
| download | compcert-kvx-91029ac1749b8186c17c6cb14347066be8226434.tar.gz compcert-kvx-91029ac1749b8186c17c6cb14347066be8226434.zip | |
Bug 17752, add rldicr instruction for PowerPC
Diffstat (limited to 'powerpc/TargetPrinter.ml')
| -rw-r--r-- | powerpc/TargetPrinter.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 73cb12f5..24511887 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -647,6 +647,9 @@ module Target (System : SYSTEM):TARGET = | Prldicl(r1, r2, c1, c2) -> fprintf oc " rldicl %a, %a, %ld, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) + | Prldicr(r1, r2, c1, c2) -> + fprintf oc " rldicr %a, %a, %ld, %ld\n" + ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) | Prlwinm(r1, r2, c1, c2) -> let (mb, me) = rolm_mask (camlint_of_coqint c2) in fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" @@ -789,7 +792,7 @@ module Target (System : SYSTEM):TARGET = let nlo = Int64.to_int32 n and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo - + let print_literal32 oc (lbl, n) = fprintf oc "%a: .long 0x%lx\n" label lbl n |