Changeset 2739 for src

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:

• ERTLptrToLTL.ma (modified) (1 diff)
• Interference.ma (modified) (1 diff)

src/ERTLptr/ERTLptrToLTL.ma

@@ -426 +426 @@
 (* colour registers *)
 let after ≝ analyse_liveness the_fixpoint globals int_fun in
-let coloured_graph ≝ build after in
+let coloured_graph ≝ build … int_fun after in
 (* compute new stack size *)
 let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in

src/ERTLptr/Interference.ma

@@ -19 +19 @@
 }.
 
-definition coloured_graph_computer ≝ ∀valuation. coloured_graph valuation.
+definition coloured_graph_computer ≝
+ ∀globals.
+  joint_internal_function ERTLptr globals →
+   ∀valuation.
+    coloured_graph valuation.