Changeset 3263 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
May 10, 2013, 1:40:31 PM (7 years ago)
Author:
tranquil
Message:

moved callee saved saving and restoring to ERTL -> LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r3255 r3263  
    7373    (* ext_seq_labels ≝ *) (λ_.[])
    7474    (* has_tailcall ≝ *) false
    75     (* paramsT ≝ *) .
     75    (* paramsT ≝ *) unit.
    7676
    7777definition regs_from_move_dst : move_dst → list register ≝
     
    169169  (mk_universe … (p0 (p0 one)))
    170170  (mk_universe … one)
    171   it 4 0 0 (empty_map …) l1 in
     171  it it 0 0 0 (empty_map …) l1 in
    172172(* todo: args for main? *)
    173173let res ≝ add_graph … l1
Note: See TracChangeset for help on using the changeset viewer.