Updated PR by removing whitespaces. Bug 17450.

1 files changed, 134 insertions, 134 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 938454c5..7e966ffe 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -85,7 +85,7 @@ Proof.
   intros until ty. destruct a; simpl; congruence.
 Qed.
 
-Local Open Scope option_monad_scope. 
+Local Open Scope option_monad_scope.
 
 Fixpoint is_val_list (al: exprlist) : option (list (val * type)) :=
   match al with
@@ -110,7 +110,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval :=
   | Vfloat f, AST.Tfloat => Some (EVfloat f)
   | Vsingle f, AST.Tsingle => Some (EVsingle f)
   | Vlong n, AST.Tlong => Some (EVlong n)
-  | Vptr b ofs, AST.Tint => 
+  | Vptr b ofs, AST.Tint =>
       do id <- Genv.invert_symbol ge b;
       check (Genv.public_symbol ge id);
       Some (EVptr_global id ofs)
@@ -153,7 +153,7 @@ Lemma eventval_of_val_complete:
   forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.
 Proof.
   induction 1; simpl; auto.
-  rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. auto. 
+  rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. auto.
 Qed.
 
 Lemma list_eventval_of_val_sound:
@@ -169,7 +169,7 @@ Qed.
 Lemma list_eventval_of_val_complete:
   forall evl tl vl, eventval_list_match ge evl tl vl -> list_eventval_of_val vl tl = Some evl.
 Proof.
-  induction 1; simpl. auto. 
+  induction 1; simpl. auto.
   rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto.
 Qed.
 
@@ -190,7 +190,7 @@ Qed.
 
 (** Volatile memory accesses. *)
 
-Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) 
+Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int)
                              : option (world * trace * val) :=
   if Genv.block_is_volatile ge b then
     do id <- Genv.invert_symbol ge b;
