From 9d8fcdd62607141814089bfa407d3dae63afa0b6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 29 Apr 2019 11:49:21 +0200
Subject: srsd

---
 mppa_k1c/Asmblockgen.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'mppa_k1c/Asmblockgen.v')

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 835b8a8c..49f6e4f9 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -641,11 +641,7 @@ Definition transl_op
       OK (Psrlil rd rs n ::i k)
   | Oshrxlimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (if Int.eq n Int.zero then Pmv rd rs ::i k else
-          Psrail RTMP rs (Int.repr 63) ::i
-          Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i
-          Paddl RTMP rs RTMP ::i
-          Psrail rd RTMP n ::i k)
+      OK (Psrxil rd rs n ::i k)
   | Omaddl, a1 :: a2 :: a3 :: nil =>
     assertion (mreg_eq a1 res);
       do r1 <- ireg_of a1;
-- 
cgit