Updated PR by removing whitespaces. Bug 17450.

1 files changed, 160 insertions, 160 deletions

diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 770648b1..e40c1322 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -53,7 +53,7 @@ Fixpoint vagree (v w: val) (x: nval) {struct x}: Prop :=
       match v, w with
       | Vint p, Vint q => iagree p q m
       | Vint p, _ => False
-      | _, _ => True                                 
+      | _, _ => True
       end
   | All => Val.lessdef v w
   end.
@@ -143,7 +143,7 @@ Lemma nge_lub_l:
   forall x y, nge (nlub x y) x.
 Proof.
   unfold nlub; destruct x, y; auto with na.
-  constructor. intros. autorewrite with ints; auto. rewrite H0; auto. 
+  constructor. intros. autorewrite with ints; auto. rewrite H0; auto.
 Qed.
 
 Lemma nge_lub_r:
@@ -171,13 +171,13 @@ Lemma iagree_and_eq:
   forall x y mask,
   iagree x y mask <-> Int.and x mask = Int.and y mask.
 Proof.
-  intros; split; intros. 
-- Int.bit_solve. specialize (H i H0). 
-  destruct (Int.testbit mask i). 
-  rewrite ! andb_true_r; auto. 
+  intros; split; intros.
+- Int.bit_solve. specialize (H i H0).
+  destruct (Int.testbit mask i).
+  rewrite ! andb_true_r; auto.
   rewrite ! andb_false_r; auto.
 - red; intros. exploit (eq_same_bits i); eauto; autorewrite with ints; auto.
-  rewrite H1. rewrite ! andb_true_r; auto. 
+  rewrite H1. rewrite ! andb_true_r; auto.
 Qed.
 
 Lemma iagree_mone:
@@ -203,7 +203,7 @@ Qed.
 Lemma iagree_not:
   forall x y m, iagree x y m -> iagree (Int.not x) (Int.not y) m.
 Proof.
-  intros; red; intros; autorewrite with ints; auto. f_equal; auto. 
+  intros; red; intros; autorewrite with ints; auto. f_equal; auto.
 Qed.
 
 Lemma iagree_not':
@@ -217,7 +217,7 @@ Lemma iagree_or:
   forall x y n m,
   iagree x y (Int.and m (Int.not n)) -> iagree (Int.or x n) (Int.or y n) m.
 Proof.
-  intros. apply iagree_not'. rewrite ! Int.not_or_and_not. apply iagree_and. 
+  intros. apply iagree_not'. rewrite ! Int.not_or_and_not. apply iagree_and.
   apply iagree_not; auto.
 Qed.
 
@@ -228,19 +228,19 @@ Lemma iagree_bitwise_binop:
   forall x1 x2 y1 y2 m,
   iagree x1 y1 m -> iagree x2 y2 m -> iagree (f x1 x2) (f y1 y2) m.
 Proof.
-  intros; red; intros. rewrite ! H by auto. f_equal; auto. 
+  intros; red; intros. rewrite ! H by auto. f_equal; auto.
 Qed.
 
 Lemma iagree_shl:
   forall x y m n,
   iagree x y (Int.shru m n) -> iagree (Int.shl x n) (Int.shl y n) m.
 Proof.
-  intros; red; intros. autorewrite with ints; auto. 
+  intros; red; intros. autorewrite with ints; auto.
   destruct (zlt i (Int.unsigned n)).
 - auto.
-- generalize (Int.unsigned_range n); intros. 
-  apply H. omega. rewrite Int.bits_shru by omega. 
-  replace (i - Int.unsigned n + Int.unsigned n) with i by omega. 
+- generalize (Int.unsigned_range n); intros.
+  apply H. omega. rewrite Int.bits_shru by omega.
+  replace (i - Int.unsigned n + Int.unsigned n) with i by omega.
   rewrite zlt_true by omega. auto.
 Qed.
 
@@ -248,11 +248,11 @@ Lemma iagree_shru:
   forall x y m n,
   iagree x y (Int.shl m n) -> iagree (Int.shru x n) (Int.shru y n) m.
 Proof.
-  intros; red; intros. autorewrite with ints; auto. 
+  intros; red; intros. autorewrite with ints; auto.
   destruct (zlt (i + Int.unsigned n) Int.zwordsize).
-- generalize (Int.unsigned_range n); intros. 
-  apply H. omega. rewrite Int.bits_shl by omega. 
-  replace (i + Int.unsigned n - Int.unsigned n) with i by omega. 
+- generalize (Int.unsigned_range n); intros.
+  apply H. omega. rewrite Int.bits_shl by omega.
+  replace (i + Int.unsigned n - Int.unsigned n) with i by omega.
   rewrite zlt_false by omega. auto.
 - auto.
 Qed.
@@ -262,8 +262,8 @@ Lemma iagree_shr_1:
   Int.shru (Int.shl m n) n = m ->
   iagree x y (Int.shl m n) -> iagree (Int.shr x n) (Int.shr y n) m.
 Proof.