@@ -230,11 +230,11 @@ Lemma do_volatile_load_sound:
   do_volatile_load w chunk m b ofs = Some(w', t, v) ->
   volatile_load ge chunk m b ofs t v /\ possible_trace w t w'.
 Proof.
-  intros until v. unfold do_volatile_load. mydestr. 
-  destruct p as [ev w'']. mydestr. 
-  split. constructor; auto. apply Genv.invert_find_symbol; auto. 
-  apply val_of_eventval_sound; auto. 
-  econstructor. constructor; eauto. constructor. 
+  intros until v. unfold do_volatile_load. mydestr.
+  destruct p as [ev w'']. mydestr.
+  split. constructor; auto. apply Genv.invert_find_symbol; auto.
+  apply val_of_eventval_sound; auto.
+  econstructor. constructor; eauto. constructor.
   split. constructor; auto. constructor.
 Qed.
 
@@ -254,10 +254,10 @@ Lemma do_volatile_store_sound:
   do_volatile_store w chunk m b ofs v = Some(w', t, m') ->
   volatile_store ge chunk m b ofs v t m' /\ possible_trace w t w'.
 Proof.
-  intros until m'. unfold do_volatile_store. mydestr. 
-  split. constructor; auto. apply Genv.invert_find_symbol; auto. 
-  apply eventval_of_val_sound; auto. 
-  econstructor. constructor; eauto. constructor. 
+  intros until m'. unfold do_volatile_store. mydestr.
+  split. constructor; auto. apply Genv.invert_find_symbol; auto.
+  apply eventval_of_val_sound; auto.
+  econstructor. constructor; eauto. constructor.
   split. constructor; auto. constructor.
 Qed.
 
@@ -297,7 +297,7 @@ Remark check_assign_copy:
   forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int),
   { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
 Proof with try (right; intuition omega).
-  intros. unfold assign_copy_ok. 
+  intros. unfold assign_copy_ok.
   assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos.
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs')); auto...
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs)); auto...
@@ -314,7 +314,7 @@ Proof with try (right; intuition omega).
   destruct (zle (Int.unsigned ofs' + sizeof ge ty) (Int.unsigned ofs)); auto.
   destruct (zle (Int.unsigned ofs + sizeof ge ty) (Int.unsigned ofs')); auto.
   right; intuition omega.
-  destruct Y... left; intuition omega. 
+  destruct Y... left; intuition omega.
 Defined.
 
 Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) :=
@@ -343,8 +343,8 @@ Lemma do_deref_loc_sound:
   deref_loc ge ty m b ofs t v /\ possible_trace w t w'.
 Proof.
   unfold do_deref_loc; intros until v.
-  destruct (access_mode ty) eqn:?; mydestr. 
-  intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto. 
+  destruct (access_mode ty) eqn:?; mydestr.
+  intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto.
   split. eapply deref_loc_value; eauto. constructor.
   split. eapply deref_loc_reference; eauto. constructor.
   split. eapply deref_loc_copy; eauto. constructor.
@@ -368,10 +368,10 @@ Lemma do_assign_loc_sound:
   assign_loc ge ty m b ofs v t m' /\ possible_trace w t w'.
 Proof.
   unfold do_assign_loc; intros until m'.
-  destruct (access_mode ty) eqn:?; mydestr. 
-  intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto. 
+  destruct (access_mode ty) eqn:?; mydestr.
+  intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto.
   split. eapply assign_loc_value; eauto. constructor.
-  destruct v; mydestr. destruct a as [P [Q R]]. 
+  destruct v; mydestr. destruct a as [P [Q R]].
   split. eapply assign_loc_copy; eauto. constructor.
 Qed.
 
@@ -385,7 +385,7 @@ Proof.
   rewrite H1; rewrite H2. apply do_volatile_store_complete; auto.
   rewrite H1. destruct (check_assign_copy ty b ofs b' ofs').
   inv H0. rewrite H5; rewrite H6; auto.
-  elim n. red; tauto. 
+  elim n. red; tauto.
 Qed.
 
 (** External calls *)
@@ -477,7 +477,7 @@ Remark memcpy_check_args:
   forall sz al bdst odst bsrc osrc,
   {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}.
 Proof with try (right; intuition omega).
-  intros. 
+  intros.
   assert (X: {al = 1 \/ al = 2 \/ al = 4 \/ al = 8} + {~(al = 1 \/ al = 2 \/ al = 4 \/ al = 8)}).
     destruct (zeq al 1); auto. destruct (zeq al 2); auto.
     destruct (zeq al 4); auto. destruct (zeq al 8); auto...
@@ -486,9 +486,9 @@ Proof with try (right; intuition omega).
   destruct (zle 0 sz)...
   destruct (Zdivide_dec al sz); auto...
   assert(U: forall x, {sz > 0 -> (al | x)} + {~(sz > 0 -> (al | x))}).
-    intros. destruct (zeq sz 0). 
+    intros. destruct (zeq sz 0).
     left; intros; omegaContradiction.
-    destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega. 
+    destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega.
   destruct (U osrc); auto...
   destruct (U odst); auto...
   assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc}
@@ -555,17 +555,17 @@ Proof with try congruence.
   intros until m'.
   destruct ef; simpl.
 (* EF_external *)
-  eapply do_external_function_sound; eauto. 
+  eapply do_external_function_sound; eauto.
 (* EF_builtin *)
-  eapply do_external_function_sound; eauto. 
+  eapply do_external_function_sound; eauto.
 (* EF_vload *)
-  unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... 
+  unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
   mydestr. destruct p as [[w'' t''] v]; mydestr.
-  exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. 
+  exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto.
   auto.
 (* EF_vstore *)
-  unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... 
-  mydestr. destruct p as [[w'' t''] m'']. mydestr. 
+  unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs...
+  mydestr. destruct p as [[w'' t''] m'']. mydestr.
   exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
   auto.
 (* EF_malloc *)
@@ -573,19 +573,19 @@ Proof with try congruence.
   destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b] eqn:?. mydestr.
   split. econstructor; eauto. constructor.
 (* EF_free *)
-  unfold do_ef_free. destruct vargs... destruct v... destruct vargs... 
-  mydestr. destruct v... mydestr. 
+  unfold do_ef_free. destruct vargs... destruct v... destruct vargs...
+  mydestr. destruct v... mydestr.
   split. econstructor; eauto. omega. constructor.
 (* EF_memcpy *)
-  unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... 
-  destruct v... destruct vargs... mydestr. red in m0. 
+  unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
+  destruct v... destruct vargs... mydestr. red in m0.
   split. econstructor; eauto; tauto. constructor.
 (* EF_annot *)
-  unfold do_ef_annot. mydestr. 
+  unfold do_ef_annot. mydestr.
   split. constructor. apply list_eventval_of_val_sound; auto.
   econstructor. constructor; eauto. constructor.
 (* EF_annot_val *)
-  unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. 
+  unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr.
   split. constructor. apply eventval_of_val_sound; auto.
   econstructor. constructor; eauto. constructor.
 (* EF_inline_asm *)
@@ -611,7 +611,7 @@ Proof.
   inv H; unfold do_ef_volatile_store.
   exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
 (* EF_malloc *)
-  inv H; unfold do_ef_malloc. 
+  inv H; unfold do_ef_malloc.
   inv H0. rewrite H1. rewrite H2. auto.
 (* EF_free *)
   inv H; unfold do_ef_free.
@@ -619,12 +619,12 @@ Proof.
 (* EF_memcpy *)
   inv H; unfold do_ef_memcpy.
   inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto.
-  red. tauto. 
+  red. tauto.
 (* EF_annot *)
-  inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. 
+  inv H; unfold do_ef_annot. inv H0. inv H6. inv H4.
   rewrite (list_eventval_of_val_complete _ _ _ H1). auto.
 (* EF_annot_val *)
-  inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. 
+  inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4.
   rewrite (eventval_of_val_complete _ _ _ H1). auto.
 (* EF_inline_asm *)
   eapply do_inline_assembly_complete; eauto.
@@ -837,7 +837,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           do w',t, v1 <- do_deref_loc w ty m b ofs;
           let op := match id with Incr => Oadd | Decr => Osub end in
           let r' :=
-            Ecomma (Eassign (Eloc b ofs ty) 
+            Ecomma (Eassign (Eloc b ofs ty)
                            (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (incrdecr_type ty))
                            ty)
                    (Eval v1 ty) ty in
@@ -922,7 +922,7 @@ Inductive imm_safe_t: kind -> expr -> mem -> Prop :=
 Remark imm_safe_t_imm_safe:
   forall k a m, imm_safe_t k a m -> imm_safe ge e k a m.
 Proof.
-  induction 1. 
+  induction 1.
   constructor.
   constructor.
   eapply imm_safe_lred; eauto.
@@ -975,7 +975,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists t, exists v1, exists w',
       ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w'
   | Epostincr id (Eloc b ofs ty1) ty =>
-      exists t, exists v1, exists w', 
+      exists t, exists v1, exists w',
       ty = ty1 /\ deref_loc ge ty m b ofs t v1 /\ possible_trace w t w'
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
@@ -1004,7 +1004,7 @@ Proof.
   exists b; auto.
   exists b; auto.
   exists b; exists ofs; auto.
-  exists b; exists ofs; split; auto. exists co, delta; auto. 
+  exists b; exists ofs; split; auto. exists co, delta; auto.
   exists b; exists ofs; split; auto. exists co; auto.
 Qed.
 
@@ -1072,8 +1072,8 @@ Proof.
   intros. elim (H0 a m); auto.
   destruct (C a); auto; contradiction.
   destruct (C a); auto; contradiction.
-  red; intros. destruct (C a); auto. 
-  red; intros. destruct e1; auto. elim (H0 a m); auto. 
+  red; intros. destruct (C a); auto.
+  red; intros. destruct e1; auto. elim (H0 a m); auto.
 Qed.
 
 Lemma imm_safe_t_inv:
@@ -1086,7 +1086,7 @@ Lemma imm_safe_t_inv:
   end.
 Proof.
   destruct invert_expr_context as [A B].
-  intros. inv H. 
+  intros. inv H.
   auto.
   auto.
   assert (invert_expr_prop (C l) m).
@@ -1160,7 +1160,7 @@ Proof.
   induction rargs; simpl; intros.
   inv H. destruct tyargs; simpl in H0; inv H0. constructor.
   monadInv. inv H. simpl in H0. destruct p as [v1 t1]. destruct tyargs; try congruence. monadInv.
-  inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. 
+  inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto.
 Qed.
 
 Lemma sem_cast_arguments_complete:
@@ -1170,7 +1170,7 @@ Lemma sem_cast_arguments_complete:
 Proof.
   induction 1.
   exists (@nil (val * type)); auto.
-  destruct IHcast_arguments as [vtl [A B]]. 
+  destruct IHcast_arguments as [vtl [A B]].
   exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto.
 Qed.
 
@@ -1179,7 +1179,7 @@ Lemma topred_ok:
   reduction_ok k a m rd ->
   reducts_ok k a m (topred rd).
 Proof.
-  intros. unfold topred; split; simpl; intros. 
+  intros. unfold topred; split; simpl; intros.
   destruct H0; try contradiction. inv H0. exists a; exists k; auto.
   congruence.
 Qed.
@@ -1199,7 +1199,7 @@ Lemma wrong_kind_ok:
   k <> Cstrategy.expr_kind a ->
   reducts_ok k a m stuck.
 Proof.
-  intros. apply stuck_ok. red; intros. exploit Cstrategy.imm_safe_kind; eauto. 
+  intros. apply stuck_ok. red; intros. exploit Cstrategy.imm_safe_kind; eauto.
   eapply imm_safe_t_imm_safe; eauto.
 Qed.
 
@@ -1212,9 +1212,9 @@ Lemma not_invert_ok:
   end ->
   reducts_ok k a m stuck.
 Proof.
-  intros. apply stuck_ok. red; intros. 
-  exploit imm_safe_t_inv; eauto. destruct a; auto. 
-Qed. 
+  intros. apply stuck_ok. red; intros.
+  exploit imm_safe_t_inv; eauto. destruct a; auto.
+Qed.
 
 Lemma incontext_ok:
   forall k a m C res k' a',
@@ -1272,7 +1272,7 @@ Lemma incontext2_list_ok:
   reducts_ok RV a1 m res1 ->
   list_reducts_ok a2 m res2 ->
   is_val a1 = None \/ is_val_list a2 = None ->
-  reducts_ok RV (Ecall a1 a2 ty) m 
+  reducts_ok RV (Ecall a1 a2 ty) m
                (incontext2 (fun x => Ecall x a2 ty) res1
                            (fun x => Ecall a1 x ty) res2).
 Proof.
@@ -1280,7 +1280,7 @@ Proof.
   destruct (in_app_or _ _ _ H4).
   exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
   exploit H; eauto. intros [a'' [k'' [U [V W]]]].
-  exists a''; exists k''. split. eauto. rewrite V; auto. 
+  exists a''; exists k''. split. eauto. rewrite V; auto.
   exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
   exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
   exists a''; exists k''. split. eauto. rewrite V; auto.
@@ -1301,7 +1301,7 @@ Proof.
   destruct (in_app_or _ _ _ H3).
   exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
   exploit H; eauto. intros [a'' [k'' [U [V W]]]].
-  exists a''; exists k''. split. eauto. rewrite V; auto. 
+  exists a''; exists k''. split. eauto. rewrite V; auto.
   exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
   exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
   exists a''; exists k''. split. eauto. rewrite V; auto.
@@ -1312,7 +1312,7 @@ Qed.
 Lemma is_val_list_all_values:
   forall al vtl, is_val_list al = Some vtl -> exprlist_all_values al.
 Proof.
-  induction al; simpl; intros. auto. 
+  induction al; simpl; intros. auto.
   destruct (is_val r1) as [[v ty]|] eqn:?; try discriminate.
   destruct (is_val_list al) as [vtl'|] eqn:?; try discriminate.
   rewrite (is_val_inv _ _ _ Heqo). eauto.
@@ -1344,7 +1344,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (is_val a) as [[v ty'] | ] eqn:?.
   rewrite (is_val_inv _ _ _ Heqo).
   destruct v...
-  destruct ty'... 
+  destruct ty'...
   (* top struct *)
   destruct (ge.(genv_cenv)!i0) as [co|] eqn:?...
   destruct (field_offset ge f (co_members co)) as [delta|] eqn:?...
@@ -1353,7 +1353,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (ge.(genv_cenv)!i0) as [co|] eqn:?...
   apply topred_ok; auto. eapply red_field_union; eauto.
   (* in depth *)
-  eapply incontext_ok; eauto. 
+  eapply incontext_ok; eauto.
 (* Evalof *)
   destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo).
   (* top *)
@@ -1367,7 +1367,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* Ederef *)
   destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
-  destruct v... apply topred_ok; auto. apply red_deref; auto. 
+  destruct v... apply topred_ok; auto. apply red_deref; auto.
   (* depth *)
   eapply incontext_ok; eauto.
 (* Eaddrof *)
@@ -1377,31 +1377,31 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   (* depth *)
   eapply incontext_ok; eauto.
 (* unop *)
-  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct (sem_unary_operation op v ty' m) as [v'|] eqn:?...
-  apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. 
+  apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* binop *)
-  destruct (is_val a1) as [[v1 ty1] | ] eqn:?. 
+  destruct (is_val a1) as [[v1 ty1] | ] eqn:?.
   destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
-  rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). 
+  rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
   (* top *)
   destruct (sem_binary_operation ge op v1 ty1 v2 ty2 m) as [v|] eqn:?...
   apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor.
   (* depth *)
-  eapply incontext2_ok; eauto. 
-  eapply incontext2_ok; eauto. 
+  eapply incontext2_ok; eauto.
+  eapply incontext2_ok; eauto.
 (* cast *)
-  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct (sem_cast v ty' ty) as [v'|] eqn:?...
-  apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. 
+  apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* seqand *)
-  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'.
   apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor.
