Changeset 3060


Ignore:
Timestamp:
Apr 2, 2013, 11:11:31 AM (4 years ago)
Author:
sacerdot
Message:

Bug fixed in the semantics of JMP.
The bug was due to a bug in the datasheets!

Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret.ml

    r3043 r3060  
    19541954             (Nat.S Nat.O))))))))) big_acc dptr
    19551955       in
    1956        let new_pc =
    1957          Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1958            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1959            Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
    1960        in
    1961        Status.set_program_counter cm s0 new_pc)) __
     1956       Status.set_program_counter cm s0 jmp_addr)) __
    19621957
    19631958(** val execute_1_preinstruction_ok' :
  • src/ASM/Interpret.ma

    r3039 r3060  
    190190          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    191191          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    192           let jmp_addr ≝ add … big_acc dptr in
    193           let new_pc : Word ≝ add … (program_counter … s) jmp_addr in (* JHM: type annotation *)
    194             set_program_counter … s new_pc
     192          let jmp_addr : Word ≝ add … big_acc dptr in
     193            set_program_counter … s jmp_addr
    195194        | NOP ⇒ λinstr_refl.
    196195           let s ≝ add_ticks1 s in
Note: See TracChangeset for help on using the changeset viewer.