Merge branch 'master' of file:///common/repositories/git/tools/compcert

2 files changed, 14 insertions, 8 deletions

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index b50065f7..ca166fd1 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -507,16 +507,22 @@ let expand_builtin_inline name args res =
       raise (Error "the first argument of __builtin_set_spr must be a constant")
   (* Special registers in 32bit hybrid mode *)
   | "__builtin_get_spr64", [BA_int n], BR_splitlong(BR(IR rh), BR(IR rl)) ->
-      emit (Pmfspr(rl, n));
-      emit (Prldicl(rh, rl, _32, _32));
-      emit (Prldicl(rl, rl, _0, _32))
+      if Archi.ppc64 then begin
+        emit (Pmfspr(rl, n));
+        emit (Prldicl(rh, rl, _32, _32));
+        emit (Prldicl(rl, rl, _0, _32))
+      end else
+        raise (Error "__builtin_get_spr64 is only supported for PPC64 targets")
   | "__builtin_get_spr64", _, _ ->
       raise (Error "the argument of __builtin_get_spr64 must be a constant")
   | "__builtin_set_spr64", [BA_int n; BA_splitlong(BA(IR ah), BA(IR al))], _ ->
-    emit (Prldicr(GPR10, ah, _32, _31));
-    emit (Prldicl(al, al, _0, _32));
-    emit (Pori(GPR10, al, Cint _0));
-    emit (Pmtspr(n, GPR10))
+      if Archi.ppc64 then begin
+        emit (Prldicr(GPR10, ah, _32, _31));
+        emit (Prldicl(al, al, _0, _32));
+        emit (Por(GPR10, GPR10, al));
+        emit (Pmtspr(n, GPR10))
+      end else
+        raise (Error "__builtin_set_spr64 is only supported for PPC64 targets")
   | "__builtin_set_spr64", _, _ ->
       raise (Error "the first argument of __builtin_set_spr64 must be a constant")
   (* Move registers *)
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3f12a829..3d183972 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -648,7 +648,7 @@ module Target (System : SYSTEM):TARGET =
           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"
+          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