@@ -1409,7 +1409,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   (* depth *)
   eapply incontext_ok; eauto.
 (* seqor *)
-  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'.
   apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor.
@@ -1417,7 +1417,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   (* depth *)
   eapply incontext_ok; eauto.
 (* condition *)
-  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct (bool_val v ty' m) as [v'|] eqn:?...
   apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor.
@@ -1428,8 +1428,8 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* alignof *)
   apply topred_ok; auto. split. apply red_alignof. exists w; constructor.
 (* assign *)
-  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. 
-  destruct (is_val a2) as [[v2 ty2] | ] eqn:?. 
+  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?.
+  destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
   rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
   (* top *)
   destruct (type_eq ty1 ty)... subst ty1.
@@ -1442,9 +1442,9 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext2_ok; eauto.
   eapply incontext2_ok; eauto.
 (* assignop *)
-  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. 
-  destruct (is_val a2) as [[v2 ty2] | ] eqn:?. 
-  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). 
+  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?.
+  destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
+  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
   (* top *)
   destruct (type_eq ty1 ty)... subst ty1.
   destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
@@ -1455,7 +1455,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext2_ok; eauto.
   eapply incontext2_ok; eauto.
 (* postincr *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo). 
+  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo).
   (* top *)
   destruct (type_eq ty' ty)... subst ty'.
   destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
@@ -1465,22 +1465,22 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   (* depth *)
   eapply incontext_ok; eauto.
 (* comma *)
-  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct (type_eq (typeof a2) ty)... subst ty.
   apply topred_ok; auto. split. apply red_comma; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* call *)
