X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Ftranslation.ma;h=0463cff55a25cf15797f17560fa496b5d7183495;hb=7845d9d0221d94418beecf3d7c3aed3efb2af7fc;hp=af54b87dd9f3fc881840c26bc900d917cfafa5ab;hpb=25be562c5436746df8d892449a9ff98755c37e9f;p=helm.git

diff --git a/helm/software/matita/library/freescale/translation.ma b/helm/software/matita/library/freescale/translation.ma
index af54b87dd..0463cff55 100644
--- a/helm/software/matita/library/freescale/translation.ma
+++ b/helm/software/matita/library/freescale/translation.ma
@@ -81,7 +81,11 @@ inductive MA_check : instr_mode → Type ≝
 | maINHA             : MA_check MODE_INHA
 | maINHX             : MA_check MODE_INHX
 | maINHH             : MA_check MODE_INHH
+| maINHX0ADD         : MA_check MODE_INHX0ADD
+| maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
+| maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
 | maIMM1             : byte8  → MA_check MODE_IMM1
+| maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
 | maIMM2             : word16 → MA_check MODE_IMM2
 | maDIR1             : byte8  → MA_check MODE_DIR1
 | maDIR2             : word16 → MA_check MODE_DIR2
@@ -125,8 +129,13 @@ definition args_picker ≝
   | maINHA   ⇒ nil ? 
   | maINHX   ⇒ nil ? 
   | maINHH   ⇒ nil ?
+  (* inherent address: legale se nessun operando/1 byte/1 word *)
+  | maINHX0ADD ⇒ nil ?
+  | maINHX1ADD b ⇒ [ TByte m b ]
+  | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]    
   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
   | maIMM1 b ⇒ [ TByte m b ]
+  | maIMM1EXT b ⇒ [ TByte m b ]
   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
   | maDIR1 b ⇒ [ TByte m b ]
   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]