Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 4 insertions, 5 deletions

diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v
index 8db871e..5eaa81e 100644
--- a/backend/CleanupLabels.v
+++ b/backend/CleanupLabels.v
@@ -16,15 +16,15 @@
   control-flow graph.  Many of these labels are never branched to,
   which can complicate further optimizations over linearized code.
   (There are no such optimizations yet.)  In preparation for these
-  further optimizations, and to make the generated LTLin code 
+  further optimizations, and to make the generated Linear code 
   better-looking, the present pass removes labels that cannot be
   branched to. *)
 
-Require Import Coqlib.
-Require Import Ordered.
 Require Import FSets.
 Require FSetAVL.
-Require Import LTLin.
+Require Import Coqlib.
+Require Import Ordered.
+Require Import Linear.
 
 Module Labelset := FSetAVL.Make(OrderedPositive).
 
@@ -63,7 +63,6 @@ Definition cleanup_labels (c: code) :=
 Definition transf_function (f: function) : function :=
   mkfunction
      (fn_sig f)
-     (fn_params f)
      (fn_stacksize f)
      (cleanup_labels (fn_code f)).