-  destruct (is_val a) as [[vf tyf] | ] eqn:?.  
-  destruct (is_val_list rargs) as [vtl | ] eqn:?. 
+  destruct (is_val a) as [[vf tyf] | ] eqn:?.
+  destruct (is_val_list rargs) as [vtl | ] eqn:?.
   rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
   destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?...
   destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... 
+  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?...
   destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))...
-  apply topred_ok; auto. red. split; auto. eapply red_call; eauto. 
+  apply topred_ok; auto. red. split; auto. eapply red_call; eauto.
   eapply sem_cast_arguments_sound; eauto.
   apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
   apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
@@ -1491,31 +1491,31 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext2_list_ok; eauto.
   eapply incontext2_list_ok; eauto.
 (* builtin *)
-  destruct (is_val_list rargs) as [vtl | ] eqn:?. 
+  destruct (is_val_list rargs) as [vtl | ] eqn:?.
   exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... 
+  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?...
   destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?...
   exploit do_ef_external_sound; eauto. intros [EC PT].
-  apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto. 
+  apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto.
   eapply sem_cast_arguments_sound; eauto.
   exists w0; auto.
   apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
-  assert (x = vargs). 
+  assert (x = vargs).
     exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence.
   subst x. exploit do_ef_external_complete; eauto. congruence.
