Changeset 1494 for src/ASM


Ignore:
Timestamp:
Nov 7, 2011, 10:56:13 AM (8 years ago)
Author:
mulligan
Message:

changes to get everything compiling again

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1037 r1494  
    678678      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    679679      let preamble ≝ \fst (code_memory ? s) in
    680       let data_labels ≝ construct_datalabels preamble in
     680      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
    681681        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels (zero ?)))) dptr
    682682    ]
  • src/ASM/WellLabeled.ma

    r1493 r1494  
    1717definition well_labelled_p ≝
    1818  ∀pc: Word.
    19   ∀dptr: Word.
    2019  ∀acc_a: Byte.
    2120  ∀function_locations: list Word.
     
    7675        | _ ⇒ λabsurd. ⊥
    7776        ] (subaddressing_modein … sjmp)
    78       | JMP jmp ⇒
    79         let big_acc_a ≝ (zero 8) @@ acc_a in
    80         let 〈carry, jmp_addr〉 ≝ half_add … big_acc_a dptr in
    81         let 〈carry, new_pc〉 ≝ half_add … pc jmp_addr in
    82           match lookup_opt … new_pc cost_labels with
    83           [ None ⇒ False
    84           | _    ⇒ True
    85           ]
     77      | JMP jmp ⇒ True (* XXX: check is dynamic, as we can only jump to functions *)
    8678      | MOVC _ _ ⇒ True
    8779      | RealInstruction instruction ⇒
Note: See TracChangeset for help on using the changeset viewer.