From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: Merge of the newmem and newextcalls branches: - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/PrintAsm.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'powerpc/PrintAsm.ml') diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 10170f9e..a1e5afe3 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -288,7 +288,8 @@ let print_instruction oc labels = function fprintf oc " extsb %a, %a\n" ireg r1 ireg r2 | Pextsh(r1, r2) -> fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 - | Pfreeframe ofs -> + | Pfreeframe(lo, hi, ofs) -> + (* Note: could also do an add on GPR1 using lo and hi *) fprintf oc " lwz %a, %ld(%a)\n" ireg GPR1 (camlint_of_coqint ofs) ireg GPR1 | Pfabs(r1, r2) -> fprintf oc " fabs %a, %a\n" freg r1 freg r2 -- cgit