Changeset 2956


Ignore:
Timestamp:
Mar 26, 2013, 4:31:36 PM (4 years ago)
Author:
tranquil
Message:

fixed LTL/LIN semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2837 r2956  
    5555  let carry ≝ other_bit (regs … st) in
    5656  return set_carry LTL_LIN_state carry st
    57 | LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge curr_id l;
     57| LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge curr_id l;
    5858                    let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
    5959                    let regs ≝ hwreg_store r addrl (regs … st) in
    6060                    return set_regs LTL_LIN_state regs st
    61 | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge curr_id l;
     61| HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge curr_id l;
    6262                    let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
    6363                    let regs ≝ hwreg_store r addrh (regs … st) in
Note: See TracChangeset for help on using the changeset viewer.