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.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].
Note: See TracChangeset for help on using the changeset viewer.