1 files changed, 14 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index b00e4e89..6af18178 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -772,6 +772,20 @@ Definition transl_op
            OK (Pcmoveu bt r0 rS r1 ::i k)
        end)
 
+  | Oextfz stop start, a1 :: nil =>
+    assertion ((Z.leb start stop)
+                 && (Z.geb start Z.zero)
+                 && (Z.ltb stop Int.zwordsize));
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pextfz stop start rd rs ::i k)
+
+  | Oextfs stop start, a1 :: nil =>
+    assertion ((Z.leb start stop)
+                 && (Z.geb start Z.zero)
+                 && (Z.ltb stop Int.zwordsize));
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pextfs stop start rd rs ::i k)
+    
   | _, _ =>
       Error(msg "Asmgenblock.transl_op")
   end.