From 58c7f5045c9cf1b64311fd7a168ed3b496666bb0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 21 Jun 2011 15:53:05 +0000 Subject: Recognition of rlwimi instruction (useful for bitfield assignment) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1676 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/PrintAsm.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'powerpc/PrintAsm.ml') diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 0c19932..eacf1dd 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -687,6 +687,11 @@ let print_instruction oc = function fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" ireg r1 ireg r2 (camlint_of_coqint c1) mb me comment (camlint_of_coqint c2) + | Prlwimi(r1, r2, c1, c2) -> + let (mb, me) = rolm_mask (camlint_of_coqint c2) in + fprintf oc " rlwimi %a, %a, %ld, %d, %d %s 0x%lx\n" + ireg r1 ireg r2 (camlint_of_coqint c1) mb me + comment (camlint_of_coqint c2) | Pslw(r1, r2, r3) -> fprintf oc " slw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psraw(r1, r2, r3) -> -- cgit v1.2.3