Changeset 3028 for src/ASM


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

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

File:
1 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 *)
Note: See TracChangeset for help on using the changeset viewer.