-  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. 
+  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
   exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence.
   (* depth *)
   eapply incontext_list_ok; eauto.
- 
+
 (* loc *)
   split; intros. tauto. simpl; congruence.
 (* paren *)
-  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct (sem_cast v ty' tycast) as [v'|] eqn:?...
-  apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. 
+  apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 
@@ -1529,7 +1529,7 @@ Qed.
 Lemma step_exprlist_val_list:
   forall m al, is_val_list al <> None -> step_exprlist al m = nil.
 Proof.
-  induction al; simpl; intros. 
+  induction al; simpl; intros.
   auto.
   destruct (is_val r1) as [[v1 ty1]|] eqn:?; try congruence.
   destruct (is_val_list al) eqn:?; try congruence.
@@ -1549,7 +1549,7 @@ Proof.
   rewrite H. rewrite dec_eq_true. econstructor; eauto.
 (* var global *)
   rewrite H; rewrite H0. econstructor; eauto.
-(* deref *) 
+(* deref *)
   econstructor; eauto.
 (* field struct *)
   rewrite H, H0; econstructor; eauto.
@@ -1564,7 +1564,7 @@ Lemma rred_topred:
 Proof.
   induction 1; simpl; intros.
 (* valof *)
-  rewrite dec_eq_true. 
+  rewrite dec_eq_true.
   rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). econstructor; eauto.
 (* addrof *)
   inv H. econstructor; eauto.
