Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (7 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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.