-  intros; red; intros. rewrite <- H in H2. rewrite Int.bits_shru in H2 by auto. 
-  rewrite ! Int.bits_shr by auto. 
+  intros; red; intros. rewrite <- H in H2. rewrite Int.bits_shru in H2 by auto.
+  rewrite ! Int.bits_shr by auto.
   destruct (zlt (i + Int.unsigned n) Int.zwordsize).
 - apply H0; auto. generalize (Int.unsigned_range n); omega.
 - discriminate.
@@ -274,17 +274,17 @@ Lemma iagree_shr:
   iagree x y (Int.or (Int.shl m n) (Int.repr Int.min_signed)) ->
   iagree (Int.shr x n) (Int.shr y n) m.
 Proof.
-  intros; red; intros. rewrite ! Int.bits_shr by auto. 
-  generalize (Int.unsigned_range n); intros. 
+  intros; red; intros. rewrite ! Int.bits_shr by auto.
+  generalize (Int.unsigned_range n); intros.
   set (j := if zlt (i + Int.unsigned n) Int.zwordsize
             then i + Int.unsigned n
             else Int.zwordsize - 1).
   assert (0 <= j < Int.zwordsize).
   { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); omega. }
-  apply H; auto. autorewrite with ints; auto. apply orb_true_intro. 
+  apply H; auto. autorewrite with ints; auto. apply orb_true_intro.
   unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize).
-- left. rewrite zlt_false by omega. 
-  replace (i + Int.unsigned n - Int.unsigned n) with i by omega. 
+- left. rewrite zlt_false by omega.
+  replace (i + Int.unsigned n - Int.unsigned n) with i by omega.
   auto.
 - right. reflexivity.
 Qed.
@@ -302,14 +302,14 @@ Proof.
    mod Int.zwordsize) with i. auto.
   apply Int.eqmod_small_eq with Int.zwordsize; auto.
   apply Int.eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
-  apply Int.eqmod_refl2; omega. 
+  apply Int.eqmod_refl2; omega.
   eapply Int.eqmod_trans. 2: apply Int.eqmod_mod; auto.
-  apply Int.eqmod_add. 
-  apply Int.eqmod_mod; auto. 
-  apply Int.eqmod_refl. 
-  apply Z_mod_lt; auto. 
+  apply Int.eqmod_add.
+  apply Int.eqmod_mod; auto.
+  apply Int.eqmod_refl.
   apply Z_mod_lt; auto.
-Qed. 
+  apply Z_mod_lt; auto.
+Qed.
 
 Lemma iagree_ror:
   forall p q m amount,
@@ -317,9 +317,9 @@ Lemma iagree_ror:
   iagree (Int.ror p amount) (Int.ror q amount) m.
 Proof.
   intros. rewrite ! Int.ror_rol_neg by apply int_wordsize_divides_modulus.
-  apply iagree_rol. 
+  apply iagree_rol.
   rewrite Int.ror_rol_neg by apply int_wordsize_divides_modulus.
-  rewrite Int.neg_involutive; auto. 
+  rewrite Int.neg_involutive; auto.
 Qed.
 
 Lemma eqmod_iagree:
@@ -327,14 +327,14 @@ Lemma eqmod_iagree:
   Int.eqmod (two_p (Int.size m)) x y ->
   iagree (Int.repr x) (Int.repr y) m.
 Proof.
-  intros. set (p := nat_of_Z (Int.size m)). 
+  intros. set (p := nat_of_Z (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
   assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
   rewrite EQ in H; rewrite <- two_power_nat_two_p in H.
   red; intros. rewrite ! Int.testbit_repr by auto.
-  destruct (zlt i (Int.size m)). 
+  destruct (zlt i (Int.size m)).
   eapply Int.same_bits_eqmod; eauto. omega.
-  assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega). 
+  assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega).
   congruence.
 Qed.
 
@@ -345,12 +345,12 @@ Lemma iagree_eqmod:
   iagree x y (complete_mask m) ->
   Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
 Proof.
