Changeset 3014 for src/LIN


Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (8 years ago)
Author:
tranquil
Message:

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

Location:
src/LIN
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2984 r3014  
    3737    let 〈x, region, data〉 ≝ x_size in
    3838      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat (size_init_data_list data)〉 in
    39   let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(globals_stacksize … p)〉 (prog_vars ?? p) in
     39      (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
     40  let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(S (globals_stacksize … p))〉 (prog_vars ?? p) in
    4041mk_ASM_universe ? (mk_universe … one)
    4142  (an_identifier … one (* dummy *))
     
    430431  ! main ← Identifier_of_ident … (prog_main … p) ;
    431432  ! u ← state_get … ;
    432   let start_sp : Z ≝ -(globals_stacksize … p) in
     433  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
     434  let start_sp : Z ≝ -(S (globals_stacksize … p)) in
    433435  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
    434436  let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in
  • src/LIN/joint_LTL_LIN.ma

    r2783 r3014  
    1111| SAVE_CARRY : ltl_lin_seq
    1212| RESTORE_CARRY : ltl_lin_seq
    13 | LOW_ADDRESS : Register → label → ltl_lin_seq
    14 | HIGH_ADDRESS : Register → label → ltl_lin_seq.
     13(* store low/high parts of label address in the accumulator *)
     14| LOW_ADDRESS : label → ltl_lin_seq
     15| HIGH_ADDRESS : label → ltl_lin_seq.
    1516
    1617definition ltl_lin_seq_labels ≝ λs.match s with
    17 [ LOW_ADDRESS _ lbl ⇒ [ lbl ]
    18 | HIGH_ADDRESS _ lbl ⇒ [ lbl ]
     18[ LOW_ADDRESS lbl ⇒ [ lbl ]
     19| HIGH_ADDRESS lbl ⇒ [ lbl ]
    1920| _ ⇒ [ ]
    2021].
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2969 r3014  
    5252  let carry ≝ other_bit (regs … st) in
    5353  return set_carry LTL_LIN_state carry st
    54 | LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge curr_id l;
     54| LOW_ADDRESS l ⇒  ! pc_lab ← gen_pc_from_label … ge curr_id l;
    5555                    let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
    56                     let regs ≝ hwreg_store r addrl (regs … st) in
     56                    let regs ≝ hwreg_store RegisterA addrl (regs … st) in
    5757                    return set_regs LTL_LIN_state regs st
    58 | HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge curr_id l;
     58| HIGH_ADDRESS l ⇒ ! pc_lab ← gen_pc_from_label … ge curr_id l;
    5959                    let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
    60                     let regs ≝ hwreg_store r addrh (regs … st) in
     60                    let regs ≝ hwreg_store RegisterA addrh (regs … st) in
    6161                    return set_regs LTL_LIN_state regs st
    6262].
Note: See TracChangeset for help on using the changeset viewer.