Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (8 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness_paolo.ma

    r2182 r2208  
    9292definition ret_regs ≝ set_from_list … RegisterRets.
    9393
    94 definition rl_arg : rtl_argument → register_lattice ≝
     94definition rl_arg : psd_argument → register_lattice ≝
    9595  λarg.match arg with
    9696  [ Imm _ ⇒ rl_bottom
     
    124124        let r2 ≝ \snd pair_reg in
    125125        match r2 with
    126         [ REG p ⇒
     126        [ Reg p ⇒
    127127          match p with
    128128          [ PSD r ⇒ rl_psingleton r
    129129          | HDW r ⇒ rl_hsingleton r
    130130          ]
    131         | INT _ ⇒ rl_bottom
     131        | Imm _ ⇒ rl_bottom
    132132        ]
    133133      | extension_seq ext ⇒
     
    236236definition livebefore ≝
    237237  λglobals: list ident.
    238   λint_fun: ertl_internal_function globals.
     238  λint_fun: joint_internal_function globals ertl_params.
    239239  λlabel.
    240240  λliveafter: valuation register_lattice.
     
    246246definition liveafter ≝
    247247   λglobals: list ident.
    248   λint_fun: ertl_internal_function globals.
     248  λint_fun: joint_internal_function globals ertl_params.
    249249  λlabel.
    250250  λliveafter: valuation register_lattice.
Note: See TracChangeset for help on using the changeset viewer.