-  intros. set (p := nat_of_Z (Int.size m)). 
+  intros. set (p := nat_of_Z (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
   assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
-  rewrite EQ; rewrite <- two_power_nat_two_p. 
-  apply Int.eqmod_same_bits. intros. apply H. omega. 
-  unfold complete_mask. rewrite Int.bits_zero_ext by omega. 
+  rewrite EQ; rewrite <- two_power_nat_two_p.
+  apply Int.eqmod_same_bits. intros. apply H. omega.
+  unfold complete_mask. rewrite Int.bits_zero_ext by omega.
   rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto.
 Qed.
 
@@ -361,13 +361,13 @@ Proof.
 + subst m; reflexivity.
 + assert (Int.unsigned m <> 0).
   { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. }
-  assert (0 < Int.size m). 
+  assert (0 < Int.size m).
   { apply Int.Zsize_pos'. generalize (Int.unsigned_range m); omega. }
   generalize (Int.size_range m); intros.
-  f_equal. apply Int.bits_size_4. tauto. 
+  f_equal. apply Int.bits_size_4. tauto.
   rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega.
   apply Int.bits_mone; omega.
-  intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; omega. 
+  intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; omega.
 Qed.
 
 (** ** Abstract operations over value needs. *)
@@ -416,7 +416,7 @@ Proof.
   unfold orimm; intros; destruct x; simpl in *.
 - auto.
 - unfold Val.or; InvAgree. apply iagree_or; auto.
-- InvAgree. simpl. apply Val.lessdef_same. f_equal. apply iagree_mone. 
+- InvAgree. simpl. apply Val.lessdef_same. f_equal. apply iagree_mone.
   apply iagree_or. rewrite Int.and_commut. rewrite Int.and_mone. auto.
 Qed.
 
@@ -438,8 +438,8 @@ Lemma vagree_bitwise_binop:
          x.
 Proof.
   unfold bitwise; intros. destruct x; simpl in *.
-- auto. 
-- InvAgree. 
+- auto.
+- InvAgree.
 - inv H0; auto. inv H1; auto. destruct w1; auto.
 Qed.
 
@@ -482,8 +482,8 @@ Lemma shlimm_sound:
   vagree v w (shlimm x n) ->
   vagree (Val.shl v (Vint n)) (Val.shl w (Vint n)) x.
 Proof.
-  unfold shlimm; intros. unfold Val.shl. 
-  destruct (Int.ltu n Int.iwordsize). 
+  unfold shlimm; intros. unfold Val.shl.
+  destruct (Int.ltu n Int.iwordsize).
   destruct x; simpl in *.
 - auto.
 - InvAgree. apply iagree_shl; auto.
@@ -504,7 +504,7 @@ Lemma shruimm_sound:
   vagree (Val.shru v (Vint n)) (Val.shru w (Vint n)) x.
 Proof.
   unfold shruimm; intros. unfold Val.shru.
-  destruct (Int.ltu n Int.iwordsize). 
+  destruct (Int.ltu n Int.iwordsize).
   destruct x; simpl in *.
 - auto.
 - InvAgree. apply iagree_shru; auto.
@@ -528,10 +528,10 @@ Lemma shrimm_sound:
   vagree (Val.shr v (Vint n)) (Val.shr w (Vint n)) x.
 Proof.
   unfold shrimm; intros. unfold Val.shr.
-  destruct (Int.ltu n Int.iwordsize). 
+  destruct (Int.ltu n Int.iwordsize).
   destruct x; simpl in *.
 - auto.
-- InvAgree. 
+- InvAgree.
   destruct (Int.eq_dec (Int.shru (Int.shl m n) n) m).
   apply iagree_shr_1; auto.
   apply iagree_shr; auto.
@@ -553,10 +553,10 @@ Lemma rolm_sound:
 Proof.
   unfold rolm; intros; destruct x; simpl in *.
 - auto.
-- unfold Val.rolm; InvAgree. unfold Int.rolm. 
-  apply iagree_and. apply iagree_rol. auto. 
-- unfold Val.rolm; InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone. 
-  unfold Int.rolm. apply iagree_and. apply iagree_rol. rewrite Int.and_commut. 
+- unfold Val.rolm; InvAgree. unfold Int.rolm.
+  apply iagree_and. apply iagree_rol. auto.
+- unfold Val.rolm; InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone.
+  unfold Int.rolm. apply iagree_and. apply iagree_rol. rewrite Int.and_commut.
   rewrite Int.and_mone. auto.
 Qed.
 
@@ -573,15 +573,15 @@ Lemma ror_sound:
   vagree (Val.ror v (Vint n)) (Val.ror w (Vint n)) x.
 Proof.
   unfold ror; intros. unfold Val.ror.
-  destruct (Int.ltu n Int.iwordsize). 
+  destruct (Int.ltu n Int.iwordsize).
   destruct x; simpl in *.
 - auto.
-- InvAgree. apply iagree_ror; auto. 
+- InvAgree. apply iagree_ror; auto.
 - inv H; auto.
 - destruct v; auto with na.
 Qed.
 
-(** Modular arithmetic operations: add, mul, opposite.  
+(** Modular arithmetic operations: add, mul, opposite.
     (But not subtraction because of the pointer - pointer case. *)
 
 Definition modarith (x: nval) :=
@@ -596,10 +596,10 @@ Lemma add_sound:
   vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
   vagree (Val.add v1 v2) (Val.add w1 w2) x.
 Proof.
-  unfold modarith; intros. destruct x; simpl in *. 
+  unfold modarith; intros. destruct x; simpl in *.
 - auto.
-- unfold Val.add; InvAgree. apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto. 
-- inv H; auto. inv H0; auto. destruct w1; auto. 
+- unfold Val.add; InvAgree. apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto.
+- inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
 Remark modarith_idem: forall nv, modarith (modarith nv) = modarith nv.
@@ -612,10 +612,10 @@ Lemma mul_sound:
   vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
   vagree (Val.mul v1 v2) (Val.mul w1 w2) x.
 Proof.
-  unfold mul, add; intros. destruct x; simpl in *. 
+  unfold mul, add; intros. destruct x; simpl in *.
 - auto.
-- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto. 
-- inv H; auto. inv H0; auto. destruct w1; auto. 
+- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto.
+- inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
 Lemma neg_sound:
@@ -625,8 +625,8 @@ Lemma neg_sound:
 Proof.
   intros; destruct x; simpl in *.
 - auto.
-- unfold Val.neg; InvAgree. 
-  apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto. 
+- unfold Val.neg; InvAgree.
+  apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto.
 - inv H; simpl; auto.
 Qed.
 
@@ -648,12 +648,12 @@ Proof.
   unfold zero_ext; intros.
   destruct x; simpl in *.
 - auto.
-- unfold Val.zero_ext; InvAgree. 
-  red; intros. autorewrite with ints; try omega. 
+- unfold Val.zero_ext; InvAgree.
+  red; intros. autorewrite with ints; try omega.
   destruct (zlt i1 n); auto. apply H; auto.
   autorewrite with ints; try omega. rewrite zlt_true; auto.
-- unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. 
-  Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto. 
+- unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal.
+  Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto.
   autorewrite with ints; try omega. apply zlt_true; auto.
 Qed.
 
@@ -672,25 +672,25 @@ Lemma sign_ext_sound:
 Proof.
   unfold sign_ext; intros. destruct x; simpl in *.
 - auto.
-- unfold Val.sign_ext; InvAgree. 
+- unfold Val.sign_ext; InvAgree.
   red; intros. autorewrite with ints; try omega.
   set (j := if zlt i1 n then i1 else n - 1).
-  assert (0 <= j < Int.zwordsize). 
+  assert (0 <= j < Int.zwordsize).
   { unfold j; destruct (zlt i1 n); omega. }
-  apply H; auto. 
-  autorewrite with ints; try omega. apply orb_true_intro. 
-  unfold j; destruct (zlt i1 n). 
-  left. rewrite zlt_true; auto. 
-  right. rewrite Int.unsigned_repr. rewrite zlt_false by omega. 
-  replace (n - 1 - (n - 1)) with 0 by omega. reflexivity. 
+  apply H; auto.
+  autorewrite with ints; try omega. apply orb_true_intro.
+  unfold j; destruct (zlt i1 n).
+  left. rewrite zlt_true; auto.
+  right. rewrite Int.unsigned_repr. rewrite zlt_false by omega.
+  replace (n - 1 - (n - 1)) with 0 by omega. reflexivity.
   generalize Int.wordsize_max_unsigned; omega.
-- unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. 
+- unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal.
   Int.bit_solve; try omega.
   set (j := if zlt i1 n then i1 else n - 1).
-  assert (0 <= j < Int.zwordsize). 
+  assert (0 <= j < Int.zwordsize).
   { unfold j; destruct (zlt i1 n); omega. }
-  apply H; auto. rewrite Int.bits_zero_ext; try omega. 
-  rewrite zlt_true. apply Int.bits_mone; auto. 
+  apply H; auto. rewrite Int.bits_zero_ext; try omega.
+  rewrite zlt_true. apply Int.bits_mone; auto.
   unfold j. destruct (zlt i1 n); omega.
 Qed.
 
@@ -713,25 +713,25 @@ Proof.
                      (list_repeat (size_chunk_nat chunk) Undef)
                      (encode_val chunk w)).
   {
-     rewrite <- (encode_val_length chunk w). 
+     rewrite <- (encode_val_length chunk w).
      apply repeat_Undef_inject_any.
   }
   assert (SAME: forall vl1 vl2,
                 vl1 = vl2 ->
                 list_forall2 memval_lessdef vl1 vl2).
   {
-     intros. subst vl2. revert vl1. induction vl1; constructor; auto. 
-     apply memval_lessdef_refl. 
+     intros. subst vl2. revert vl1. induction vl1; constructor; auto.
+     apply memval_lessdef_refl.
   }
 
   intros. unfold store_argument in H; destruct chunk.
-- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod. 
+- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod.
   change 8 with (Int.size (Int.repr 255)). apply iagree_eqmod; auto.
-- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod. 
+- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod.
   change 8 with (Int.size (Int.repr 255)). apply iagree_eqmod; auto.
-- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod. 
+- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod.
   change 16 with (Int.size (Int.repr 65535)). apply iagree_eqmod; auto.
-- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod. 
+- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod.
   change 16 with (Int.size (Int.repr 65535)). apply iagree_eqmod; auto.
 - apply encode_val_inject. rewrite val_inject_id; auto.
 - apply encode_val_inject. rewrite val_inject_id; auto.
@@ -768,7 +768,7 @@ Lemma maskzero_sound:
   Val.maskzero_bool v n = Some b ->
   Val.maskzero_bool w n = Some b.
 Proof.
-  unfold maskzero; intros. 
+  unfold maskzero; intros.
   unfold Val.maskzero_bool; InvAgree; try discriminate.
   inv H0. rewrite iagree_and_eq in H. rewrite H. auto.
 Qed.
@@ -795,9 +795,9 @@ Let valid_pointer_inj:
   Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 Proof.
-  unfold inject_id; intros. inv H. rewrite Int.add_zero. 
+  unfold inject_id; intros. inv H. rewrite Int.add_zero.
   rewrite Mem.valid_pointer_nonempty_perm in *. eauto.
-Qed. 
+Qed.
 
 Let weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
@@ -805,7 +805,7 @@ Let weak_valid_pointer_inj:
   Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 Proof.
-  unfold inject_id; intros. inv H. rewrite Int.add_zero. 
+  unfold inject_id; intros. inv H. rewrite Int.add_zero.
   rewrite Mem.weak_valid_pointer_spec in *.
   rewrite ! Mem.valid_pointer_nonempty_perm in *.
   destruct H0; [left|right]; eauto.
@@ -830,7 +830,7 @@ Let valid_different_pointers_inj:
   b1' <> b2' \/
   Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
 Proof.
-  unfold inject_id; intros. left; congruence. 
+  unfold inject_id; intros. left; congruence.
 Qed.
 
 Lemma default_needs_of_condition_sound:
@@ -846,7 +846,7 @@ Qed.
 Lemma default_needs_of_operation_sound:
   forall op args1 v1 args2 nv,
   eval_operation ge (Vptr sp Int.zero) op args1 m1 = Some v1 ->
-  vagree_list args1 args2 nil 
+  vagree_list args1 args2 nil
   \/ vagree_list args1 args2 (default nv :: nil)
   \/ vagree_list args1 args2 (default nv :: default nv :: nil) ->
   nv <> Nothing ->
@@ -854,12 +854,12 @@ Lemma default_needs_of_operation_sound:
      eval_operation ge (Vptr sp Int.zero) op args2 m2 = Some v2
   /\ vagree v1 v2 nv.
 Proof.
-  intros. assert (default nv = All) by (destruct nv; simpl; congruence). 
+  intros. assert (default nv = All) by (destruct nv; simpl; congruence).
   rewrite H2 in H0.
   assert (Val.lessdef_list args1 args2).
   {
-    destruct H0. auto with na. 
-    destruct H0. inv H0; constructor; auto with na. 
+    destruct H0. auto with na.
+    destruct H0. inv H0; constructor; auto with na.
     inv H0; constructor; auto with na. inv H8; constructor; auto with na.
   }
   exploit (@eval_operation_inj _ _ _ _ ge ge inject_id).
@@ -869,7 +869,7 @@ Proof.
   apply val_inject_list_lessdef; eauto.
   eauto.
   intros (v2 & A & B). exists v2; split; auto.
-  apply vagree_lessdef. apply val_inject_lessdef. auto. 
+  apply vagree_lessdef. apply val_inject_lessdef. auto.
 Qed.
 
 End DEFAULT.
@@ -890,12 +890,12 @@ Lemma andimm_redundant_sound:
   vagree (Val.and v (Vint n)) w x.
 Proof.
   unfold andimm_redundant; intros. destruct x; try discriminate.
-- simpl; auto. 
+- simpl; auto.
 - InvBooleans. simpl in *; unfold Val.and; InvAgree.
-  red; intros. exploit (eq_same_bits i1); eauto. 
-  autorewrite with ints; auto. rewrite H2; simpl; intros. 
-  destruct (Int.testbit n i1) eqn:N; try discriminate. 
-  rewrite andb_true_r. apply H0; auto. autorewrite with ints; auto. 
+  red; intros. exploit (eq_same_bits i1); eauto.
+  autorewrite with ints; auto. rewrite H2; simpl; intros.
+  destruct (Int.testbit n i1) eqn:N; try discriminate.
+  rewrite andb_true_r. apply H0; auto. autorewrite with ints; auto.
   rewrite H2, N; auto.
 Qed.
 
@@ -915,7 +915,7 @@ Proof.
   unfold orimm_redundant; intros. destruct x; try discriminate.
 - auto.
 - InvBooleans. simpl in *; unfold Val.or; InvAgree.
-  apply iagree_not'. rewrite Int.not_or_and_not. 
+  apply iagree_not'. rewrite Int.not_or_and_not.
   apply (andimm_redundant_sound (Vint (Int.not i)) (Vint (Int.not i0)) (I m) (Int.not n)).
   simpl. rewrite Int.not_involutive. apply proj_sumbool_is_true. auto.
   simpl. apply iagree_not; auto.
@@ -933,9 +933,9 @@ Proof.
   unfold rolm_redundant; intros; InvBooleans. subst amount. rewrite Val.rolm_zero.
   apply andimm_redundant_sound; auto.
   assert (forall n, Int.ror n Int.zero = n).
-  { intros. rewrite Int.ror_rol_neg by apply int_wordsize_divides_modulus. 
+  { intros. rewrite Int.ror_rol_neg by apply int_wordsize_divides_modulus.
     rewrite Int.neg_zero. apply Int.rol_zero. }
-  unfold rolm, andimm in *. destruct x; auto. 
+  unfold rolm, andimm in *. destruct x; auto.
   rewrite H in H0. auto.
   rewrite H in H0. auto.
 Qed.
@@ -956,8 +956,8 @@ Lemma zero_ext_redundant_sound:
 Proof.
   unfold zero_ext_redundant; intros. destruct x; try discriminate.
 - auto.
-- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. 
-  red; intros; autorewrite with ints; try omega. 
+- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H.
+  red; intros; autorewrite with ints; try omega.
   destruct (zlt i1 n). apply H0; auto.
   rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate.
 Qed.
@@ -978,10 +978,10 @@ Lemma sign_ext_redundant_sound:
 Proof.
   unfold sign_ext_redundant; intros. destruct x; try discriminate.
 - auto.
-- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. 
-  red; intros; autorewrite with ints; try omega. 
+- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H.
+  red; intros; autorewrite with ints; try omega.
   destruct (zlt i1 n). apply H0; auto.
-  rewrite Int.bits_or; auto. rewrite H3; auto. 
+  rewrite Int.bits_or; auto. rewrite H3; auto.
   rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate.
 Qed.
 
@@ -1014,7 +1014,7 @@ End NVal.
 
 Module NE := LPMap1(NVal).
 
-Definition nenv := NE.t. 
+Definition nenv := NE.t.
 
 Definition nreg (ne: nenv) (r: reg) := NE.get r ne.
 
@@ -1024,7 +1024,7 @@ Definition eagree (e1 e2: regset) (ne: nenv) : Prop :=
 Lemma nreg_agree:
   forall rs1 rs2 ne r, eagree rs1 rs2 ne -> vagree rs1#r rs2#r (nreg ne r).
 Proof.
-  intros. apply H. 
+  intros. apply H.
 Qed.
 
 Hint Resolve nreg_agree: na.
@@ -1033,7 +1033,7 @@ Lemma eagree_ge:
   forall e1 e2 ne ne',
   eagree e1 e2 ne -> NE.ge ne ne' -> eagree e1 e2 ne'.
 Proof.
-  intros; red; intros. apply nge_agree with (NE.get r ne); auto. apply H0.  
+  intros; red; intros. apply nge_agree with (NE.get r ne); auto. apply H0.
 Qed.
 
 Lemma eagree_bot:
@@ -1045,15 +1045,15 @@ Qed.
 Lemma eagree_same:
   forall e ne, eagree e e ne.
 Proof.
-  intros; red; intros. apply vagree_same. 
+  intros; red; intros. apply vagree_same.
 Qed.
 
 Lemma eagree_update_1:
   forall e1 e2 ne v1 v2 nv r,
   eagree e1 e2 ne -> vagree v1 v2 nv -> eagree (e1#r <- v1) (e2#r <- v2) (NE.set r nv ne).
 Proof.
-  intros; red; intros. rewrite NE.gsspec. rewrite ! PMap.gsspec. 
-  destruct (peq r0 r); auto. 
+  intros; red; intros. rewrite NE.gsspec. rewrite ! PMap.gsspec.
+  destruct (peq r0 r); auto.
 Qed.
 
 Lemma eagree_update:
@@ -1062,7 +1062,7 @@ Lemma eagree_update:
   eagree e1 e2 (NE.set r Nothing ne) ->
   eagree (e1#r <- v1) (e2#r <- v2) ne.
 Proof.
-  intros; red; intros. specialize (H0 r0). rewrite NE.gsspec in H0. 
+  intros; red; intros. specialize (H0 r0). rewrite NE.gsspec in H0.
   rewrite ! PMap.gsspec. destruct (peq r0 r).
   subst r0. auto.
   auto.
@@ -1073,8 +1073,8 @@ Lemma eagree_update_dead:
   nreg ne r = Nothing ->
   eagree e1 e2 ne -> eagree (e1#r <- v1) e2 ne.
 Proof.
-  intros; red; intros. rewrite PMap.gsspec. 
-  destruct (peq r0 r); auto. subst. unfold nreg in H. rewrite H. red; auto. 
+  intros; red; intros. rewrite PMap.gsspec.
+  destruct (peq r0 r); auto. subst. unfold nreg in H. rewrite H. red; auto.
 Qed.
 
 (** * Neededness for memory locations *)
@@ -1146,12 +1146,12 @@ Lemma nlive_add:
   Int.unsigned ofs <= i < Int.unsigned ofs + sz ->
   nlive (nmem_add nm p sz) b i.
 Proof.
-  intros. unfold nmem_add. destruct nm. apply nlive_all. 
-  inv H1; try (apply nlive_all). 
+  intros. unfold nmem_add. destruct nm. apply nlive_all.
+  inv H1; try (apply nlive_all).
   - (* Gl id ofs *)
-    assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). 
+    assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto).
     destruct gl!id as [iv|] eqn:NG.
-  + constructor; simpl; intros. 
+  + constructor; simpl; intros.
     congruence.
     assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0.
     rewrite PTree.gss in H5. inv H5. rewrite ISet.In_remove.
@@ -1161,13 +1161,13 @@ Proof.
     assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0.
     congruence.
   - (* Glo id *)
-    assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). 
+    assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto).
     constructor; simpl; intros.
     congruence.
-    assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. 
+    assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0.
     rewrite PTree.grs in H5. congruence.
   - (* Stk ofs *)
-    constructor; simpl; intros. 
+    constructor; simpl; intros.
     rewrite ISet.In_remove. intros [A B]. elim A; auto.
     assert (bc b = BCglob id) by (eapply H; eauto). congruence.
   - (* Stack *)
@@ -1183,19 +1183,19 @@ Proof.
   intros. inversion H; subst. unfold nmem_add; destruct p; try (apply nlive_all).
 - (* Gl id ofs *)
   destruct gl!id as [iv|] eqn:NG.
-  + split; simpl; intros. auto. 
-    rewrite PTree.gsspec in H1. destruct (peq id0 id); eauto. inv H1. 
+  + split; simpl; intros. auto.
+    rewrite PTree.gsspec in H1. destruct (peq id0 id); eauto. inv H1.
     rewrite ISet.In_remove. intros [P Q]. eelim GL; eauto.
-  + auto. 
+  + auto.
 - (* Glo id *)
-  split; simpl; intros. auto. 
+  split; simpl; intros. auto.
   rewrite PTree.grspec in H1. destruct (PTree.elt_eq id0 id). congruence. eauto.
 - (* Stk ofs *)
-  split; simpl; intros. 
+  split; simpl; intros.
   rewrite ISet.In_remove. intros [P Q]. eelim STK; eauto.
   eauto.
 - (* Stack *)
-  split; simpl; intros. 
+  split; simpl; intros.
   apply ISet.In_empty.
   eauto.
 Qed.
@@ -1243,13 +1243,13 @@ Proof.
   split; simpl; auto; intros.
   rewrite PTree.gsspec in H6. destruct (peq id0 id).
 + inv H6. destruct H3. congruence. destruct gl!id as [iv0|] eqn:NG.
-  rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto. 
-  rewrite ISet.In_interval. omega. 
-+ eauto. 
+  rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto.
+  rewrite ISet.In_interval. omega.
++ eauto.
 - (* Stk ofs *)
-  split; simpl; auto; intros. destruct H3. 
-  elim H3. subst b'. eapply bc_stack; eauto. 
-  rewrite ISet.In_add. intros [P|P]. omega. eapply STK; eauto. 
+  split; simpl; auto; intros. destruct H3.
+  elim H3. subst b'. eapply bc_stack; eauto.
+  rewrite ISet.In_add. intros [P|P]. omega. eapply STK; eauto.
 Qed.
 
 (** Test (conservatively) whether some locations in the range delimited
@@ -1284,12 +1284,12 @@ Proof.
   inv H1; try discriminate.
 - (* Gl id ofs *)
   assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto).
-  destruct gl!id as [iv|] eqn:HG; inv H2. 
+  destruct gl!id as [iv|] eqn:HG; inv H2.
   destruct (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) iv) eqn:IC; try discriminate.
   rewrite ISet.contains_spec in IC. eelim GL; eauto.
-- (* Stk ofs *) 
+- (* Stk ofs *)
   destruct (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) stk) eqn:IC; try discriminate.
-  rewrite ISet.contains_spec in IC. eelim STK; eauto. eapply bc_stack; eauto. 
+  rewrite ISet.contains_spec in IC. eelim STK; eauto. eapply bc_stack; eauto.
 Qed.
 
 (** Kill all stack locations between 0 and [sz], and mark everything else
@@ -1303,7 +1303,7 @@ Lemma nlive_dead_stack:
   forall sz b' i, b' <> sp \/ ~(0 <= i < sz) -> nlive (nmem_dead_stack sz) b' i.
 Proof.
   intros; constructor; simpl; intros.
-- rewrite ISet.In_interval. intuition. 
+- rewrite ISet.In_interval. intuition.
 - rewrite PTree.gempty in H1; discriminate.
 Qed.
 
@@ -1330,10 +1330,10 @@ Proof.
   intros. inversion H; subst. destruct nm2; simpl. auto.
   constructor; simpl; intros.
 - rewrite ISet.In_inter. intros [P Q]. eelim STK; eauto.
-- rewrite PTree.gcombine in H1 by auto. 
+- rewrite PTree.gcombine in H1 by auto.
   destruct gl!id as [iv1|] eqn:NG1; try discriminate;
   destruct gl0!id as [iv2|] eqn:NG2; inv H1.
-  rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto. 
+  rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto.
 Qed.
 
 Lemma nlive_lub_r:
@@ -1342,10 +1342,10 @@ Proof.
   intros. inversion H; subst. destruct nm1; simpl. auto.
   constructor; simpl; intros.
 - rewrite ISet.In_inter. intros [P Q]. eelim STK; eauto.
-- rewrite PTree.gcombine in H1 by auto. 
+- rewrite PTree.gcombine in H1 by auto.
   destruct gl0!id as [iv1|] eqn:NG1; try discriminate;
   destruct gl!id as [iv2|] eqn:NG2; inv H1.
-  rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto. 
+  rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto.
 Qed.
 
 (** Boolean-valued equality test *)
@@ -1362,18 +1362,18 @@ Lemma nmem_beq_sound:
   nmem_beq nm1 nm2 = true ->
   (nlive nm1 b ofs <-> nlive nm2 b ofs).
 Proof.
-  unfold nmem_beq; intros. 
+  unfold nmem_beq; intros.
   destruct nm1 as [ | stk1 gl1]; destruct nm2 as [ | stk2 gl2]; try discriminate.
 - split; intros L; inv L.
 - InvBooleans. rewrite ISet.beq_spec in H0. rewrite PTree.beq_correct in H1.
   split; intros L; inv L; constructor; intros.
-+ rewrite <- H0. eauto. 
++ rewrite <- H0. eauto.
 + specialize (H1 id). rewrite H2 in H1. destruct gl1!id as [iv1|] eqn: NG; try contradiction.
-  rewrite ISet.beq_spec in H1. rewrite <- H1. eauto. 
-+ rewrite H0. eauto. 
+  rewrite ISet.beq_spec in H1. rewrite <- H1. eauto.
++ rewrite H0. eauto.
 + specialize (H1 id). rewrite H2 in H1. destruct gl2!id as [iv2|] eqn: NG; try contradiction.
   rewrite ISet.beq_spec in H1. rewrite H1. eauto.
-Qed. 
+Qed.
 
 End LOCATIONS.
 
@@ -1390,11 +1390,11 @@ Module NA <: SEMILATTICE.
 
   Lemma eq_refl: forall x, eq x x.
   Proof.
-    unfold eq; destruct x; simpl; split. apply NE.eq_refl. tauto. 
+    unfold eq; destruct x; simpl; split. apply NE.eq_refl. tauto.
   Qed.
   Lemma eq_sym: forall x y, eq x y -> eq y x.
   Proof.
-    unfold eq; destruct x, y; simpl. intros [A B]. 
+    unfold eq; destruct x, y; simpl. intros [A B].
     split. apply NE.eq_sym; auto.
     intros. rewrite B. tauto.
   Qed.
@@ -1407,10 +1407,10 @@ Module NA <: SEMILATTICE.
 
   Definition beq (x y: t) : bool :=
     NE.beq (fst x) (fst y) && nmem_beq (snd x) (snd y).
- 
+
   Lemma beq_correct: forall x y, beq x y = true -> eq x y.
   Proof.
-    unfold beq, eq; destruct x, y; simpl; intros. InvBooleans. split. 
+    unfold beq, eq; destruct x, y; simpl; intros. InvBooleans. split.
     apply NE.beq_correct; auto.
     intros. apply nmem_beq_sound; auto.
   Qed.
@@ -1438,7 +1438,7 @@ Module NA <: SEMILATTICE.
   Proof.
     unfold ge, bot; destruct x; simpl. split.
     apply NE.ge_bot.
-    intros. inv H. 
+    intros. inv H.
   Qed.
 
   Definition lub (x y: t) : t :=
@@ -1446,13 +1446,13 @@ Module NA <: SEMILATTICE.
 
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
-    unfold ge; destruct x, y; simpl; split. 
+    unfold ge; destruct x, y; simpl; split.
     apply NE.ge_lub_left.
     intros; apply nlive_lub_l; auto.
   Qed.
   Lemma ge_lub_right: forall x y, ge (lub x y) y.
   Proof.
-    unfold ge; destruct x, y; simpl; split. 
+    unfold ge; destruct x, y; simpl; split.
     apply NE.ge_lub_right.
     intros; apply nlive_lub_r; auto.
   Qed.