Changeset 2705 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Feb 22, 2013, 5:56:31 PM (7 years ago)
Author:
sacerdot
Message:

More progress in ASM towards implementing the new pseudoinstructions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2651 r2705  
    183183        [ ([[true;false;true;false;false;false;true;true]]) ]
    184184      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     185  | JMP adptr ⇒
     186     [ ([[false;true;true;true;false;false;true;true]]) ]
    185187  | MOV addrs ⇒
    186188     match addrs with
     
    395397          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    396398      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    397   | JMP adptr ⇒
    398      [ ([[false;true;true;true;false;false;true;true]]) ]
    399399  | LCALL addr ⇒
    400400     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     
    509509  | RET ⇒ [ RET ? ]
    510510  | RETI ⇒ [ RETI ? ]
    511   | NOP ⇒ [ RealInstruction (NOP ?) ]
     511  | NOP ⇒ [ NOP ? ]
     512  | JMP arg ⇒ [ RealInstruction (JMP ? arg) ]
    512513  ].
    513514
     
    557558        let address ≝ ADDR16 lookup_address in
    558559        [ LJMP address ]
     560  | Jnz acc tgt1 tgt2 ⇒
     561     
    559562  ].
    560563  %
Note: See TracChangeset for help on using the changeset viewer.