Changeset 1729 for src/ERTL/liveness.ma


Ignore:
Timestamp:
Feb 23, 2012, 2:29:57 PM (8 years ago)
Author:
sacerdot
Message:

Comment left from SVN merge removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1463 r1729  
    152152    | PUSH r ⇒ lattice_psingleton r
    153153    | MOVE pair_reg ⇒
    154       (* only second reg in paidefinition liveafter ≝
    155   λglobals: list ident.
    156   λint_fun: ertl_internal_function globals.
    157   λlivebefore: label → ?.
    158   λlabel.
    159   λliveafter: valuation.
    160   match lookup … (joint_if_code … int_fun) label with
    161   [ None      ⇒ ?
    162   | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
    163       lattice_join (livebefore successor liveafter) accu)
    164       (statement_successors globals stmt) lattice_bottom
    165   ].
    166   cases not_implemented (* XXX *)
    167 qed.r relevant *)
    168154      let r2 ≝ \snd pair_reg in
    169155      match r2 with
Note: See TracChangeset for help on using the changeset viewer.