Changeset 2739 for src


Ignore:
Timestamp:
Feb 27, 2013, 4:37:31 PM (7 years ago)
Author:
sacerdot
Message:

The graph colouring algorithm takes in input also the function.

Location:
src/ERTLptr
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2700 r2739  
    426426(* colour registers *)
    427427let after ≝ analyse_liveness the_fixpoint globals int_fun in
    428 let coloured_graph ≝ build after in
     428let coloured_graph ≝ build … int_fun after in
    429429(* compute new stack size *)
    430430let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
  • src/ERTLptr/Interference.ma

    r2700 r2739  
    1919}.
    2020
    21 definition coloured_graph_computer ≝ ∀valuation. coloured_graph valuation.
     21definition coloured_graph_computer ≝
     22 ∀globals.
     23  joint_internal_function ERTLptr globals →
     24   ∀valuation.
     25    coloured_graph valuation.
Note: See TracChangeset for help on using the changeset viewer.