Changeset 2906


Ignore:
Timestamp:
Mar 19, 2013, 9:54:38 AM (4 years ago)
Author:
sacerdot
Message:

Bug fixed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2899 r2906  
    182182                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
    183183                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
    184                 let s ≝ set_8051_sfr … s' SFR_DPL bl in
    185                  set_8051_sfr … s' SFR_DPH bu
     184                let s'' ≝ set_8051_sfr … s' SFR_DPL bl in
     185                 set_8051_sfr … s'' SFR_DPH bu
    186186              | _ ⇒ λother: False. ⊥
    187187              ] (subaddressing_modein … addr)
     
    609609                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
    610610                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
    611                 let s ≝ set_8051_sfr … s' SFR_DPL bl in
    612                  set_8051_sfr … s' SFR_DPH bu
     611                let s'' ≝ set_8051_sfr … s' SFR_DPL bl in
     612                 set_8051_sfr … s'' SFR_DPH bu
    613613              | _ ⇒ λother: False. ⊥
    614614              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
Note: See TracChangeset for help on using the changeset viewer.