Changeset 3060
- Timestamp:
- Apr 2, 2013, 11:11:31 AM (8 years ago)
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/interpret.ml
r3043 r3060 1954 1954 (Nat.S Nat.O))))))))) big_acc dptr 1955 1955 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)) __ 1962 1957 1963 1958 (** val execute_1_preinstruction_ok' : -
src/ASM/Interpret.ma
r3039 r3060 190 190 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 191 191 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 195 194 | NOP ⇒ λinstr_refl. 196 195 let s ≝ add_ticks1 s in
Note: See TracChangeset
for help on using the changeset viewer.