Changeset 3060

Timestamp:

Apr 2, 2013, 11:11:31 AM (7 years ago)

Author:

sacerdot

Message:

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

Files:

• extracted/interpret.ml (modified) (1 diff)
• src/ASM/Interpret.ma (modified) (1 diff)

extracted/interpret.ml

@@ -1954 +1954 @@
              (Nat.S Nat.O))))))))) big_acc dptr
        in
-       let new_pc =
-         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-           Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
-       in
-       Status.set_program_counter cm s0 new_pc)) __
+       Status.set_program_counter cm s0 jmp_addr)) __
 
 (** val execute_1_preinstruction_ok' :

src/ASM/Interpret.ma

@@ -190 +190 @@
           let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
           let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
-          let jmp_addr ≝ add … big_acc dptr in
-          let new_pc : Word ≝ add … (program_counter … s) jmp_addr in (* JHM: type annotation *)
-            set_program_counter … s new_pc 
+          let jmp_addr : Word ≝ add … big_acc dptr in
+            set_program_counter … s jmp_addr 
         | NOP ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in