@@ -1591,7 +1591,7 @@ Proof.
   econstructor; eauto.
 (* assignop *)
   rewrite dec_eq_true. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0).
-  econstructor; eauto. 
+  econstructor; eauto.
 (* postincr *)
   rewrite dec_eq_true. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1).
   econstructor; eauto.
@@ -1601,7 +1601,7 @@ Proof.
   inv H0. rewrite H; econstructor; eauto.
 (* builtin *)
   exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]].
-  exploit do_ef_external_complete; eauto. intros C. 
+  exploit do_ef_external_complete; eauto. intros C.
   rewrite A. rewrite B. rewrite C. econstructor; eauto.
 Qed.
 
@@ -1624,7 +1624,7 @@ Lemma reducts_incl_trans:
   reducts_incl C' res2 res3 ->
   reducts_incl (fun x => C'(C x)) res1 res3.
 Proof.
-  unfold reducts_incl; intros. auto. 
+  unfold reducts_incl; intros. auto.
 Qed.
 
 Lemma reducts_incl_nil:
@@ -1756,11 +1756,11 @@ Proof.
   eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto.
   destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* call right *)
-  eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. 
+  eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto.
   destruct (is_val e1) as [[v1 ty1]|] eqn:?; eauto.
   destruct (is_val_list (C a)) as [vl|] eqn:?; eauto.
 (* builtin *)
-  eapply reducts_incl_trans with (C' := fun x => Ebuiltin ef tyargs x ty). apply step_exprlist_context. auto. 
+  eapply reducts_incl_trans with (C' := fun x => Ebuiltin ef tyargs x ty). apply step_exprlist_context. auto.
   destruct (is_val_list (C a)) as [vl|] eqn:?; eauto.
 (* comma *)
   eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto.
@@ -1785,18 +1785,18 @@ Lemma not_stuckred_imm_safe:
   forall m a k,
   (forall C, ~In (C, Stuckred) (step_expr k a m)) -> imm_safe_t k a m.
 Proof.
-  intros. generalize (step_expr_sound a k m). intros [A B]. 
+  intros. generalize (step_expr_sound a k m). intros [A B].
   destruct (step_expr k a m) as [|[C rd] res] eqn:?.
   specialize (B (refl_equal _)). destruct k.
   destruct a; simpl in B; try congruence. constructor.
   destruct a; simpl in B; try congruence. constructor.
   assert (NOTSTUCK: rd <> Stuckred).
     red; intros. elim (H C); subst rd; auto with coqlib.
-  exploit A. eauto with coqlib. intros [a' [k' [P [Q R]]]]. 
+  exploit A. eauto with coqlib. intros [a' [k' [P [Q R]]]].
   destruct k'; destruct rd; simpl in R; intuition.
   subst a. eapply imm_safe_t_lred; eauto.
-  subst a. destruct H1 as [w' PT]. eapply imm_safe_t_rred; eauto. 
-  subst. eapply imm_safe_t_callred; eauto. 
+  subst a. destruct H1 as [w' PT]. eapply imm_safe_t_rred; eauto.
+  subst. eapply imm_safe_t_callred; eauto.
 Qed.
 
 Lemma not_imm_safe_stuck_red:
@@ -1805,14 +1805,14 @@ Lemma not_imm_safe_stuck_red:
   ~imm_safe_t k a m ->
   exists C', In (C', Stuckred) (step_expr RV (C a) m).
 Proof.
-  intros. 
+  intros.
   assert (exists C', In (C', Stuckred) (step_expr k a m)).
     destruct (classic (exists C', In (C', Stuckred) (step_expr k a m))); auto.
