BROKEN - works for x86, not for k1 anymore

4 files changed, 7 insertions, 16 deletions

diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 0f666a65..f5c76925 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -26,9 +26,7 @@ let emit i = current_code := i :: !current_code
 
 (* Generation of fresh labels *)
 
-(** dummy_funtion is now defined in Asm.v *)
-(* let dummy_function = { fn_code = []; fn_sig = signature_main } *)
-
+let dummy_function = { fn_code = []; fn_sig = signature_main }
 let current_function = ref dummy_function
 let next_label = ref (None: label option)
 
@@ -122,7 +120,7 @@ let expand_debug id sp preg simple l =
         begin
           match kind with
           | 1->
-              emit i; aux lbl scopes rest
+              emit i;aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
@@ -163,7 +161,7 @@ let expand_debug id sp preg simple l =
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
   let rec move_debug acc bcc = function
-    | (Pbuiltin(EF_debug (kind,_,_),_,_)) as i::rest ->
+    | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest ->
         let kind = (P.to_int kind) in
         if kind = 1 then
           move_debug acc (i::bcc) rest (* Do not move debug line *)
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 3e25c79b..70c4323c 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -39,14 +39,12 @@ Proof.
   unfold ireg_of; intros. destruct (preg_of r); inv H; auto.
 Qed.
 
-(* FIXME - Replaced FR by IR for MPPA *)
 Lemma freg_of_eq:
-  forall r r', freg_of r = OK r' -> preg_of r = IR r'.
+  forall r r', freg_of r = OK r' -> preg_of r = FR r'.
 Proof.
   unfold freg_of; intros. destruct (preg_of r); inv H; auto.
 Qed.
 
-
 Lemma preg_of_injective:
   forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
 Proof.
@@ -756,7 +754,7 @@ Lemma tail_nolabel_cons:
 Proof.
   intros. destruct H0. split.
   constructor; auto.
-  intros. simpl. rewrite <- H1. destruct i; destruct i; reflexivity || contradiction.
+  intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
 Qed.
 
 Hint Resolve tail_nolabel_refl: labels.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 55d86448..fc163719 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -324,7 +324,7 @@ Local Opaque mreg_type.
     apply wt_setreg; auto. eapply Val.has_subtype; eauto.
     change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
     red; intros; subst op. simpl in ISMOVE.
-    destruct args; try discriminate. destruct args; discriminate;
+    destruct args; try discriminate. destruct args; discriminate.
     apply wt_undef_regs; auto.
 - (* load *)
   simpl in *; InvBooleans.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index c9b07427..ffd9b227 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1893,15 +1893,10 @@ Proof.
   exact symbols_preserved. eauto.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
-   (* FIXME - MPPA specific *)
-  replace (destroyed_by_op op) with (@nil mreg).
-  replace (LTL.undef_regs nil rs) with rs.
-  apply agree_locs_set_reg; auto. auto. auto.
-(* (* The generic proof is there *)
   rewrite transl_destroyed_by_op.  apply agree_regs_undef_regs; auto.
   apply agree_locs_set_reg; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_op_caller_save.
   apply frame_set_reg. apply frame_undef_regs. exact SEP.
-*)
+
 - (* Lload *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'