Changeset 2264 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jul 26, 2012, 12:38:42 AM (7 years ago)
Author:
sacerdot
Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2212 r2264  
    11901190  let s ≝
    11911191    match instr with
    1192     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
     1192    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s
    11931193    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    11941194    | Cost cst ⇒ s
    11951195    | Jmp jmp ⇒
    11961196       let s ≝ set_clock … s (\fst ticks + clock … s) in
    1197         set_program_counter … s (address_of_word_labels cm jmp)
     1197        set_program_counter … s (address_of_word_labels (\snd cm) jmp)
    11981198    | Call call ⇒
    11991199      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1200       let a ≝ address_of_word_labels cm call in
     1200      let a ≝ address_of_word_labels (\snd cm) call in
    12011201      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    12021202      let s ≝ set_8051_sfr … s SFR_SP new_sp in
Note: See TracChangeset for help on using the changeset viewer.