-    elim H0. apply not_stuckred_imm_safe. apply not_ex_all_not. auto. 
+    elim H0. apply not_stuckred_imm_safe. apply not_ex_all_not. auto.
   destruct H1 as [C' IN].
-  specialize (step_expr_context _ _ _ H a m). unfold reducts_incl. 
+  specialize (step_expr_context _ _ _ H a m). unfold reducts_incl.
   intro.
-  exists (fun x => (C (C' x))). apply H1; auto. 
+  exists (fun x => (C (C' x))). apply H1; auto.
 Qed.
 
 (** Connections between [imm_safe_t] and [imm_safe] *)
@@ -1824,12 +1824,12 @@ Lemma imm_safe_imm_safe_t:
   exists C, exists a1, exists t, exists a1', exists m',
     context RV k C /\ a = C a1 /\ rred ge a1 m t a1' m' /\ forall w', ~possible_trace w t w'.
 Proof.
-  intros. inv H. 
+  intros. inv H.
   left. apply imm_safe_t_val.
   left. apply imm_safe_t_loc.
   left. eapply imm_safe_t_lred; eauto.
   destruct (classic (exists w', possible_trace w t w')) as [[w' A] | A].
-  left. eapply imm_safe_t_rred; eauto. 
+  left. eapply imm_safe_t_rred; eauto.
   right. exists C; exists e0; exists t; exists e'; exists m'; intuition. apply A; exists w'; auto.
   left. eapply imm_safe_t_callred; eauto.
 Qed.
@@ -1847,10 +1847,10 @@ Theorem not_imm_safe_t:
   Csem.step ge (ExprState f (C a) k e m) E0 Stuckstate \/ can_crash_world w (ExprState f (C a) k e m).
 Proof.
   intros. destruct (classic (imm_safe ge e K a m)).
-  exploit imm_safe_imm_safe_t; eauto. 
+  exploit imm_safe_imm_safe_t; eauto.
   intros [A | [C1 [a1 [t [a1' [m' [A [B [D E]]]]]]]]]. contradiction.
-  right. red. exists t; econstructor; split; auto. 
-  left. rewrite B. eapply step_rred with (C := fun x => C(C1 x)). eauto. eauto. 
+  right. red. exists t; econstructor; split; auto.
+  left. rewrite B. eapply step_rred with (C := fun x => C(C1 x)). eauto. eauto.
   left. left. eapply step_stuck; eauto.
 Qed.
 
@@ -1862,14 +1862,14 @@ Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l
   match l with
   | nil => (e,m)
   | (id, ty) :: l' =>
-      let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in 
+      let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in
       do_alloc_variables (PTree.set id (b1, ty) e) m1 l'
 end.
 
 Lemma do_alloc_variables_sound:
   forall l e m, alloc_variables ge e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)).
 Proof.
-  induction l; intros; simpl. 
+  induction l; intros; simpl.
   constructor.
   destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ge ty)) as [m1 b1] eqn:?; simpl.
   econstructor; eauto.
@@ -1879,12 +1879,12 @@ Lemma do_alloc_variables_complete:
   forall e1 m1 l e2 m2, alloc_variables ge e1 m1 l e2 m2 ->
   do_alloc_variables e1 m1 l = (e2, m2).
 Proof.
-  induction 1; simpl. 
+  induction 1; simpl.
   auto.
-  rewrite H; rewrite IHalloc_variables; auto. 
+  rewrite H; rewrite IHalloc_variables; auto.
 Qed.
 
-Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list val) 
+Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list val)
                           {struct l} : option mem :=
   match l, lv  with
   | nil, nil => Some m
@@ -1900,7 +1900,7 @@ Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type
 end.
 
 Lemma sem_bind_parameters_sound : forall w e m l lv m',
-  sem_bind_parameters w e m l lv = Some m' -> 
+  sem_bind_parameters w e m l lv = Some m' ->
   bind_parameters ge e m l lv m'.
 Proof.
    intros; functional induction (sem_bind_parameters w e m l lv); try discriminate.
@@ -1916,7 +1916,7 @@ Proof.
    rewrite H. rewrite dec_eq_true.
    assert (possible_trace w E0 w) by constructor.
    rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H2).
-   simpl. auto. 
+   simpl. auto.
 Qed.
 
 Inductive transition : Type := TR (rule: string) (t: trace) (S': state).
@@ -1946,7 +1946,7 @@ Definition do_step (w: world) (s: state) : list transition :=
             do b <- bool_val v ty m;
             ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m)
         | Kwhile1 x s k =>
-            do b <- bool_val v ty m; 
+            do b <- bool_val v ty m;
             if b
             then ret "step_while_true" (State f s (Kwhile2 x s k) e m)
             else ret "step_while_false" (State f Sskip k e m)
@@ -2018,7 +2018,7 @@ Definition do_step (w: world) (s: state) : list transition :=
       ret "step_return_0" (Returnstate Vundef (call_cont k) m')
   | State f (Sreturn (Some x)) k e m =>
       ret "step_return_1" (ExprState f x (Kreturn k) e m)
-  | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => 
+  | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m =>
       do m' <- Mem.free_list m (blocks_of_env ge e);
       ret "step_skip_call" (Returnstate Vundef k m')
 
@@ -2057,10 +2057,10 @@ Definition do_step (w: world) (s: state) : list transition :=
 Ltac myinv :=
   match goal with
   | [ |- In _ nil -> _ ] => intro X; elim X
-  | [ |- In _ (ret _ _) -> _ ] => 
+  | [ |- In _ (ret _ _) -> _ ] =>
         intro X; elim X; clear X;
         [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
-  | [ |- In _ (_ :: nil) -> _ ] => 
+  | [ |- In _ (_ :: nil) -> _ ] =>
         intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv]
   | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv
   | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv
@@ -2096,7 +2096,7 @@ Proof with try (left; right; econstructor; eauto; fail).
   generalize (step_expr_sound e w r RV m). unfold reducts_ok. intros [P Q].
   exploit P; eauto. intros [a' [k' [CTX [EQ RD]]]].
   unfold expr_final_state in A. simpl in A.
-  destruct k'; destruct rd; inv A; simpl in RD; try contradiction. 
+  destruct k'; destruct rd; inv A; simpl in RD; try contradiction.
   (* lred *)
   left; left; apply step_lred; auto.
   (* stuck lred *)
@@ -2111,11 +2111,11 @@ Proof with try (left; right; econstructor; eauto; fail).
   destruct fd; myinv.
   (* internal *)
   destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1] eqn:?.
-  myinv. left; right; apply step_internal_function with m1. auto. 
-  change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. 
+  myinv. left; right; apply step_internal_function with m1. auto.
+  change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp.
   apply do_alloc_variables_sound. eapply sem_bind_parameters_sound; eauto.
   (* external *)
-  destruct p as [[[w' tr] v] m']. myinv. left; right; constructor. 
+  destruct p as [[[w' tr] v] m']. myinv. left; right; constructor.
   eapply do_ef_external_sound; eauto.
 (* returnstate *)
   destruct k; myinv...
@@ -2126,10 +2126,10 @@ Qed.
 Remark estep_not_val:
   forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None.
 Proof.
-  intros. 
+  intros.
   assert (forall b from to C, context from to C -> (from = to /\ C = fun x => x) \/ is_val (C b) = None).
-    induction 1; simpl; auto. 
-  inv H. 
+    induction 1; simpl; auto.
+  inv H.
   destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
   destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
   destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
@@ -2141,7 +2141,7 @@ Theorem do_step_complete:
   possible_trace w t w' -> Csem.step ge S t S' -> exists rule, In (TR rule t S') (do_step w S).
 Proof with (unfold ret; eauto with coqlib).
   intros until w'; intros PT H.
-  destruct H. 
+  destruct H.
   (* Expression step *)
   inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL.
 (* lred *)
@@ -2170,7 +2170,7 @@ Proof with (unfold ret; eauto with coqlib).
   change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)).
   apply in_map.
   generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
-  intro. replace C with (fun x => C x). apply H2. 
+  intro. replace C with (fun x => C x). apply H2.
   rewrite STEP; unfold topred; auto with coqlib.
   apply extensionality; auto.
 (* stuck *)
@@ -2179,7 +2179,7 @@ Proof with (unfold ret; eauto with coqlib).
   simpl do_step. rewrite NOTVAL.
   exists "step_stuck".
   change (TR "step_stuck" E0 Stuckstate) with (expr_final_state f k e (C', Stuckred)).
-  apply in_map. auto. 
+  apply in_map. auto.
 
   (* Statement step *)
   inv H; simpl; econstructor...