Changeset 3028


Ignore:
Timestamp:
Mar 29, 2013, 9:42:11 AM (4 years ago)
Author:
sacerdot
Message:

Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should have
been 0x82 and 0x83!

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2999 r3028  
    22
    33definition ASMRegisterRets: list [[ acc_a; direct; registr ]] ≝
    4  [ DIRECT (bitvector_of_nat 8 82);       (* DPL *)
    5    DIRECT (bitvector_of_nat 8 83);       (* DPH *)
     4 [ DIRECT (bitvector_of_nat 8 130);       (* DPL *)
     5   DIRECT (bitvector_of_nat 8 131);       (* DPH *)
    66   REGISTER [[ false; false; false ]];   (* Register00 *)
    77   REGISTER [[ false; false; true ]] ].  (* Register01 *)
  • src/LIN/LINToASM.ma

    r3023 r3028  
    123123    | RegisterA ⇒ ACC_A
    124124    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    125     | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
    126     | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
     125    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 130)
     126    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 131)
    127127    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
    128128    ]. @I qed.
Note: See TracChangeset for help on using the changeset viewer.