From 91029ac1749b8186c17c6cb14347066be8226434 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Tue, 15 Dec 2015 09:17:07 +0100 Subject: Bug 17752, add rldicr instruction for PowerPC --- powerpc/TargetPrinter.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'powerpc/TargetPrinter.ml') 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 -- cgit