Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.

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

10 files changed, 2275 insertions, 1783 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index d021a63c..8596ebfa 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -79,7 +79,7 @@ Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
   end.
 
 Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt :=
-  Sexpr (Estore chunk e1 (store_arg chunk e2)).
+  Sstore chunk e1 (store_arg chunk e2).
 
 Definition make_stackaddr (ofs: Z): expr :=
   Econst (Oaddrstack (Int.repr ofs)).
@@ -160,35 +160,22 @@ Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
   | Csharpminor.Eload chunk e =>
       do te <- transl_expr cenv e;
       OK (Eload chunk te)
-  | Csharpminor.Ecall sig e el =>
-      do te <- transl_expr cenv e;
-      do tel <- transl_exprlist cenv el;
-      OK (Ecall sig te tel)
   | Csharpminor.Econdition e1 e2 e3 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_expr cenv e2;
       do te3 <- transl_expr cenv e3;
       OK (Econdition te1 te2 te3)
-  | Csharpminor.Elet e1 e2 =>
-      do te1 <- transl_expr cenv e1;
-      do te2 <- transl_expr cenv e2;
-      OK (Elet te1 te2)
-  | Csharpminor.Eletvar n =>
-      OK (Eletvar n)
-  | Csharpminor.Ealloc e =>
-      do te <- transl_expr cenv e;
-      OK (Ealloc te)
-  end
+  end.
 
-with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist)
-                     {struct el}: res exprlist :=
+Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr)
+                     {struct el}: res (list expr) :=
   match el with
-  | Csharpminor.Enil =>
-      OK Enil
-  | Csharpminor.Econs e1 e2 =>
+  | nil =>
+      OK nil
+  | e1 :: e2 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_exprlist cenv e2;
-      OK (Econs te1 te2)
+      OK (te1 :: te2)
   end.
 
 (** Translation of statements.  Entirely straightforward. *)
@@ -198,14 +185,21 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt)
   match s with
   | Csharpminor.Sskip =>
       OK Sskip
-  | Csharpminor.Sexpr e =>
-      do te <- transl_expr cenv e; OK(Sexpr te)
   | Csharpminor.Sassign id e =>
       do te <- transl_expr cenv e; var_set cenv id te
   | Csharpminor.Sstore chunk e1 e2 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_expr cenv e2;
       OK (make_store chunk te1 te2)
+  | Csharpminor.Scall None sig e el =>
+      do te <- transl_expr cenv e;
+      do tel <- transl_exprlist cenv el;
+      OK (Scall None sig te tel)
+  | Csharpminor.Scall (Some id) sig e el =>
+      do te <- transl_expr cenv e;
+      do tel <- transl_exprlist cenv el;
+      do s <- var_set cenv id (Evar id);
+      OK (Sseq (Scall (Some id) sig te tel) s)
   | Csharpminor.Sseq s1 s2 =>
       do ts1 <- transl_stmt cenv s1;
       do ts2 <- transl_stmt cenv s2;
@@ -245,31 +239,26 @@ Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t :=
   | Csharpminor.Ebinop op e1 e2 =>
       Identset.union (addr_taken_expr e1) (addr_taken_expr e2)
   | Csharpminor.Eload chunk e => addr_taken_expr e
-  | Csharpminor.Ecall sig e el =>
-      Identset.union (addr_taken_expr e) (addr_taken_exprlist el)
   | Csharpminor.Econdition e1 e2 e3 =>
       Identset.union (addr_taken_expr e1) 
         (Identset.union (addr_taken_expr e2) (addr_taken_expr e3))
-  | Csharpminor.Elet e1 e2 =>
-      Identset.union (addr_taken_expr e1) (addr_taken_expr e2)
-  | Csharpminor.Eletvar n => Identset.empty
-  | Csharpminor.Ealloc e => addr_taken_expr e
-  end
+  end.
 
-with addr_taken_exprlist (e: Csharpminor.exprlist): Identset.t :=
+Fixpoint addr_taken_exprlist (e: list Csharpminor.expr): Identset.t :=
   match e with
-  | Csharpminor.Enil => Identset.empty
-  | Csharpminor.Econs e1 e2 =>
+  | nil => Identset.empty
+  | e1 :: e2 =>
       Identset.union (addr_taken_expr e1) (addr_taken_exprlist e2)
   end.
 
 Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t :=
   match s with
   | Csharpminor.Sskip => Identset.empty
-  | Csharpminor.Sexpr e => addr_taken_expr e
   | Csharpminor.Sassign id e => addr_taken_expr e
   | Csharpminor.Sstore chunk e1 e2 =>
       Identset.union (addr_taken_expr e1) (addr_taken_expr e2)
+  | Csharpminor.Scall optid sig e el =>
+      Identset.union (addr_taken_expr e) (addr_taken_exprlist el)
   | Csharpminor.Sseq s1 s2 =>
       Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2)
   | Csharpminor.Sifthenelse e s1 s2 =>
@@ -342,20 +331,13 @@ Definition build_global_compilenv (p: Csharpminor.program) : compilenv :=
 
 Fixpoint store_parameters
        (cenv: compilenv) (params: list (ident * memory_chunk))
-       {struct params} : stmt :=
+       {struct params} : res stmt :=
   match params with
-  | nil => Sskip
+  | nil => OK Sskip
   | (id, chunk) :: rem =>
-      match PMap.get id cenv with
-      | Var_local chunk =>
-          Sseq (Sassign id (make_cast chunk (Evar id)))
-               (store_parameters cenv rem)
-      | Var_stack_scalar chunk ofs =>
-          Sseq (make_store chunk (make_stackaddr ofs) (Evar id))
-               (store_parameters cenv rem)
-      | _ =>
-          Sskip (* should never happen *)
-      end
+      do s1 <- var_set cenv id (Evar id);
+      do s2 <- store_parameters cenv rem;
+      OK (Sseq s1 s2)
   end.
 
 (** Translation of a Csharpminor function.  We must check that the
@@ -368,12 +350,13 @@ Definition transl_function
   let (cenv, stacksize) := build_compilenv gce f in
   if zle stacksize Int.max_signed then
     do tbody <- transl_stmt cenv f.(Csharpminor.fn_body);
+    do sparams <- store_parameters cenv f.(Csharpminor.fn_params);
        OK (mkfunction
               (Csharpminor.fn_sig f)
               (Csharpminor.fn_params_names f)
               (Csharpminor.fn_vars_names f)
               stacksize
-              (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody))
+              (Sseq sparams tbody))
   else Error(msg "Cminorgen: too many local variables, stack size exceeded").
 
 Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): res fundef :=
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5bcb8801..ff10bb3e 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -12,6 +12,7 @@ Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Csharpminor.
+Require Import Op.
 Require Import Cminor.
 Require Import Cminorgen.
 
@@ -279,30 +280,6 @@ Qed.
   must be normalized with respect to the memory chunk of the variable,
   in the following sense. *)
 
-(*
-Definition val_normalized (chunk: memory_chunk) (v: val) : Prop :=
-  exists v0, v = Val.load_result chunk v0.
-
-Lemma load_result_idem:
-  forall chunk v,
-  Val.load_result chunk (Val.load_result chunk v) =
-  Val.load_result chunk v.
-Proof.
-  destruct chunk; destruct v; simpl; auto.
-  rewrite Int.cast8_signed_idem; auto.
-  rewrite Int.cast8_unsigned_idem; auto.
-  rewrite Int.cast16_signed_idem; auto.
-  rewrite Int.cast16_unsigned_idem; auto.
-  rewrite Float.singleoffloat_idem; auto.
-Qed.
-
-Lemma load_result_normalized:
-  forall chunk v,
-  val_normalized chunk v -> Val.load_result chunk v = v.
-Proof.
-  intros chunk v [v0 EQ]. rewrite EQ. apply load_result_idem. 
-Qed.
-*)
 Lemma match_env_store_local:
   forall f cenv e m1 m2 te sp lo hi id b chunk v tv,
   e!id = Some(b, Vscalar chunk) ->
@@ -796,21 +773,12 @@ Qed.
 
 (** * Correctness of Cminor construction functions *)
 
-Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr.
-
 Remark val_inject_val_of_bool:
   forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
 Proof.
   intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor.
 Qed.
 
-Remark val_inject_bool_of_val:
-  forall f v b tv,
-  val_inject f v tv -> Val.bool_of_val v b -> Val.bool_of_val tv b.
-Proof.
-  intros. inv H; inv H0; constructor; auto.
-Qed.
-
 Remark val_inject_eval_compare_null:
   forall f c i v,  
   eval_compare_null c i = Some v ->
@@ -822,6 +790,8 @@ Proof.
   discriminate.
 Qed.
 
+Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr.
+
 Ltac TrivialOp :=
   match goal with
   | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] =>
@@ -838,6 +808,17 @@ Ltac TrivialOp :=
   | _ => idtac
   end.
 
+Remark eval_compare_null_inv:
+  forall c i v,
+  eval_compare_null c i = Some v ->
+  i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue).
+Proof.
+  intros until v. unfold eval_compare_null.
+  predSpec Int.eq Int.eq_spec i Int.zero.
+  case c; intro EQ; simplify_eq EQ; intro; subst v; tauto.
+  congruence.
+Qed.
+
 (** Correctness of [transl_constant]. *)
 
 Lemma transl_constant_correct:
@@ -865,12 +846,12 @@ Proof.
   inv H; inv H0; simpl; TrivialOp.
   inv H; inv H0; simpl; TrivialOp.
   inv H; inv H0; simpl; TrivialOp.
-  inv H0; inv H. TrivialOp. 
+  inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp.
   inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
-  inv H; inv H0; simpl; TrivialOp.
+  inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
@@ -950,12 +931,11 @@ Qed.
   normalized according to the given memory chunk. *)
 
 Lemma make_cast_correct:
-  forall f sp le te tm1 a t tm2 v chunk tv,
-  eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 tv ->
+  forall f sp te tm a v tv chunk,
+  eval_expr tge sp te tm a tv ->
   val_inject f v tv ->
   exists tv',
-  eval_expr tge (Vptr sp Int.zero) le
-            te tm1 (make_cast chunk a) t tm2 tv'
+     eval_expr tge sp te tm (make_cast chunk a) tv'
   /\ val_inject f (Val.load_result chunk v) tv'.
 Proof.
   intros. destruct chunk; simpl make_cast.
@@ -983,46 +963,44 @@ Proof.
 Qed.
 
 Lemma make_stackaddr_correct:
-  forall sp le te tm ofs,
-  eval_expr tge (Vptr sp Int.zero) le
-            te tm (make_stackaddr ofs)
-            E0 tm (Vptr sp (Int.repr ofs)).
+  forall sp te tm ofs,
+  eval_expr tge (Vptr sp Int.zero) te tm
+            (make_stackaddr ofs) (Vptr sp (Int.repr ofs)).
 Proof.
   intros; unfold make_stackaddr.
-  econstructor. simpl. decEq. decEq.
+  eapply eval_Econst. simpl. decEq. decEq.
   rewrite Int.add_commut. apply Int.add_zero.
 Qed.
 
 Lemma make_globaladdr_correct:
-  forall sp le te tm id b,
+  forall sp te tm id b,
   Genv.find_symbol tge id = Some b ->
-  eval_expr tge (Vptr sp Int.zero) le
-            te tm (make_globaladdr id)
-            E0 tm (Vptr b Int.zero).
+  eval_expr tge (Vptr sp Int.zero) te tm
+            (make_globaladdr id) (Vptr b Int.zero).
 Proof.
   intros; unfold make_globaladdr.
-  econstructor. simpl. rewrite H. auto.
+  eapply eval_Econst. simpl. rewrite H. auto.
 Qed.
 
 (** Correctness of [make_store]. *)
 
 Lemma store_arg_content_inject:
-  forall f sp le te tm1 a t tm2 v va chunk,
-  eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 va ->
+  forall f sp te tm a v va chunk,
+  eval_expr tge sp te tm a va ->
   val_inject f v va ->
   exists vb,
-  eval_expr tge (Vptr sp Int.zero) le te tm1 (store_arg chunk a) t tm2 vb  
+     eval_expr tge sp te tm (store_arg chunk a) vb
   /\ val_content_inject f chunk v vb.
 Proof.
   intros. 
   assert (exists vb,
-    eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 vb  
+       eval_expr tge sp te tm a vb  
     /\ val_content_inject f chunk v vb).
   exists va; split. assumption. constructor. assumption.
   destruct a; simpl store_arg; trivial;
   destruct u; trivial;
   destruct chunk; trivial;
-  inv H; simpl in H12; inv H12;
+  inv H; simpl in H6; inv H6;
   econstructor; (split; [eauto|idtac]);
   destruct v1; simpl in H0; inv H0; try (constructor; constructor).
   apply val_content_inject_8. auto. apply Int.cast8_unsigned_idem.
@@ -1033,47 +1011,43 @@ Proof.
 Qed.
 
 Lemma make_store_correct:
-  forall f sp te tm1 addr tm2 tvaddr rhs tm3 tvrhs
-         chunk vrhs m3 vaddr m4 t1 t2,
-  eval_expr tge (Vptr sp Int.zero) nil
-            te tm1 addr t1 tm2 tvaddr ->
-  eval_expr tge (Vptr sp Int.zero) nil
-            te tm2 rhs t2 tm3 tvrhs ->
-  Mem.storev chunk m3 vaddr vrhs = Some m4 ->
-  mem_inject f m3 tm3 ->
+  forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m',
+  eval_expr tge sp te tm addr tvaddr ->
+  eval_expr tge sp te tm rhs tvrhs ->
+  Mem.storev chunk m vaddr vrhs = Some m' ->
+  mem_inject f m tm ->
   val_inject f vaddr tvaddr ->
   val_inject f vrhs tvrhs ->
-  exists tm4,
-  exec_stmt tge (Vptr sp Int.zero)
-            te tm1 (make_store chunk addr rhs)
-            (t1**t2) te tm4 Out_normal
-  /\ mem_inject f m4 tm4
-  /\ nextblock tm4 = nextblock tm3.
+  exists tm',
+  exec_stmt tge sp te tm (make_store chunk addr rhs)
+                E0 te tm' Out_normal
+  /\ mem_inject f m' tm'
+  /\ nextblock tm' = nextblock tm.
 Proof.
   intros. unfold make_store.
   exploit store_arg_content_inject. eexact H0. eauto. 
   intros [tv [EVAL VCINJ]].
   exploit storev_mapped_inject_1; eauto.
-  intros [tm4 [STORE MEMINJ]].
-  exists tm4. 
-  split. apply exec_Sexpr with tv. eapply eval_Estore; eauto. 
-  split. auto. 
+  intros [tm' [STORE MEMINJ]].
+  exists tm'.
+  split. eapply exec_Sstore; eauto. 
+  split. auto.
   unfold storev in STORE; destruct tvaddr; try discriminate.
   eapply nextblock_store; eauto.
 Qed.
 
-(** Correctness of the variable accessors [var_get], [var_set]
-  and [var_addr]. *)
+(** Correctness of the variable accessors [var_get], [var_addr],
+  and [var_set]. *)
 
 Lemma var_get_correct:
-  forall cenv id a f e te sp lo hi m cs tm b chunk v le,
+  forall cenv id a f e te sp lo hi m cs tm b chunk v,
   var_get cenv id = OK a ->
   match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
   mem_inject f m tm ->
   eval_var_ref prog e id b chunk ->
   load chunk m b 0 = Some v ->
   exists tv,
-    eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\
+    eval_expr tge (Vptr sp Int.zero) te tm a tv /\
     val_inject f v tv.
 Proof.
   unfold var_get; intros.
@@ -1093,7 +1067,7 @@ Proof.
     unfold loadv. eexact H3. 
   intros [tv [LOAD INJ]].
   exists tv; split. 
-  econstructor; eauto. eapply make_stackaddr_correct; eauto.
+  eapply eval_Eload; eauto. eapply make_stackaddr_correct; eauto.
   auto.
   (* var_global_scalar *)
   inversion H2; [congruence|subst]. 
@@ -1106,17 +1080,17 @@ Proof.
   generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13).
   intros [tv [LOAD INJ]].
   exists tv; split. 
-  econstructor; eauto. eapply make_globaladdr_correct; eauto.
+  eapply eval_Eload; eauto. eapply make_globaladdr_correct; eauto.
   auto.
 Qed.
 
 Lemma var_addr_correct:
-  forall cenv id a f e te sp lo hi m cs tm b le,
+  forall cenv id a f e te sp lo hi m cs tm b,
   match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
   var_addr cenv id = OK a ->
   eval_var_addr prog e id b ->
   exists tv,
-    eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\
+    eval_expr tge (Vptr sp Int.zero) te tm a tv /\
     val_inject f (Vptr b Int.zero) tv.
 Proof.
   unfold var_addr; intros.
@@ -1150,62 +1124,169 @@ Proof.
 Qed.
 
 Lemma var_set_correct:
-  forall cenv id rhs a f e te sp lo hi m2 cs tm2 tm1 tv b chunk v m3 t,
+  forall cenv id rhs a f e te sp lo hi m cs tm tv v m',
   var_set cenv id rhs = OK a ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 ->
-  eval_expr tge (Vptr sp Int.zero) nil te tm1 rhs t tm2 tv ->
+  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
+  eval_expr tge (Vptr sp Int.zero) te tm rhs tv ->
   val_inject f v tv ->
-  mem_inject f m2 tm2 ->
-  eval_var_ref prog e id b chunk ->
-  store chunk m2 b 0 v = Some m3 ->
-  exists te3, exists tm3,
-    exec_stmt tge (Vptr sp Int.zero) te tm1 a t te3 tm3 Out_normal /\
-    mem_inject f m3 tm3 /\
-    match_callstack f (mkframe cenv e te3 sp lo hi :: cs) m3.(nextblock) tm3.(nextblock) m3.
+  mem_inject f m tm ->
+  exec_assign prog e m id v m' ->
+  exists te', exists tm',
+    exec_stmt tge (Vptr sp Int.zero) te tm a E0 te' tm' Out_normal /\
+    mem_inject f m' tm' /\
+    match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m' /\
+    (forall id', id' <> id -> te'!id' = te!id').
 Proof.
   unfold var_set; intros.
-  assert (NEXTBLOCK: nextblock m3 = nextblock m2).
+  inv H4. 
+  assert (NEXTBLOCK: nextblock m' = nextblock m).
     eapply nextblock_store; eauto.
-  inversion H0. subst.
-  assert (match_var f id e m2 te sp cenv!!id). inversion H19; auto.
-  inversion H6; subst; rewrite <- H7 in H; inversion H; subst; clear H.
+  inversion H0; subst.
+  assert (match_var f id e m te sp cenv!!id). inversion H19; auto.
+  inv H4; rewrite <- H7 in H; inv H.
   (* var_local *)
-  inversion H4; [subst|congruence]. 
-  assert (b0 = b). congruence. subst b0.
-  assert (chunk0 = chunk). congruence. subst chunk0.
+  inversion H5; [subst|congruence]. 
+  assert (b0 = b) by congruence. subst b0.
+  assert (chunk0 = chunk) by congruence. subst chunk0.
   exploit make_cast_correct; eauto.  
   intros [tv' [EVAL INJ]].
-  exists (PTree.set id tv' te); exists tm2.
+  exists (PTree.set id tv' te); exists tm.
   split. eapply exec_Sassign. eauto. 
   split. eapply store_unmapped_inject; eauto. 
-  rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto.
+  split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto.
+  intros. apply PTree.gso; auto.
   (* var_stack_scalar *)
+  inversion H5; [subst|congruence].
+  assert (b0 = b) by congruence. subst b0.
+  assert (chunk0 = chunk) by congruence. subst chunk0.
+  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
+  exploit make_store_correct.
+    eapply make_stackaddr_correct.
+    eauto. eauto. eauto. eauto. eauto. 
+  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
+  exists te; exists tm'.
+  split. auto. split. auto.  
+  split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
+  eapply match_callstack_mapped; eauto. 
+  inversion H9; congruence.
+  auto.
+  (* var_global_scalar *)
+  inversion H5; [congruence|subst]. 
+  assert (chunk0 = chunk) by congruence. subst chunk0.  
+  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
+  assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
+  inversion H12. destruct (mg_symbols0 _ _ H4) as [A B].
+  exploit make_store_correct.
+    eapply make_globaladdr_correct; eauto.
+    eauto. eauto. eauto. eauto. eauto. 
+  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
+  exists te; exists tm'.
+  split. auto. split. auto. 
+  split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
+  eapply match_callstack_mapped; eauto. congruence.
+  auto.
+Qed.
+
+Lemma match_env_extensional':
+  forall f cenv e m te1 sp lo hi,
+  match_env f cenv e m te1 sp lo hi ->
+  forall te2,
+  (forall id, 
+     match cenv!!id with
+     | Var_local _ => te2!id = te1!id
+     | _ => True
+     end) ->
+  match_env f cenv e m te2 sp lo hi.
+Proof.
+  induction 1; intros; econstructor; eauto.
+  intros. generalize (me_vars0 id); intro. 
+  inversion H0; econstructor; eauto.
+  generalize (H id). rewrite <- H1. congruence. 
+Qed.
+
+
+Lemma match_callstack_extensional:
+  forall f cenv e te1 te2 sp lo hi cs bound tbound m,
+  (forall id, 
+     match cenv!!id with
+     | Var_local _ => te2!id = te1!id
+     | _ => True
+     end) ->
+  match_callstack f (mkframe cenv e te1 sp lo hi :: cs) bound tbound m ->
+  match_callstack f (mkframe cenv e te2 sp lo hi :: cs) bound tbound m.
+Proof.
+  intros. inv H0. constructor; auto. 
+  apply match_env_extensional' with te1; auto.
+Qed.
+
+Lemma var_set_self_correct:
+  forall cenv id a f e te sp lo hi m cs tm tv v m',
+  var_set cenv id (Evar id) = OK a ->
+  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
+  val_inject f v tv ->
+  mem_inject f m tm ->
+  exec_assign prog e m id v m' ->
+  exists te', exists tm',
+    exec_stmt tge (Vptr sp Int.zero) (PTree.set id tv te) tm a E0 te' tm' Out_normal /\
+    mem_inject f m' tm' /\
+    match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m'.
+Proof.
+  unfold var_set; intros.
+  inv H3. 
+  assert (NEXTBLOCK: nextblock m' = nextblock m).
+    eapply nextblock_store; eauto.
+  inversion H0; subst.
+  assert (EVAR: eval_expr tge (Vptr sp Int.zero) (PTree.set id tv te) tm (Evar id) tv).
+    constructor. apply PTree.gss.
+  assert (match_var f id e m te sp cenv!!id). inversion H18; auto.
+  inv H3; rewrite <- H6 in H; inv H.
+  (* var_local *)
   inversion H4; [subst|congruence]. 
-  assert (b0 = b). congruence. subst b0.
-  assert (chunk0 = chunk). congruence. subst chunk0.  
-  assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption.
+  assert (b0 = b) by congruence. subst b0.
+  assert (chunk0 = chunk) by congruence. subst chunk0.
+  exploit make_cast_correct; eauto. 
+  intros [tv' [EVAL INJ]].
+  exists (PTree.set id tv' (PTree.set id tv te)); exists tm.
+  split. eapply exec_Sassign. eauto. 
+  split. eapply store_unmapped_inject; eauto. 
+  rewrite NEXTBLOCK.
+  apply match_callstack_extensional with (PTree.set id tv' te).
+  intros. destruct (cenv!!id0); auto. 
+  repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. 
+  eapply match_callstack_store_local; eauto.
+  (* var_stack_scalar *)
+  inversion H4; [subst|congruence].
+  assert (b0 = b) by congruence. subst b0.
+  assert (chunk0 = chunk) by congruence. subst chunk0.
+  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
   exploit make_store_correct.
     eapply make_stackaddr_correct.
     eauto. eauto. eauto. eauto. eauto. 
-  rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]].
-  exists te; exists tm3.
+  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
+  exists (PTree.set id tv te); exists tm'.
   split. auto. split. auto.  
   rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
+  apply match_callstack_extensional with te.
+  intros. caseEq (cenv!!id0); intros; auto.
+  rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto.
   eapply match_callstack_mapped; eauto. 
-  inversion H9; congruence.
+  inversion H8; congruence.
   (* var_global_scalar *)
   inversion H4; [congruence|subst]. 
-  assert (chunk0 = chunk). congruence. subst chunk0.  
-  assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption.
+  assert (chunk0 = chunk) by congruence. subst chunk0.  
+  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
   assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inversion H13. destruct (mg_symbols0 _ _ H10) as [A B].
+  inversion H11. destruct (mg_symbols0 _ _ H3) as [A B].
   exploit make_store_correct.
     eapply make_globaladdr_correct; eauto.
     eauto. eauto. eauto. eauto. eauto. 
-  rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]].
-  exists te; exists tm3.
+  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
+  exists (PTree.set id tv te); exists tm'.
   split. auto. split. auto. 
   rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
+  apply match_callstack_extensional with te.
+  intros. caseEq (cenv!!id0); intros; auto.
+  rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto.
   eapply match_callstack_mapped; eauto. congruence.
 Qed.
 
@@ -1501,79 +1582,42 @@ Qed.
 Lemma store_parameters_correct:
   forall e m1 params vl m2,
   bind_parameters e m1 params vl m2 ->
-  forall f te1 cenv sp lo hi cs tm1,
+  forall s f te1 cenv sp lo hi cs tm1,
   vars_vals_match f params vl te1 ->
   list_norepet (List.map (@fst ident memory_chunk) params) ->
   mem_inject f m1 tm1 ->
   match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 ->
+  store_parameters cenv params = OK s ->
   exists te2, exists tm2,
      exec_stmt tge (Vptr sp Int.zero)
-                   te1 tm1 (store_parameters cenv params)
+                   te1 tm1 s
                 E0 te2 tm2 Out_normal
   /\ mem_inject f m2 tm2
   /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2.
 Proof.
   induction 1.
   (* base case *)
-  intros; simpl. exists te1; exists tm1. split. constructor. tauto.
+  intros; simpl. monadInv H3.
+  exists te1; exists tm1. split. constructor. tauto.
   (* inductive case *)
-  intros until tm1.  intros VVM NOREPET MINJ MATCH. simpl.
+  intros until tm1.  intros VVM NOREPET MINJ MATCH STOREP.
+  monadInv STOREP.
   inversion VVM. subst f0 id0 chunk0 vars v vals te.
-  inversion MATCH. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m0.
-  inversion H18.
   inversion NOREPET. subst hd tl.
-  assert (NEXT: nextblock m1 = nextblock m).
-    eapply nextblock_store; eauto.
-  generalize (me_vars0 id). intro. inversion H2; subst.
-  (* cenv!!id = Var_local chunk *)
-  assert (b0 = b). congruence. subst b0.
-  assert (chunk0 = chunk). congruence. subst chunk0.
-  assert (v' = tv). congruence. subst v'.
-  exploit make_cast_correct.
-    apply eval_Evar with (id := id). eauto.
-    eexact H10. 
-  intros [tv' [EVAL1 VINJ1]].
-  set (te2 := PTree.set id tv' te1).
-  assert (VVM2: vars_vals_match f params vl te2).
+  exploit var_set_correct; eauto.
+    constructor; auto.
+    econstructor; eauto.
+    econstructor; eauto.
+  intros [te2 [tm2 [EXEC1 [MINJ1 [MATCH1 UNCHANGED1]]]]].
+  assert (vars_vals_match f params vl te2).
     apply vars_vals_match_extensional with te1; auto.
-    intros. unfold te2; apply PTree.gso. red; intro; subst id0.
-    elim H4. change id with (fst (id, lv)). apply List.in_map; auto.
-  exploit store_unmapped_inject; eauto. intro MINJ2.
-  exploit match_callstack_store_local; eauto. 
-  fold te2; rewrite <- NEXT; intro MATCH2.
+    intros. apply UNCHANGED1. red; intro; subst id0.
+    elim H4. change id with (fst (id, lv)). apply List.in_map. auto.
   exploit IHbind_parameters; eauto.
-  intros [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]].
-  exists te3; exists tm3. 
-  (* execution *)
-  split. apply exec_Sseq_continue with E0 te2 tm1 E0. 
-  unfold te2. constructor. eassumption. assumption. traceEq.
-  (* meminj & match_callstack *)
-  tauto.
-
-  (* cenv!!id = Var_stack_scalar *)
-  assert (b0 = b). congruence. subst b0.
-  assert (chunk0 = chunk). congruence. subst chunk0.
-  exploit make_store_correct.
-    eapply make_stackaddr_correct.
-    apply eval_Evar with (id := id).
-    eauto. 2:eauto. 2:eauto. unfold storev; eexact H0. eauto.
-  intros [tm2 [EVAL3 [MINJ2 NEXT1]]].
-  exploit match_callstack_mapped.
-    eexact MATCH. 2:eauto. inversion H7. congruence. 
-  rewrite <- NEXT; rewrite <- NEXT1; intro MATCH2.
-  exploit IHbind_parameters; eauto.
-  intros  [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]].
+  intros [te3 [tm3 [EXEC2 [MINJ2 MATCH2]]]].
   exists te3; exists tm3.
-  (* execution *)
-  split. apply exec_Sseq_continue with (E0**E0) te1 tm2 E0. 
-  auto. assumption. traceEq.
-  (* meminj & match_callstack *)
-  tauto.
-
-  (* Impossible cases on cenv!!id *)
-  congruence. 
-  congruence.
-  congruence.
+  split. econstructor; eauto.
+  auto.
 Qed.
 
 Lemma vars_vals_match_holds_1:
@@ -1634,7 +1678,7 @@ Qed.
   and initialize the blocks corresponding to function parameters). *)
 
 Lemma function_entry_ok:
-  forall fn m e m1 lb vargs m2 f cs tm cenv sz tm1 sp tvargs,
+  forall fn m e m1 lb vargs m2 f cs tm cenv sz tm1 sp tvargs s,
   alloc_variables empty_env m (fn_variables fn) e m1 lb ->
   bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 ->
   match_callstack f cs m.(nextblock) tm.(nextblock) m ->
@@ -1646,9 +1690,10 @@ Lemma function_entry_ok:
   val_list_inject f vargs tvargs ->
   mem_inject f m tm ->
   list_norepet (fn_params_names fn ++ fn_vars_names fn) ->
+  store_parameters cenv fn.(Csharpminor.fn_params) = OK s ->
   exists f2, exists te2, exists tm2,
      exec_stmt tge (Vptr sp Int.zero)
-               te tm1 (store_parameters cenv fn.(Csharpminor.fn_params))
+               te tm1 s
             E0 te2 tm2 Out_normal
   /\ mem_inject f2 m2 tm2
   /\ inject_incr f f2
@@ -1669,7 +1714,7 @@ Proof.
   exploit store_parameters_correct.
     eauto. eauto. 
     unfold fn_params_names in H7. eapply list_norepet_append_left; eauto.
-    eexact MINJ1. eauto. 
+    eexact MINJ1. eauto. eauto. 
   intros [te2 [tm2 [EXEC [MINJ2 MATCH2]]]].
   exists f1; exists te2; exists tm2.
   split; auto. split; auto. split; auto. split; auto.
@@ -1681,64 +1726,101 @@ Qed.
 (** The proof of semantic preservation uses simulation diagrams of the
   following form:
 <<
-     le, e, m1, a --------------- tle, sp, te1, tm1, ta
-          |                                |
+       e, m1, s ----------------- sp, te1, tm1, ts
           |                                |
+         t|                                |t
           v                                v
-     le, e, m2, v --------------- tle, sp, te2, tm2, tv
+       e, m2, out --------------- sp, te2, tm2, tout
 >>
-  where [ta] is the Cminor expression obtained by translating the
-  Csharpminor expression [a].  The left vertical arrow is an evaluation
-  of a Csharpminor expression.  The right vertical arrow is an evaluation
-  of a Cminor expression.  The precondition (top vertical bar)
+  where [ts] is the Cminor statement obtained by translating the
+  Csharpminor statement [s].  The left vertical arrow is an execution
+  of a Csharpminor statement.  The right vertical arrow is an execution
+  of a Cminor statement.  The precondition (top vertical bar)
   includes a [mem_inject] relation between the memory states [m1] and [tm1],
-  a [val_list_inject] relation between the let environments [le] and [tle],
   and a [match_callstack] relation for any callstack having
   [e], [te1], [sp] as top frame.  The postcondition (bottom vertical bar)
   is the existence of a memory injection [f2] that extends the injection
   [f1] we started with, preserves the [match_callstack] relation for
   the transformed callstack at the final state, and validates a
-  [val_inject] relation between the result values [v] and [tv].
+  [outcome_inject] relation between the outcomes [out] and [tout].
+*)
 
-  We capture these diagrams by the following predicates, parameterized
-  over the Csharpminor executions, which will serve as induction
-  hypotheses in the proof of simulation. *)
+(** ** Semantic preservation for expressions *)
 
-Definition eval_expr_prop
-    (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (t: trace) (m2: mem) (v: val) : Prop :=
-  forall cenv ta f1 tle te tm1 sp lo hi cs
-  (TR: transl_expr cenv a = OK ta)
-  (LINJ: val_list_inject f1 le tle)
-  (MINJ: mem_inject f1 m1 tm1)
-  (MATCH: match_callstack f1
-           (mkframe cenv e te sp lo hi :: cs)
-           m1.(nextblock) tm1.(nextblock) m1),
-  exists f2, exists tm2, exists tv,
-     eval_expr tge (Vptr sp Int.zero) tle te tm1 ta t tm2 tv
-  /\ val_inject f2 v tv
-  /\ mem_inject f2 m2 tm2
-  /\ inject_incr f1 f2
-  /\ match_callstack f2
-        (mkframe cenv e te sp lo hi :: cs)
-        m2.(nextblock) tm2.(nextblock) m2.
+Remark bool_of_val_inject:
+  forall f v tv b,
+  Val.bool_of_val v b -> val_inject f v tv -> Val.bool_of_val tv b.
+Proof.
+  intros. inv H0; inv H; constructor; auto.
+Qed.
 
-Definition eval_exprlist_prop
-    (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (t: trace) (m2: mem) (vl: list val) : Prop :=
-  forall cenv tal f1 tle te tm1 sp lo hi cs
-  (TR: transl_exprlist cenv al = OK tal)
-  (LINJ: val_list_inject f1 le tle)
-  (MINJ: mem_inject f1 m1 tm1)
-  (MATCH: match_callstack f1
-           (mkframe cenv e te sp lo hi :: cs)
-           m1.(nextblock) tm1.(nextblock) m1),
-  exists f2, exists tm2, exists tvl,
-     eval_exprlist tge (Vptr sp Int.zero) tle te tm1 tal t tm2 tvl
-  /\ val_list_inject f2 vl tvl
-  /\ mem_inject f2 m2 tm2
-  /\ inject_incr f1 f2
-  /\ match_callstack f2
-        (mkframe cenv e te sp lo hi :: cs)
-        m2.(nextblock) tm2.(nextblock) m2.
+Lemma transl_expr_correct:
+  forall f m tm cenv e te sp lo hi cs
+    (MINJ: mem_inject f m tm)
+    (MATCH: match_callstack f
+             (mkframe cenv e te sp lo hi :: cs)
+             m.(nextblock) tm.(nextblock) m),
+  forall a v,
+  Csharpminor.eval_expr prog e m a v ->
+  forall ta
+    (TR: transl_expr cenv a = OK ta),
+  exists tv,
+     eval_expr tge (Vptr sp Int.zero) te tm ta tv
+  /\ val_inject f v tv.
+Proof.
+  induction 3; intros; simpl in TR; try (monadInv TR).
+  (* Evar *)
+  eapply var_get_correct; eauto.
+  (* Eaddrof *)
+  eapply var_addr_correct; eauto.
+  (* Econst *)
+  exploit transl_constant_correct; eauto. intros [tv [A B]].
+  exists tv; split. constructor; eauto. eauto.
+  (* Eunop *)
+  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
+  exploit eval_unop_compat; eauto. intros [tv [EVAL INJ]].
+  exists tv; split. econstructor; eauto. auto.
+  (* Ebinop *)
+  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
+  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]].
+  exploit eval_binop_compat; eauto. intros [tv [EVAL INJ]].
+  exists tv; split. econstructor; eauto. auto.
+  (* Eload *)
+  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
+  exploit loadv_inject; eauto. intros [tv [LOAD INJ]].
+  exists tv; split. econstructor; eauto. auto.
+  (* Econdition *)
+  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
+  assert (transl_expr cenv (if vb1 then b else c) =
+          OK (if vb1 then x0 else x1)).
+    destruct vb1; auto.
+  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]].
+  exists tv2; split. eapply eval_Econdition; eauto.
+  eapply bool_of_val_inject; eauto. auto.
+Qed.
+
+Lemma transl_exprlist_correct:
+  forall f m tm cenv e te sp lo hi cs
+    (MINJ: mem_inject f m tm)
+    (MATCH: match_callstack f
+             (mkframe cenv e te sp lo hi :: cs)
+             m.(nextblock) tm.(nextblock) m),
+  forall a v,
+  Csharpminor.eval_exprlist prog e m a v ->
+  forall ta
+    (TR: transl_exprlist cenv a = OK ta),
+  exists tv,
+     eval_exprlist tge (Vptr sp Int.zero) te tm ta tv
+  /\ val_list_inject f v tv.
+Proof.
+  induction 3; intros; monadInv TR.
+  exists (@nil val); split. constructor. constructor.
+  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]].
+  exploit IHeval_exprlist; eauto. intros [tv2 [EVAL2 VINJ2]].
+  exists (tv1 :: tv2); split. constructor; auto. constructor; auto.
+Qed.
+
+(** ** Semantic preservation for statements and functions *)
 
 Definition eval_funcall_prop
     (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop :=
@@ -1783,316 +1865,12 @@ Definition exec_stmt_prop
         (mkframe cenv e te2 sp lo hi :: cs)
         m2.(nextblock) tm2.(nextblock) m2.
 
+(* Check (Csharpminor.eval_funcall_ind2 prog eval_funcall_prop exec_stmt_prop). *)
+
 (** There are as many cases in the inductive proof as there are evaluation
   rules in the Csharpminor semantics.  We treat each case as a separate
   lemma. *)
 
-Lemma transl_expr_Evar_correct:
-   forall (le : Csharpminor.letenv)
-     (e : Csharpminor.env) (m : mem) (id : positive)
-     (b : block) (chunk : memory_chunk) (v : val),
-   eval_var_ref prog e id b chunk ->
-   load chunk m b 0 = Some v ->
-   eval_expr_prop le e m (Csharpminor.Evar id) E0 m v.
-Proof.
-  intros; red; intros. unfold transl_expr in TR.
-  exploit var_get_correct; eauto.
-  intros [tv [EVAL VINJ]].
-  exists f1; exists tm1; exists tv; intuition eauto.
-Qed.
-
-Lemma transl_expr_Eaddrof_correct:
-   forall (le : Csharpminor.letenv)
-     (e : Csharpminor.env) (m : mem) (id : positive)
-     (b : block),
-   eval_var_addr prog e id b ->
-   eval_expr_prop le e m (Eaddrof id) E0 m (Vptr b Int.zero).
-Proof.
-  intros; red; intros. simpl in TR. 
-  exploit var_addr_correct; eauto.
-  intros [tv [EVAL VINJ]].
-  exists f1; exists tm1; exists tv. intuition eauto.
-Qed.
-
-Lemma transl_expr_Econst_correct:
-  forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-         (cst : Csharpminor.constant) (v : val),
-  Csharpminor.eval_constant cst = Some v ->
-  eval_expr_prop le e m (Csharpminor.Econst cst) E0 m v.
-Proof.
-  intros; red; intros; monadInv TR.
-  exploit transl_constant_correct; eauto.
-  intros [tv [EVAL VINJ]].
-  exists f1; exists tm1; exists tv. intuition eauto. 
-  constructor; eauto.
-Qed.
-
-Lemma transl_expr_Eunop_correct:
-  forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-         (op : unary_operation) (a : Csharpminor.expr) (t : trace)
-         (m1 : mem) (v1 v : val),
-  Csharpminor.eval_expr prog le e m a t m1 v1 ->
-  eval_expr_prop le e m a t m1 v1 ->
-  Csharpminor.eval_unop op v1 = Some v ->
-  eval_expr_prop le e m (Csharpminor.Eunop op a) t m1 v.
-Proof.
-  intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
-  exploit eval_unop_compat; eauto. intros [tv [EVAL VINJ]].
-  exists f2; exists tm2; exists tv; intuition.
-  econstructor; eauto.
-Qed.
-
-Lemma transl_expr_Ebinop_correct:
-  forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-         (op : binary_operation) (a1 a2 : Csharpminor.expr) (t1 : trace)
-         (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem) (v2 : val)
-         (t : trace) (v : val),
-  Csharpminor.eval_expr prog le e m a1 t1 m1 v1 ->
-  eval_expr_prop le e m a1 t1 m1 v1 ->
-  Csharpminor.eval_expr prog le e m1 a2 t2 m2 v2 ->
-  eval_expr_prop le e m1 a2 t2 m2 v2 ->
-  Csharpminor.eval_binop op v1 v2 m2 = Some v ->
-  t = t1 ** t2 ->
-  eval_expr_prop le e m (Csharpminor.Ebinop op a1 a2) t m2 v.
-Proof.
-  intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
-  exploit H2.
-    eauto. eapply val_list_inject_incr; eauto. eauto. eauto.  
-  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exploit eval_binop_compat.
-    eauto. eapply val_inject_incr; eauto. eauto. eauto. 
-  intros [tv [EVAL VINJ]].
-  exists f3; exists tm3; exists tv; intuition.
-  econstructor; eauto.
-  eapply inject_incr_trans; eauto.
-Qed.
-
-Lemma transl_expr_Eload_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-     (chunk : memory_chunk) (a : Csharpminor.expr) (t: trace) (m1 : mem)
-     (v1 v : val),
-   Csharpminor.eval_expr prog le e m a t m1 v1 ->
-   eval_expr_prop le e m a t m1 v1 ->
-   loadv chunk m1 v1 = Some v ->
-   eval_expr_prop le e m (Csharpminor.Eload chunk a) t m1 v.
-Proof.
-  intros; red; intros.
-  monadInv TR. 
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
-  exploit loadv_inject; eauto. 
-  intros [tv [TLOAD VINJ]].
-  exists f2; exists tm2; exists tv.
-  intuition.
-  econstructor; eauto.
-Qed.
-
-Lemma transl_expr_Ecall_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-     (sig : signature) (a : Csharpminor.expr) (bl : Csharpminor.exprlist)
-     (t1: trace) (m1: mem) (t2: trace) (m2: mem) (t3: trace) (m3: mem) 
-     (vf : val) (vargs : list val) (vres : val)
-     (f : Csharpminor.fundef) (t: trace),
-   Csharpminor.eval_expr prog le e m a t1 m1 vf ->
-   eval_expr_prop le e m a t1 m1 vf ->
-   Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vargs ->
-   eval_exprlist_prop le e m1 bl t2 m2 vargs ->
-   Genv.find_funct ge vf = Some f ->
-   Csharpminor.funsig f = sig ->
-   Csharpminor.eval_funcall prog m2 f vargs t3 m3 vres ->
-   eval_funcall_prop m2 f vargs t3 m3 vres ->
-   t = t1 ** t2 ** t3 ->
-   eval_expr_prop le e m (Csharpminor.Ecall sig a bl) t m3 vres.
-Proof.
-  intros;red;intros. monadInv TR. 
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
-  exploit H2.
-    eauto. eapply val_list_inject_incr; eauto. eauto. eauto. 
-  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
-  assert (tv1 = vf).
-    elim (Genv.find_funct_inv H3). intros bf VF. rewrite VF in H3.
-    rewrite Genv.find_funct_find_funct_ptr in H3. 
-    generalize (Genv.find_funct_ptr_negative H3). intro.
-    assert (match_globalenvs f2). eapply match_callstack_match_globalenvs; eauto.
-    generalize (mg_functions _ H7 _ H4). intro.
-    rewrite VF in VINJ1. inversion VINJ1. subst vf. 
-    decEq. congruence. 
-    subst ofs2. replace x1 with 0. reflexivity. congruence.
-  subst tv1. elim (functions_translated _ _ H3). intros tf [FIND TRF].
-  exploit H6; eauto.
-  intros [f4 [tm4 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]].
-  exists f4; exists tm4; exists tres. intuition.
-  eapply eval_Ecall; eauto. 
-  apply sig_preserved; auto.
-  apply inject_incr_trans with f2; auto. 
-  apply inject_incr_trans with f3; auto.
-Qed.
-
-Lemma transl_expr_Econdition_true_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-     (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val)
-     (t2: trace) (m2 : mem) (v2 : val) (t: trace),
-   Csharpminor.eval_expr prog le e m a t1 m1 v1 ->
-   eval_expr_prop le e m a t1 m1 v1 ->
-   Val.is_true v1 ->
-   Csharpminor.eval_expr prog le e m1 b t2 m2 v2 ->
-   eval_expr_prop le e m1 b t2 m2 v2 ->
-   t = t1 ** t2 ->
-   eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2.
-Proof.
-  intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
-  exploit H3.
-    eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
-  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exists f3; exists tm3; exists tv2.
-  intuition.
-  eapply eval_Econdition with (b1 := true); eauto. 
-    eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; eauto.
-  eapply inject_incr_trans; eauto.
-Qed.
-
-Lemma transl_expr_Econdition_false_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-     (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val)
-     (t2: trace) (m2 : mem) (v2 : val) (t: trace),
-   Csharpminor.eval_expr prog le e m a t1 m1 v1 ->
-   eval_expr_prop le e m a t1 m1 v1 ->
-   Val.is_false v1 ->
-   Csharpminor.eval_expr prog le e m1 c t2 m2 v2 ->
-   eval_expr_prop le e m1 c t2 m2 v2 ->
-   t = t1 ** t2 ->
-   eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2.
-Proof.
-  intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
-  exploit H3.
-    eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
-  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exists f3; exists tm3; exists tv2.
-  intuition.
-  eapply eval_Econdition with (b1 := false); eauto. 
-    eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; eauto.
-  eapply inject_incr_trans; eauto.
-Qed.
-
-Lemma transl_expr_Elet_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-     (a b : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val)
-     (t2: trace) (m2 : mem) (v2 : val) (t: trace),
-   Csharpminor.eval_expr prog le e m a t1 m1 v1 ->
-   eval_expr_prop le e m a t1 m1 v1 ->
-   Csharpminor.eval_expr prog (v1 :: le) e m1 b t2 m2 v2 ->
-   eval_expr_prop (v1 :: le) e m1 b t2 m2 v2 ->
-   t = t1 ** t2 ->
-   eval_expr_prop le e m (Csharpminor.Elet a b) t m2 v2.
-Proof.
-  intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
-  exploit H2.
-    eauto. 
-    constructor. eauto. eapply val_list_inject_incr; eauto.
-    eauto. eauto.
-  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exists f3; exists tm3; exists tv2.
-  intuition.
-  eapply eval_Elet; eauto.
-  eapply inject_incr_trans; eauto.
-Qed.
-
-Remark val_list_inject_nth:
-  forall f l1 l2, val_list_inject f l1 l2 ->
-  forall n v1, nth_error l1 n = Some v1 ->
-  exists v2, nth_error l2 n = Some v2 /\ val_inject f v1 v2.
-Proof.
-  induction 1; destruct n; simpl; intros.
-  discriminate. discriminate.
-  injection H1; intros; subst v. exists v'; split; auto.
-  eauto.
-Qed.
-
-Lemma transl_expr_Eletvar_correct:
-   forall (le : list val) (e : Csharpminor.env) (m : mem) (n : nat)
-     (v : val),
-   nth_error le n = Some v ->
-   eval_expr_prop le e m (Csharpminor.Eletvar n) E0 m v.
-Proof.
-  intros; red; intros. monadInv TR.
-  exploit val_list_inject_nth; eauto. intros [tv [A B]].
-  exists f1; exists tm1; exists tv.
-  intuition.
-  eapply eval_Eletvar; auto.
-Qed.
-
-Lemma transl_expr_Ealloc_correct:
-  forall (le: list val) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr)
-         (t: trace) (m2: mem) (n: int) (m3: mem) (b: block),
-  Csharpminor.eval_expr prog le e m1 a t m2 (Vint n) ->
-  eval_expr_prop le e m1 a t m2 (Vint n) ->
-  Mem.alloc m2 0 (Int.signed n) = (m3, b) ->
-  eval_expr_prop le e m1 (Csharpminor.Ealloc a) t m3 (Vptr b Int.zero).
-Proof.
-  intros; red; intros. monadInv TR. 
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
-  inversion VINJ1. subst tv1 i. 
-  caseEq (alloc tm2 0 (Int.signed n)). intros tm3 tb TALLOC.
-  assert (LB: Int.min_signed <= 0). compute. congruence.
-  assert (HB: Int.signed n <= Int.max_signed). 
-    generalize (Int.signed_range n); omega.
-  exploit alloc_parallel_inject; eauto.
-  intros [MINJ3 INCR3].
-  exists (extend_inject b (Some (tb, 0)) f2); 
-  exists tm3; exists (Vptr tb Int.zero).
-  split. econstructor; eauto.
-  split. econstructor. unfold extend_inject, eq_block. rewrite zeq_true. reflexivity.
-  reflexivity.
-  split. assumption.
-  split. eapply inject_incr_trans; eauto. 
-  eapply match_callstack_alloc; eauto.
-Qed.
-
-Lemma transl_exprlist_Enil_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem),
-   eval_exprlist_prop le e m Csharpminor.Enil E0 m nil.
-Proof.
-  intros; red; intros. monadInv TR. 
-  exists f1; exists tm1; exists (@nil val).
-  intuition. constructor.
-Qed.
-
-Lemma transl_exprlist_Econs_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-     (a : Csharpminor.expr) (bl : Csharpminor.exprlist)
-     (t1: trace) (m1 : mem) (v : val) 
-     (t2: trace) (m2 : mem) (vl : list val) (t: trace),
-   Csharpminor.eval_expr prog le e m a t1 m1 v ->
-   eval_expr_prop le e m a t1 m1 v ->
-   Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vl ->
-   eval_exprlist_prop le e m1 bl t2 m2 vl ->
-   t = t1 ** t2 ->
-   eval_exprlist_prop le e m (Csharpminor.Econs a bl) t m2 (v :: vl).
-Proof.
-  intros; red; intros. monadInv TR. 
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exploit H2.
-    eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
-  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]].
-  exists f3; exists tm3; exists (tv1 :: tv2).
-  intuition. econstructor; eauto.
-  constructor. eapply val_inject_incr; eauto. auto.
-  eapply inject_incr_trans; eauto.
-Qed.
-
 Lemma transl_funcall_internal_correct:
    forall (m : mem) (f : Csharpminor.function) (vargs : list val)
      (e : Csharpminor.env) (m1 : mem) (lb : list block) (m2: mem)
@@ -2176,77 +1954,104 @@ Proof.
   intuition. constructor. constructor.
 Qed.
 
-Lemma transl_stmt_Sexpr_correct:
-   forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr)
-          (t: trace) (m1 : mem) (v : val),
-   Csharpminor.eval_expr prog nil e m a t m1 v ->
-   eval_expr_prop nil e m a t m1 v ->
-   exec_stmt_prop e m (Csharpminor.Sexpr a) t m1 Csharpminor.Out_normal.
-Proof.
-  intros; red; intros. monadInv TR. 
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exists f2; exists te1; exists tm2; exists Out_normal.
-  intuition. econstructor; eauto.
-  constructor.
-Qed.
-
 Lemma transl_stmt_Sassign_correct:
-   forall (e : Csharpminor.env) (m : mem)
-     (id : ident) (a : Csharpminor.expr) (t: trace) (m1 : mem) (b : block)
-     (chunk : memory_chunk) (v : val) (m2 : mem),
-   Csharpminor.eval_expr prog nil e m a t m1 v ->
-   eval_expr_prop nil e m a t m1 v ->
-   eval_var_ref prog e id b chunk ->
-   store chunk m1 b 0 v = Some m2 ->
-   exec_stmt_prop e m (Csharpminor.Sassign id a) t m2 Csharpminor.Out_normal.
+  forall (e : Csharpminor.env) (m : mem) (id : ident)
+         (a : Csharpminor.expr) (v : val) (m' : mem),
+  Csharpminor.eval_expr prog e m a v ->
+  exec_assign prog e m id v m' ->
+  exec_stmt_prop e m (Csharpminor.Sassign id a) E0 m' Csharpminor.Out_normal.
 Proof.
   intros; red; intros. monadInv TR.
-  exploit H0; eauto. 
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]].
-  exploit var_set_correct; eauto.
-  intros [te3 [tm3 [EVAL2 [MINJ2 MATCH2]]]].
-  exists f2; exists te3; exists tm3; exists Out_normal.
+  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]].
+  exploit var_set_correct; eauto. 
+  intros [te2 [tm2 [EVAL2 [MINJ2 MATCH2]]]].
+  exists f1; exists te2; exists tm2; exists Out_normal.
   intuition. constructor.
 Qed.
 
 Lemma transl_stmt_Sstore_correct:
-   forall (e : Csharpminor.env) (m : mem)
-     (chunk : memory_chunk) (a b : Csharpminor.expr) (t1: trace) (m1 : mem)
-     (v1 : val) (t2: trace) (m2 : mem) (v2 : val) 
-     (t3: trace) (m3 : mem),
-   Csharpminor.eval_expr prog nil e m a t1 m1 v1 ->
-   eval_expr_prop nil e m a t1 m1 v1 ->
-   Csharpminor.eval_expr prog nil e m1 b t2 m2 v2 ->
-   eval_expr_prop nil e m1 b t2 m2 v2 ->
-   storev chunk m2 v1 v2 = Some m3 ->
-   t3 = t1 ** t2 ->
-   exec_stmt_prop e m (Csharpminor.Sstore chunk a b) t3 m3 Csharpminor.Out_normal.
+  forall (e : Csharpminor.env) (m : mem) (chunk : memory_chunk)
+         (a b : Csharpminor.expr) (v1 v2 : val) (m' : mem),
+  Csharpminor.eval_expr prog e m a v1 ->
+  Csharpminor.eval_expr prog e m b v2 ->
+  storev chunk m v1 v2 = Some m' ->
+  exec_stmt_prop e m (Csharpminor.Sstore chunk a b) E0 m' Csharpminor.Out_normal.
 Proof.
   intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exploit H2.
-    eauto. 
-    eapply val_list_inject_incr; eauto.
-    eauto. eauto. 
-  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]].
+  exploit transl_expr_correct.
+    eauto. eauto. eexact H. eauto. 
+  intros [tv1 [EVAL1 INJ1]].
+  exploit transl_expr_correct.
+    eauto. eauto. eexact H0. eauto. 
+  intros [tv2 [EVAL2 INJ2]].
   exploit make_store_correct.
-    eexact EVAL1. eexact EVAL2. eauto. eauto. 
-    eapply val_inject_incr; eauto. eauto.
-  intros [tm4 [EVAL [MINJ4 NEXTBLOCK]]].
-  exists f3; exists te1; exists tm4; exists Out_normal.
+    eexact EVAL1. eexact EVAL2. eauto. eauto. eauto. eauto.
+  intros [tm2 [EXEC [MINJ2 NEXTBLOCK]]].
+  exists f1; exists te1; exists tm2; exists Out_normal.
   intuition. 
   constructor.
-  eapply inject_incr_trans; eauto.
-  assert (val_inject f3 v1 tv1). eapply val_inject_incr; eauto.
-  unfold storev in H3; destruct v1; try discriminate.
-  inversion H4. 
-  rewrite NEXTBLOCK. replace (nextblock m3) with (nextblock m2).
+  unfold storev in H1; destruct v1; try discriminate.
+  inv INJ1.
+  rewrite NEXTBLOCK. replace (nextblock m') with (nextblock m).
   eapply match_callstack_mapped; eauto. congruence.
   symmetry. eapply nextblock_store; eauto. 
 Qed.
 
+Lemma transl_stmt_Scall_correct:
+  forall (e : Csharpminor.env) (m : mem) (optid : option ident)
+         (sig : signature) (a : Csharpminor.expr)
+         (bl : list Csharpminor.expr) (vf : val) (vargs : list val)
+         (f : Csharpminor.fundef) (t : trace) (m1 : mem) (vres : val)
+         (m2 : mem),
+  Csharpminor.eval_expr prog e m a vf ->
+  Csharpminor.eval_exprlist prog e m bl vargs ->
+  Genv.find_funct (Genv.globalenv prog) vf = Some f ->
+  Csharpminor.funsig f = sig ->
+  Csharpminor.eval_funcall prog m f vargs t m1 vres ->
+  eval_funcall_prop m f vargs t m1 vres ->
+  exec_opt_assign prog e m1 optid vres m2 ->
+  exec_stmt_prop e m (Csharpminor.Scall optid sig a bl) t m2 Csharpminor.Out_normal.
+Proof.
+  intros;red;intros.
+  assert (forall tv, val_inject f1 vf tv -> tv = vf).
+    intros.
+    elim (Genv.find_funct_inv H1). intros bf VF. rewrite VF in H1.
+    rewrite Genv.find_funct_find_funct_ptr in H1. 
+    generalize (Genv.find_funct_ptr_negative H1). intro.
+    assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto.
+    generalize (mg_functions _ H8 _ H7). intro.
+    rewrite VF in H6. inv H6.  
+    decEq. congruence. 
+    replace x with 0. reflexivity. congruence.
+  inv H5; monadInv TR.
+  (* optid = None *)
+  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]].
+  exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]].
+  rewrite <- (H6 _ VINJ1) in H1. 
+  elim (functions_translated _ _ H1). intros tf [FIND TRF].
+  exploit H4; eauto.
+  intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]].
+  exists f2; exists te1; exists tm2; exists Out_normal.
+  intuition. eapply exec_Scall; eauto. 
+  apply sig_preserved; auto.
+  constructor.
+  (* optid = Some id *)
+  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]].
+  exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]].
+  rewrite <- (H6 _ VINJ1) in H1. 
+  elim (functions_translated _ _ H1). intros tf [FIND TRF].
+  exploit H4; eauto.
+  intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]].
+  exploit var_set_self_correct.
+    eauto. eexact MATCH3. eauto. eauto. eauto. 
+  intros [te3 [tm3 [EVAL4 [MINJ4 MATCH4]]]].  
+  exists f2; exists te3; exists tm3; exists Out_normal. intuition.
+  eapply exec_Sseq_continue. eapply exec_Scall; eauto. 
+  apply sig_preserved; auto.
+  simpl. eexact EVAL4. traceEq.
+  constructor.
+Qed.
+
 Lemma transl_stmt_Sseq_continue_correct:
   forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt)
          (t1 t2: trace) (m1 m2 : mem) (t: trace) (out : Csharpminor.outcome),
@@ -2284,54 +2089,27 @@ Proof.
   inversion OINJ1; subst out tout1; congruence.
 Qed.
 
-Lemma transl_stmt_Sifthenelse_true_correct:
-   forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr)
-     (sl1 sl2 : Csharpminor.stmt) 
-     (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem)
-     (out : Csharpminor.outcome) (t: trace),
-   Csharpminor.eval_expr prog nil e m a t1 m1 v1 ->
-   eval_expr_prop nil e m a t1 m1 v1 ->
-   Val.is_true v1 ->
-   Csharpminor.exec_stmt prog e m1 sl1 t2 m2 out ->
-   exec_stmt_prop e m1 sl1 t2 m2 out ->
-   t = t1 ** t2 ->
-   exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out.
-Proof.
-  intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exploit H3; eauto.
-  intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]].
-  exists f3; exists te3; exists tm3; exists tout.
-  intuition. 
-  eapply exec_Sifthenelse with (b1 := true); eauto.
-  eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; auto.
-  eapply inject_incr_trans; eauto.
-Qed.
-
-Lemma transl_stmt_Sifthenelse_false_correct:
-   forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr)
-     (sl1 sl2 : Csharpminor.stmt) 
-     (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem)
-     (out : Csharpminor.outcome) (t: trace),
-   Csharpminor.eval_expr prog nil e m a t1 m1 v1 ->
-   eval_expr_prop nil e m a t1 m1 v1 ->
-   Val.is_false v1 ->
-   Csharpminor.exec_stmt prog e m1 sl2 t2 m2 out ->
-   exec_stmt_prop e m1 sl2 t2 m2 out ->
-   t = t1 ** t2 ->
-   exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out.
+Lemma transl_stmt_Sifthenelse_correct:
+  forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr)
+         (sl1 sl2 : Csharpminor.stmt) (v : val) (vb : bool) (t : trace)
+         (m' : mem) (out : Csharpminor.outcome),
+  Csharpminor.eval_expr prog e m a v ->
+  Val.bool_of_val v vb ->
+  Csharpminor.exec_stmt prog e m (if vb then sl1 else sl2) t m' out ->
+  exec_stmt_prop e m (if vb then sl1 else sl2) t m' out ->
+  exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m' out.
 Proof.
   intros; red; intros. monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
-  exploit H3; eauto.
-  intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]].
-  exists f3; exists te3; exists tm3; exists tout.
+  exploit transl_expr_correct; eauto.
+  intros [tv1 [EVAL1 VINJ1]].
+  assert (transl_stmt cenv (if vb then sl1 else sl2) =
+          OK (if vb then x0 else x1)). destruct vb; auto.
+  exploit H2; eauto.
+  intros [f2 [te2 [tm2 [tout [EVAL2 [OINJ [MINJ2 [INCR2 MATCH2]]]]]]]].
+  exists f2; exists te2; exists tm2; exists tout.
   intuition. 
-  eapply exec_Sifthenelse with (b1 := false); eauto.
-  eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; auto.
-  eapply inject_incr_trans; eauto.
+  eapply exec_Sifthenelse; eauto.
+  eapply bool_of_val_inject; eauto.
 Qed.
 
 Lemma transl_stmt_Sloop_loop_correct:
@@ -2373,6 +2151,18 @@ Proof.
   inversion OINJ1; subst out tout1; congruence.
 Qed.
 
+Remark outcome_block_inject:
+  forall f out tout,
+  outcome_inject f out tout ->
+  outcome_inject f (Csharpminor.outcome_block out) (outcome_block tout).
+Proof.
+  induction 1; simpl.
+  constructor.
+  destruct n; constructor.
+  constructor.
+  constructor; auto.
+Qed.
+
 Lemma transl_stmt_Sblock_correct:
    forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt)
      (t1: trace) (m1 : mem) (out : Csharpminor.outcome),
@@ -2386,11 +2176,7 @@ Proof.
   intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
   exists f2; exists te2; exists tm2; exists (outcome_block tout1).
   intuition. eapply exec_Sblock; eauto.
-  inversion OINJ1; subst out tout1; simpl.
-  constructor.
-  destruct n; constructor.
-  constructor.
-  constructor; auto.
+  apply outcome_block_inject; auto.
 Qed.
 
 Lemma transl_stmt_Sexit_correct:
@@ -2403,21 +2189,22 @@ Proof.
 Qed.
 
 Lemma transl_stmt_Sswitch_correct:
-  forall (e : Csharpminor.env) (m : mem)
-         (a : Csharpminor.expr) (cases : list (int * nat)) (default : nat)
-         (t1 : trace) (m1 : mem) (n : int),
-  Csharpminor.eval_expr prog nil e m a t1 m1 (Vint n) ->
-  eval_expr_prop nil e m a t1 m1 (Vint n) ->
-  exec_stmt_prop e m (Csharpminor.Sswitch a cases default) t1 m1
-       (Csharpminor.Out_exit (Csharpminor.switch_target n default cases)).
+  forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr)
+         (cases : list (int * nat)) (default : nat) (n : int),
+  Csharpminor.eval_expr prog e m a (Vint n) ->
+  exec_stmt_prop e m (Csharpminor.Sswitch a cases default) E0 m
+                     (Csharpminor.Out_exit (switch_target n default cases)).
 Proof.
   intros; red; intros. monadInv TR.
-  exploit H0; eauto. 
-  intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
-  exists f2; exists te1; exists tm2; 
-  exists (Out_exit (switch_target n default cases)). intuition. 
-  constructor. inversion VINJ1. subst tv1. assumption.
-  constructor. 
+  exploit transl_expr_correct; eauto.
+  intros [tv1 [EVAL VINJ1]].
+  inv VINJ1.
+  exists f1; exists te1; exists tm1; exists (Out_exit (switch_target n default cases)).
+  split. constructor. auto.
+  split. constructor.
+  split. auto.
+  split. apply inject_incr_refl.
+  auto.
 Qed.
 
 Lemma transl_stmt_Sreturn_none_correct:
@@ -2431,17 +2218,16 @@ Proof.
 Qed.
 
 Lemma transl_stmt_Sreturn_some_correct:
-   forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr)
-     (t1: trace) (m1 : mem) (v : val),
-   Csharpminor.eval_expr prog nil e m a t1 m1 v ->
-   eval_expr_prop nil e m a t1 m1 v ->
-   exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) t1 m1
-     (Csharpminor.Out_return (Some v)).
+  forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr)
+         (v : val),
+  Csharpminor.eval_expr prog e m a v ->
+  exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) E0 m
+                     (Csharpminor.Out_return (Some v)).
 Proof.
   intros; red; intros; monadInv TR.
-  exploit H0; eauto.
-  intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
-  exists f2; exists te1; exists tm2; exists (Out_return (Some tv1)).
+  exploit transl_expr_correct; eauto.
+  intros [tv1 [EVAL VINJ1]].
+  exists f1; exists te1; exists tm1; exists (Out_return (Some tv1)).
   intuition. econstructor; eauto. constructor; auto.
 Qed.
 
@@ -2453,36 +2239,45 @@ Lemma transl_function_correct:
    Csharpminor.eval_funcall prog m1 f vargs t m2 vres ->
    eval_funcall_prop m1 f vargs t m2 vres.
 Proof
-  (Csharpminor.eval_funcall_ind4 prog
-     eval_expr_prop
-     eval_exprlist_prop
+  (Csharpminor.eval_funcall_ind2 prog
+     eval_funcall_prop
+     exec_stmt_prop
+
+     transl_funcall_internal_correct
+     transl_funcall_external_correct
+     transl_stmt_Sskip_correct
+     transl_stmt_Sassign_correct
+     transl_stmt_Sstore_correct
+     transl_stmt_Scall_correct
+     transl_stmt_Sseq_continue_correct
+     transl_stmt_Sseq_stop_correct
+     transl_stmt_Sifthenelse_correct
+     transl_stmt_Sloop_loop_correct
+     transl_stmt_Sloop_exit_correct
+     transl_stmt_Sblock_correct
+     transl_stmt_Sexit_correct
+     transl_stmt_Sswitch_correct
+     transl_stmt_Sreturn_none_correct
+     transl_stmt_Sreturn_some_correct).
+
+Lemma transl_stmt_correct:
+   forall e m1 s t m2 out,
+   Csharpminor.exec_stmt prog e m1 s t m2 out ->
+   exec_stmt_prop e m1 s t m2 out.
+Proof
+  (Csharpminor.exec_stmt_ind2 prog
      eval_funcall_prop
      exec_stmt_prop
 
-     transl_expr_Evar_correct
-     transl_expr_Eaddrof_correct
-     transl_expr_Econst_correct
-     transl_expr_Eunop_correct
-     transl_expr_Ebinop_correct
-     transl_expr_Eload_correct
-     transl_expr_Ecall_correct
-     transl_expr_Econdition_true_correct
-     transl_expr_Econdition_false_correct
-     transl_expr_Elet_correct
-     transl_expr_Eletvar_correct
-     transl_expr_Ealloc_correct
-     transl_exprlist_Enil_correct
-     transl_exprlist_Econs_correct
      transl_funcall_internal_correct
      transl_funcall_external_correct
      transl_stmt_Sskip_correct
-     transl_stmt_Sexpr_correct
      transl_stmt_Sassign_correct
      transl_stmt_Sstore_correct
+     transl_stmt_Scall_correct
      transl_stmt_Sseq_continue_correct
      transl_stmt_Sseq_stop_correct
-     transl_stmt_Sifthenelse_true_correct
-     transl_stmt_Sifthenelse_false_correct
+     transl_stmt_Sifthenelse_correct
      transl_stmt_Sloop_loop_correct
      transl_stmt_Sloop_exit_correct
      transl_stmt_Sblock_correct
@@ -2491,6 +2286,133 @@ Proof
      transl_stmt_Sreturn_none_correct
      transl_stmt_Sreturn_some_correct).
 
+(** ** Semantic preservation for divergence *)
+
+Definition evalinf_funcall_prop
+    (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: traceinf) : Prop :=
+  forall tfn f1 tm1 cs targs
+  (TR: transl_fundef gce fn = OK tfn)
+  (MINJ: mem_inject f1 m1 tm1)
+  (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1)
+  (ARGSINJ: val_list_inject f1 args targs),
+  evalinf_funcall tge tm1 tfn targs t.
+
+Definition execinf_stmt_prop
+    (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: traceinf): Prop :=
+  forall cenv ts f1 te1 tm1 sp lo hi cs
+  (TR: transl_stmt cenv s = OK ts)
+  (MINJ: mem_inject f1 m1 tm1)
+  (MATCH: match_callstack f1
+           (mkframe cenv e te1 sp lo hi :: cs)
+           m1.(nextblock) tm1.(nextblock) m1),
+  execinf_stmt tge (Vptr sp Int.zero) te1 tm1 ts t.
+
+Theorem transl_function_divergence_correct:
+  forall m1 fn args t,
+  Csharpminor.evalinf_funcall prog m1 fn args t ->
+  evalinf_funcall_prop m1 fn args t.
+Proof.
+  unfold evalinf_funcall_prop; cofix FUNCALL.
+  assert (STMT: forall e m1 s t,
+          Csharpminor.execinf_stmt prog e m1 s t ->
+          execinf_stmt_prop e m1 s t).
+  unfold execinf_stmt_prop; cofix STMT.
+  intros. inv H; simpl in TR; try (monadInv TR).
+  (* Scall *)
+  assert (forall tv, val_inject f1 vf tv -> tv = vf).
+    intros.
+    elim (Genv.find_funct_inv H2). intros bf VF. rewrite VF in H2.
+    rewrite Genv.find_funct_find_funct_ptr in H2. 
+    generalize (Genv.find_funct_ptr_negative H2). intro.
+    assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto.
+    generalize (mg_functions _ H5 _ H3). intro.
+    rewrite VF in H. inv H.  
+    decEq. congruence. 
+    replace x with 0. reflexivity. congruence.
+  destruct optid; monadInv TR.
+  (* optid = Some i *)
+  destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ)
+  as [tv1 [EVAL1 VINJ1]].
+  destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1)
+  as [tv2 [EVAL2 VINJ2]].
+  rewrite <- (H _ VINJ1) in H2. 
+  elim (functions_translated _ _ H2). intros tf [FIND TRF].
+  apply execinf_Sseq_1. eapply execinf_Scall.
+  eauto. eauto. eauto. apply sig_preserved; auto. 
+  eapply FUNCALL; eauto.
+  (* optid = None *)
+  destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ)
+  as [tv1 [EVAL1 VINJ1]].
+  destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1)
+  as [tv2 [EVAL2 VINJ2]].
+  rewrite <- (H _ VINJ1) in H2. 
+  elim (functions_translated _ _ H2). intros tf [FIND TRF].
+  eapply execinf_Scall.
+  eauto. eauto. eauto. apply sig_preserved; auto. 
+  eapply FUNCALL; eauto.
+  (* Sseq, 1 *)
+  apply execinf_Sseq_1. eapply STMT; eauto. 
+  (* Sseq, 2 *)
+  destruct (transl_stmt_correct _ _ _ _ _ _ H0
+            _ _ _ _ _ _ _ _ _ EQ MINJ MATCH)
+  as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]].
+  inv OUT.
+  eapply execinf_Sseq_2. eexact EXEC1.
+  eapply STMT; eauto. 
+  auto.
+  (* Sifthenelse, true *)
+  destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ)
+  as [tv1 [EVAL1 VINJ1]].
+  assert (transl_stmt cenv (if vb then sl1 else sl2) =
+          OK (if vb then x0 else x1)). destruct vb; auto.
+  eapply execinf_Sifthenelse. eexact EVAL1. 
+  eapply bool_of_val_inject; eauto.
+  eapply STMT; eauto.
+  (* Sloop, body *)
+  eapply execinf_Sloop_body. eapply STMT; eauto.
+  (* Sloop, loop *)
+  destruct (transl_stmt_correct _ _ _ _ _ _ H0
+            _ _ _ _ _ _ _ _ _ EQ MINJ MATCH)
+  as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]].
+  inv OUT.
+  eapply execinf_Sloop_loop. eexact EXEC1. 
+  eapply STMT; eauto. 
+  simpl. rewrite EQ. auto. auto.
+  (* Sblock *)
+  apply execinf_Sblock. eapply STMT; eauto.
+  (* stutter *)
+  generalize (execinf_stmt_N_inv _ _ _ _ _ _ H0); intro.
+  destruct s; try contradiction; monadInv TR.
+  apply execinf_Sseq_1. eapply STMT; eauto. 
+  apply execinf_Sblock. eapply STMT; eauto.
+  (* Sloop_block *)
+  destruct (transl_stmt_correct _ _ _ _ _ _ H0
+            _ _ _ _ _ _ _ _ _ EQ MINJ MATCH)
+  as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]].
+  inv OUT. 
+  eapply execinf_Sloop_loop. eexact EXEC1. 
+  eapply STMT with (s := Csharpminor.Sloop sl); eauto.
+  apply execinf_Sblock_inv; eauto.
+  simpl. rewrite EQ; auto. auto.   
+  (* Function *)
+  intros. inv H.
+  monadInv TR. generalize EQ.
+  unfold transl_function.
+  caseEq (build_compilenv gce f); intros cenv stacksize CENV.
+  destruct (zle stacksize Int.max_signed); try congruence.
+  intro TR. monadInv TR.
+  caseEq (alloc tm1 0 stacksize). intros tm2 sp ALLOC.
+  destruct (function_entry_ok _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
+            H1 H2 MATCH CENV z ALLOC ARGSINJ MINJ H0 EQ2)
+  as [f2 [te2 [tm3 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]].
+  eapply evalinf_funcall_internal; simpl.
+  eauto. reflexivity. eapply execinf_Sseq_2. eexact STOREPARAM. 
+  unfold execinf_stmt_prop in STMT. eapply STMT; eauto.
+  traceEq.
+Qed.
+
+(** ** Semantic preservation for whole programs *)  
+
 (** The [match_globalenvs] relation holds for the global environments
   of the source program and the transformed program. *)
 
@@ -2513,12 +2435,11 @@ Qed.
   follows. *)
 
 Theorem transl_program_correct:
-  forall t n,
-  Csharpminor.exec_program prog t (Vint n) ->
-  exec_program tprog t (Vint n).
+  forall beh,
+  Csharpminor.exec_program prog beh ->
+  exec_program tprog beh.
 Proof.
-  intros t n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]].
-  elim (function_ptr_translated _ _ FINDF). intros tfn [TFIND TR].
+  intros.
   set (m0 := Genv.init_mem prog) in *.
   set (f := meminj_init m0).
   assert (MINJ0: mem_inject f m0 m0).
@@ -2526,17 +2447,31 @@ Proof.
     unfold m0; apply Genv.initmem_inject_neutral.
   assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0).
     constructor. unfold f; apply match_globalenvs_init.
-  fold ge in EVAL.
+  inv H.
+  (* Terminating case *)
+  subst ge0 m1. 
+  elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR].
+  fold ge in H3.
   exploit transl_function_correct; eauto.
   intros [f1 [tm1 [tres [TEVAL [VINJ [MINJ1 [INCR MATCH1]]]]]]].
-  exists b; exists tfn; exists tm1.
-  split. fold tge. rewrite <- FINDS. 
-  replace (prog_main prog) with (AST.prog_main tprog). fold ge. apply symbols_preserved.
+  econstructor; eauto. 
+  fold tge. rewrite <- H0. fold ge. 
+  replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved.
   apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption.
-  split. assumption.
-  split. rewrite <- SIG. apply sig_preserved; auto.
+  rewrite <- H2. apply sig_preserved; auto.
+  rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
+  inv VINJ. fold tge; fold m0. eexact TEVAL.
+  (* Diverging case *)
+  subst ge0 m1. 
+  elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR].
+  econstructor; eauto.
+  fold tge. rewrite <- H0. fold ge. 
+  replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved.
+  apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption.
+  rewrite <- H2. apply sig_preserved; auto.
   rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
-  inversion VINJ; subst tres. assumption. 
+  fold tge; fold m0.
+  eapply (transl_function_divergence_correct _ _ _ _ H3); eauto.
 Qed.
 
 End TRANSLATION.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 385f7c68..af601aca 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -11,6 +11,7 @@ Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Csyntax.
+Require Import Smallstep.
 
 (** * Semantics of type-dependent operations *)
 
@@ -509,129 +510,108 @@ Section RELSEM.
 
 Variable ge: genv.
 
-(** [eval_expr ge e m1 a t m2 v] defines the evaluation of expression [a]
-  in r-value position.  [v] is the value of the expression.
-  [m1] is the initial memory state, [m2] the final memory state.
-  [t] is the trace of input/output events performed during this
-  evaluation. *)
+Section EXPR.
+
+Variable e: env.
+Variable m: mem.
 
-Inductive eval_expr: env -> mem -> expr -> trace -> mem -> val -> Prop :=
-  | eval_Econst_int:   forall e m i ty,
-      eval_expr e m (Expr (Econst_int i) ty)
-               E0 m (Vint i)
-  | eval_Econst_float:   forall e m f ty,
-      eval_expr e m (Expr (Econst_float f) ty)
-               E0 m (Vfloat f)
-  | eval_Elvalue: forall e m a ty t m1 loc ofs v,
-      eval_lvalue e m (Expr a ty) t m1 loc ofs ->
-      load_value_of_type ty m1 loc ofs = Some v ->
-      eval_expr e m (Expr a ty) 
-                t m1 v
-  | eval_Eaddrof: forall e m a t m1 loc ofs ty,
-      eval_lvalue e m a t m1 loc ofs ->
-      eval_expr e m (Expr (Eaddrof a) ty)
-                t m1 (Vptr loc ofs)
-  | eval_Esizeof: forall e m ty' ty,
-      eval_expr e m (Expr (Esizeof ty') ty) 
-               E0 m (Vint (Int.repr (sizeof ty')))
-  | eval_Eunop:  forall e m op a ty t m1 v1 v,
-      eval_expr e m a t m1 v1 ->
+(** [eval_expr ge e m a v] defines the evaluation of expression [a]
+  in r-value position.  [v] is the value of the expression.
+  [e] is the current environment and [m] is the current memory state. *)
+
+Inductive eval_expr: expr -> val -> Prop :=
+  | eval_Econst_int:   forall i ty,
+      eval_expr (Expr (Econst_int i) ty) (Vint i)
+  | eval_Econst_float:   forall f ty,
+      eval_expr (Expr (Econst_float f) ty) (Vfloat f)
+  | eval_Elvalue: forall a ty loc ofs v,
+      eval_lvalue (Expr a ty) loc ofs ->
+      load_value_of_type ty m loc ofs = Some v ->
+      eval_expr (Expr a ty) v
+  | eval_Eaddrof: forall a ty loc ofs,
+      eval_lvalue a loc ofs ->
+      eval_expr (Expr (Eaddrof a) ty) (Vptr loc ofs)
+  | eval_Esizeof: forall ty' ty,
+      eval_expr (Expr (Esizeof ty') ty) (Vint (Int.repr (sizeof ty')))
+  | eval_Eunop:  forall op a ty v1 v,
+      eval_expr a v1 ->
       sem_unary_operation op v1 (typeof a) = Some v ->
-      eval_expr e m (Expr (Eunop op a) ty) 
-                t m1 v
-  | eval_Ebinop: forall e m op a1 a2 ty t1 m1 v1 t2 m2 v2 v,
-      eval_expr e m a1 t1 m1 v1 ->
-      eval_expr e m1 a2 t2 m2 v2 ->
-      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m2 = Some v ->
-      eval_expr e m (Expr (Ebinop op a1 a2) ty)
-                (t1 ** t2) m2 v
-  | eval_Eorbool_1: forall e m a1 a2 t m1 v1 ty,
-      eval_expr e m a1 t m1 v1 ->
+      eval_expr (Expr (Eunop op a) ty) v
+  | eval_Ebinop: forall op a1 a2 ty v1 v2 v,
+      eval_expr a1 v1 ->
+      eval_expr a2 v2 ->
+      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
+      eval_expr (Expr (Ebinop op a1 a2) ty) v
+  | eval_Eorbool_1: forall a1 a2 ty v1,
+      eval_expr a1 v1 ->
       is_true v1 (typeof a1) ->
-      eval_expr e m (Expr (Eorbool a1 a2) ty)
-                  t m1 Vtrue
-  | eval_Eorbool_2: forall e m a1 a2 ty t1 m1 v1 t2 m2 v2 v,
-      eval_expr e m a1 t1 m1 v1 ->
+      eval_expr (Expr (Eorbool a1 a2) ty) Vtrue
+  | eval_Eorbool_2: forall a1 a2 ty v1 v2 v,
+      eval_expr a1 v1 ->
       is_false v1 (typeof a1) -> 
-      eval_expr e m1 a2 t2 m2 v2 ->
+      eval_expr a2 v2 ->
       bool_of_val v2 (typeof a2) v ->
-      eval_expr e m (Expr (Eorbool a1 a2) ty)
-                (t1 ** t2) m2 v
-  | eval_Eandbool_1: forall e m a1 a2 t m1 v1 ty,
-      eval_expr e m a1 t m1 v1 ->
+      eval_expr (Expr (Eorbool a1 a2) ty) v
+  | eval_Eandbool_1: forall a1 a2 ty v1,
+      eval_expr a1 v1 ->
       is_false v1 (typeof a1) ->
-      eval_expr e m (Expr (Eandbool a1 a2) ty)
-                  t m1 Vfalse
-  | eval_Eandbool_2: forall e m a1 a2 ty t1 m1 v1 t2 m2 v2 v,
-      eval_expr e m a1 t1 m1 v1 ->
+      eval_expr (Expr (Eandbool a1 a2) ty) Vfalse
+  | eval_Eandbool_2: forall a1 a2 ty v1 v2 v,
+      eval_expr a1 v1 ->
       is_true v1 (typeof a1) -> 
-      eval_expr e m1 a2 t2 m2 v2 ->
+      eval_expr a2 v2 ->
       bool_of_val v2 (typeof a2) v ->
-      eval_expr e m (Expr (Eandbool a1 a2) ty)
-                (t1 ** t2) m2 v
-  | eval_Ecast:   forall e m a ty t m1 v1 v,
-      eval_expr e m a t m1 v1 ->
+      eval_expr (Expr (Eandbool a1 a2) ty) v
+  | eval_Ecast:   forall a ty v1 v,
+      eval_expr a v1 ->
       cast v1 (typeof a) ty v ->
-      eval_expr e m (Expr (Ecast ty a) ty)
-                t m1 v
-  | eval_Ecall: forall e m a bl ty m3 vres t1 m1 vf t2 m2 vargs f t3,
-      eval_expr e m a t1 m1 vf ->
-      eval_exprlist e m1 bl t2 m2 vargs ->
-      Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
-      eval_funcall m2 f vargs t3 m3 vres ->
-      eval_expr e m (Expr (Ecall a bl) ty)
-                (t1 ** t2 ** t3) m3 vres 
-
-(** [eval_lvalue ge e m1 a t m2  b ofs] defines the evaluation of
-  expression [a] in r-value position.  The result of the evaluation
-  is the block reference [b] and the byte offset [ofs] of the
-  memory location where the value of [a] resides.
-  The other parameters are as in [eval_expr]. *)
-
-with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop :=
-  | eval_Evar_local:   forall e m id l ty,
+      eval_expr (Expr (Ecast ty a) ty) v
+
+(** [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
+  in l-value position.  The result is the memory location [b, ofs]
+  that contains the value of the expression [a]. *)
+
+with eval_lvalue: expr -> block -> int -> Prop :=
+  | eval_Evar_local:   forall id l ty,
       e!id = Some l ->
-      eval_lvalue e m (Expr (Evar id) ty) 
-                 E0 m l Int.zero
-  | eval_Evar_global: forall e m id l ty,
+      eval_lvalue (Expr (Evar id) ty) l Int.zero
+  | eval_Evar_global: forall id l ty,
       e!id = None ->
       Genv.find_symbol ge id = Some l ->
-      eval_lvalue e m (Expr (Evar id) ty)
-                 E0 m l Int.zero
-  | eval_Ederef: forall e m m1 a t ofs ty l,
-      eval_expr e m a t m1 (Vptr l ofs) ->
-      eval_lvalue e m (Expr (Ederef a) ty)
-                  t m1 l ofs
-  | eval_Eindex: forall e m a1 t1 m1 v1 a2 t2 m2 v2 l ofs ty,
-      eval_expr e m a1 t1 m1 v1 ->
-      eval_expr e m1 a2 t2 m2 v2 ->
+      eval_lvalue (Expr (Evar id) ty) l Int.zero
+  | eval_Ederef: forall a ty l ofs,
+      eval_expr a (Vptr l ofs) ->
+      eval_lvalue (Expr (Ederef a) ty) l ofs
+  | eval_Eindex: forall a1 a2 ty v1 v2 l ofs,
+      eval_expr a1 v1 ->
+      eval_expr a2 v2 ->
       sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
-      eval_lvalue e m (Expr (Eindex a1 a2) ty)
-                  (t1 ** t2) m2 l ofs
- | eval_Efield_struct:   forall e m a t m1 l ofs id fList i ty delta,
-      eval_lvalue e m a t m1 l ofs ->
+      eval_lvalue (Expr (Eindex a1 a2) ty) l ofs
+ | eval_Efield_struct:   forall a i ty l ofs id fList delta,
+      eval_lvalue a l ofs ->
       typeof a = Tstruct id fList ->
       field_offset i fList = OK delta ->
-      eval_lvalue e m (Expr (Efield a i) ty)
-                  t m1 l (Int.add ofs (Int.repr delta))
- | eval_Efield_union:   forall e m a t m1 l ofs id fList i ty,
-      eval_lvalue e m a t m1 l ofs ->
+      eval_lvalue (Expr (Efield a i) ty) l (Int.add ofs (Int.repr delta))
+ | eval_Efield_union:   forall a i ty l ofs id fList,
+      eval_lvalue a l ofs ->
       typeof a = Tunion id fList ->
-      eval_lvalue e m (Expr (Efield a i) ty) 
-                  t m1 l ofs
+      eval_lvalue (Expr (Efield a i) ty) l ofs.
+
+Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
+  with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop.
 
-(** [eval_exprlist ge e m1 al t m2 vl] evaluates a list of r-value
+(** [eval_exprlist ge e m al vl] evaluates a list of r-value
   expressions [al] to their values [vl]. *)
 
-with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> list val -> Prop :=
-  | eval_Enil:   forall e m,
-      eval_exprlist e m Enil E0 m nil
-  | eval_Econs:   forall e m a bl t1 m1 v t2 m2 vl,
-      eval_expr e m a t1 m1 v ->
-      eval_exprlist e m1 bl t2 m2 vl ->
-      eval_exprlist e m (Econs a bl)
-                    (t1 ** t2) m2 (v :: vl)
+Inductive eval_exprlist: list expr -> list val -> Prop :=
+  | eval_Enil:
+      eval_exprlist nil nil
+  | eval_Econs:   forall a bl v vl,
+      eval_expr a v ->
+      eval_exprlist bl vl ->
+      eval_exprlist (a :: bl) (v :: vl).
+
+End EXPR.
 
 (** [exec_stmt ge e m1 s t m2 out] describes the execution of 
   the statement [s].  [out] is the outcome for this execution.
@@ -639,20 +619,34 @@ with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> list val -> Prop :
   [t] is the trace of input/output events performed during this
   evaluation. *)
 
-with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
+Inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
   | exec_Sskip:   forall e m,
       exec_stmt e m Sskip
                E0 m Out_normal
-  | exec_Sexpr: forall e m a t m1 v,
-      eval_expr e m a t m1 v ->
-      exec_stmt e m (Sexpr a)
-                t m1 Out_normal 
-  | exec_Sassign:   forall e m a1 a2 t1 m1 loc ofs t2 m2 v2 m3,
-      eval_lvalue e m a1 t1 m1 loc ofs ->
-      eval_expr e m1 a2 t2 m2 v2 ->
-      store_value_of_type (typeof a1) m2 loc ofs v2 = Some m3 ->
+  | exec_Sassign:   forall e m a1 a2 loc ofs v2 m',
+      eval_lvalue e m a1 loc ofs ->
+      eval_expr e m a2 v2 ->
+      store_value_of_type (typeof a1) m loc ofs v2 = Some m' ->
       exec_stmt e m (Sassign a1 a2)
-                (t1 ** t2) m3 Out_normal
+               E0 m' Out_normal
+  | exec_Scall_none:   forall e m a al vf vargs f t m' vres,
+      eval_expr e m a vf ->
+      eval_exprlist e m al vargs ->
+      Genv.find_funct ge vf = Some f ->
+      type_of_fundef f = typeof a ->
+      eval_funcall m f vargs t m' vres ->
+      exec_stmt e m (Scall None a al)
+                t m' Out_normal
+  | exec_Scall_some:   forall e m lhs a al loc ofs vf vargs f t m' vres m'',
+      eval_lvalue e m lhs loc ofs ->
+      eval_expr e m a vf ->
+      eval_exprlist e m al vargs ->
+      Genv.find_funct ge vf = Some f ->
+      type_of_fundef f = typeof a ->
+      eval_funcall m f vargs t m' vres ->
+      store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' ->
+      exec_stmt e m (Scall (Some lhs) a al)
+                t m'' Out_normal
   | exec_Sseq_1:   forall e m s1 s2 t1 m1 t2 m2 out,
       exec_stmt e m s1 t1 m1 Out_normal ->
       exec_stmt e m1 s2 t2 m2 out ->
@@ -663,102 +657,103 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
       out <> Out_normal ->
       exec_stmt e m (Ssequence s1 s2)
                 t1 m1 out
-  | exec_Sifthenelse_true: forall e m a s1 s2 t1 m1 v1 t2 m2 out,
-      eval_expr e m a t1 m1 v1 ->
+  | exec_Sifthenelse_true: forall e m a s1 s2 v1 t m' out,
+      eval_expr e m a v1 ->
       is_true v1 (typeof a) ->
-      exec_stmt e m1 s1 t2 m2 out ->
+      exec_stmt e m s1 t m' out ->
       exec_stmt e m (Sifthenelse a s1 s2)
-                (t1 ** t2) m2 out
-  | exec_Sifthenelse_false: forall e m a s1 s2 t1 m1 v1 t2 m2 out,
-      eval_expr e m a t1 m1 v1 ->
+                t m' out
+  | exec_Sifthenelse_false: forall e m a s1 s2 v1 t m' out,
+      eval_expr e m a v1 ->
       is_false v1 (typeof a) ->
-      exec_stmt e m1 s2 t2 m2 out ->
+      exec_stmt e m s2 t m' out ->
       exec_stmt e m (Sifthenelse a s1 s2)
-                (t1 ** t2) m2 out
+                t m' out
   | exec_Sreturn_none:   forall e m,
       exec_stmt e m (Sreturn None)
                E0 m (Out_return None)
-  | exec_Sreturn_some: forall e m a t m1 v,
-      eval_expr e m a t m1 v ->
+  | exec_Sreturn_some: forall e m a v,
+      eval_expr e m a v ->
       exec_stmt e m (Sreturn (Some a))
-                t m1 (Out_return (Some v))
+               E0 m (Out_return (Some v))
   | exec_Sbreak:   forall e m,
       exec_stmt e m Sbreak
                E0 m Out_break
   | exec_Scontinue:   forall e m,
       exec_stmt e m Scontinue
                E0 m Out_continue
-  | exec_Swhile_false: forall e m s a t v m1,
-      eval_expr e m a t m1 v ->
+  | exec_Swhile_false: forall e m a s v,
+      eval_expr e m a v ->
       is_false v (typeof a) ->
       exec_stmt e m (Swhile a s)
-                t m1 Out_normal
-  | exec_Swhile_stop: forall e m a t1 m1 v s m2 t2 out2 out,
-      eval_expr e m a t1 m1 v ->
+               E0 m Out_normal
+  | exec_Swhile_stop: forall e m a v s t m' out' out,
+      eval_expr e m a v ->
       is_true v (typeof a) ->
-      exec_stmt e m1 s t2 m2 out2 ->
-      out_break_or_return out2 out ->
+      exec_stmt e m s t m' out' ->
+      out_break_or_return out' out ->
       exec_stmt e m (Swhile a s)
-                (t1 ** t2) m2 out
-  | exec_Swhile_loop: forall e m a t1 m1 v s out2 out t2 m2 t3 m3,
-      eval_expr e m a t1 m1 v ->
+                t m' out
+  | exec_Swhile_loop: forall e m a s v t1 m1 out1 t2 m2 out,
+      eval_expr e m a v ->
       is_true v (typeof a) ->
-      exec_stmt e m1 s t2 m2 out2 ->
-      out_normal_or_continue out2 ->
-      exec_stmt e m2 (Swhile a s) t3 m3 out ->
-      exec_stmt e m (Swhile a s)
-                (t1 ** t2 ** t3) m3 out
-  | exec_Sdowhile_false: forall e m s a t1 m1 out1 v t2 m2,
       exec_stmt e m s t1 m1 out1 ->
       out_normal_or_continue out1 ->
-      eval_expr e m1 a t2 m2 v ->
+      exec_stmt e m1 (Swhile a s) t2 m2 out ->
+      exec_stmt e m (Swhile a s)
+                (t1 ** t2) m2 out
+  | exec_Sdowhile_false: forall e m s a t m1 out1 v,
+      exec_stmt e m s t m1 out1 ->
+      out_normal_or_continue out1 ->
+      eval_expr e m1 a v ->
       is_false v (typeof a) ->
       exec_stmt e m (Sdowhile a s)
-                (t1 ** t2) m2 Out_normal
+                t m1 Out_normal
   | exec_Sdowhile_stop: forall e m s a t m1 out1 out,
       exec_stmt e m s t m1 out1 ->
       out_break_or_return out1 out ->
       exec_stmt e m (Sdowhile a s)
                 t m1 out
-  | exec_Sdowhile_loop: forall e m s a m1 m2 m3 t1 t2 t3 out out1 v,
+  | exec_Sdowhile_loop: forall e m s a m1 m2 t1 t2 out out1 v,
       exec_stmt e m s t1 m1 out1 ->
       out_normal_or_continue out1 ->
-      eval_expr e m1 a t2 m2 v ->
+      eval_expr e m1 a v ->
       is_true v (typeof a) ->
-      exec_stmt e m2 (Sdowhile a s) t3 m3 out ->
+      exec_stmt e m1 (Sdowhile a s) t2 m2 out ->
       exec_stmt e m (Sdowhile a s) 
-                (t1 ** t2 ** t3) m3 out
+                (t1 ** t2) m2 out
   | exec_Sfor_start: forall e m s a1 a2 a3 out m1 m2 t1 t2,
+      a1 <> Sskip ->
       exec_stmt e m a1 t1 m1 Out_normal ->
       exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out ->
       exec_stmt e m (Sfor a1 a2 a3 s) 
                 (t1 ** t2) m2 out
-  | exec_Sfor_false: forall e m s a2 a3 t v m1,
-      eval_expr e m a2 t m1 v ->
+  | exec_Sfor_false: forall e m s a2 a3 v,
+      eval_expr e m a2 v ->
       is_false v (typeof a2) ->
       exec_stmt e m (Sfor Sskip a2 a3 s)
-                t m1 Out_normal
-  | exec_Sfor_stop: forall e m s a2 a3 v m1 m2 t1 t2 out2 out,
-      eval_expr e m a2 t1 m1 v ->
+               E0 m Out_normal
+  | exec_Sfor_stop: forall e m s a2 a3 v m1 t out1 out,
+      eval_expr e m a2 v ->
       is_true v (typeof a2) ->
-      exec_stmt e m1 s t2 m2 out2 ->
-      out_break_or_return out2 out ->
+      exec_stmt e m s t m1 out1 ->
+      out_break_or_return out1 out ->
       exec_stmt e m (Sfor Sskip a2 a3 s)
-                (t1 ** t2) m2 out
-  | exec_Sfor_loop: forall e m s a2 a3 v m1 m2 m3 m4 t1 t2 t3 t4 out2 out,
-      eval_expr e m a2 t1 m1 v ->
+                t m1 out
+  | exec_Sfor_loop: forall e m s a2 a3 v m1 m2 m3 t1 t2 t3 out1 out,
+      eval_expr e m a2 v ->
       is_true v (typeof a2) ->
-      exec_stmt e m1 s t2 m2 out2 ->
-      out_normal_or_continue out2 ->
-      exec_stmt e m2 a3 t3 m3 Out_normal ->
-      exec_stmt e m3 (Sfor Sskip a2 a3 s) t4 m4 out ->
+      exec_stmt e m s t1 m1 out1 ->
+      out_normal_or_continue out1 ->
+      exec_stmt e m1 a3 t2 m2 Out_normal ->
+      exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out ->
       exec_stmt e m (Sfor Sskip a2 a3 s)
-                (t1 ** t2 ** t3 ** t4) m4 out
-  | exec_Sswitch:   forall e m a t1 m1 n sl t2 m2 out,
-      eval_expr e m a t1 m1 (Vint n) ->
-      exec_lblstmts e m1 (select_switch n sl) t2 m2 out ->
+                (t1 ** t2 ** t3) m3 out
+  | exec_Sswitch:   forall e m a t n sl m1 out,
+      eval_expr e m a (Vint n) ->
+      exec_lblstmts e m (select_switch n sl) t m1 out ->
       exec_stmt e m (Sswitch a sl)
-                (t1 ** t2) m2 (outcome_switch out)
+                t m1 (outcome_switch out)
 
 (** [exec_lblstmts ge e m1 ls t m2 out] is a variant of [exec_stmt]
   that executes in sequence all statements in the list of labeled
@@ -791,25 +786,137 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       event_match (external_function id targs tres) vargs t vres ->
       eval_funcall m (External id targs tres) vargs t m vres.
 
-Scheme eval_expr_ind6 := Minimality for eval_expr Sort Prop
-  with eval_lvalue_ind6 := Minimality for eval_lvalue Sort Prop
-  with eval_exprlist_ind6 := Minimality for eval_exprlist Sort Prop
-  with exec_stmt_ind6 := Minimality for exec_stmt Sort Prop
-  with exec_lblstmts_ind6 := Minimality for exec_lblstmts Sort Prop
-  with eval_funcall_ind6 := Minimality for eval_funcall Sort Prop.
+Scheme exec_stmt_ind3 := Minimality for exec_stmt Sort Prop
+  with exec_lblstmts_ind3 := Minimality for exec_lblstmts Sort Prop
+  with eval_funcall_ind3 := Minimality for eval_funcall Sort Prop.
+
+(** Coinductive semantics for divergence.
+  [execinf_stmt ge e m s t] holds if the execution of statement [s]
+  diverges, i.e. loops infinitely.  [t] is the possibly infinite
+  trace of observable events performed during the execution. *)
+
+CoInductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
+  | execinf_Scall:   forall e m lhs a al vf vargs f t,
+      eval_expr e m a vf ->
+      eval_exprlist e m al vargs ->
+      Genv.find_funct ge vf = Some f ->
+      type_of_fundef f = typeof a ->
+      evalinf_funcall m f vargs t ->
+      execinf_stmt e m (Scall lhs a al) t
+  | execinf_Sseq_1:   forall e m s1 s2 t,
+      execinf_stmt e m s1 t ->
+      execinf_stmt e m (Ssequence s1 s2) t
+  | execinf_Sseq_2:   forall e m s1 s2 t1 m1 t2,
+      exec_stmt e m s1 t1 m1 Out_normal ->
+      execinf_stmt e m1 s2 t2 ->
+      execinf_stmt e m (Ssequence s1 s2) (t1 *** t2)
+  | execinf_Sifthenelse_true: forall e m a s1 s2 v1 t,
+      eval_expr e m a v1 ->
+      is_true v1 (typeof a) ->
+      execinf_stmt e m s1 t ->
+      execinf_stmt e m (Sifthenelse a s1 s2) t
+  | execinf_Sifthenelse_false: forall e m a s1 s2 v1 t,
+      eval_expr e m a v1 ->
+      is_false v1 (typeof a) ->
+      execinf_stmt e m s2 t ->
+      execinf_stmt e m (Sifthenelse a s1 s2) t
+  | execinf_Swhile_body: forall e m a v s t,
+      eval_expr e m a v ->
+      is_true v (typeof a) ->
+      execinf_stmt e m s t ->
+      execinf_stmt e m (Swhile a s) t
+  | execinf_Swhile_loop: forall e m a s v t1 m1 out1 t2,
+      eval_expr e m a v ->
+      is_true v (typeof a) ->
+      exec_stmt e m s t1 m1 out1 ->
+      out_normal_or_continue out1 ->
+      execinf_stmt e m1 (Swhile a s) t2 ->
+      execinf_stmt e m (Swhile a s) (t1 *** t2)
+  | execinf_Sdowhile_body: forall e m s a t,
+      execinf_stmt e m s t ->
+      execinf_stmt e m (Sdowhile a s) t
+  | execinf_Sdowhile_loop: forall e m s a m1 t1 t2 out1 v,
+      exec_stmt e m s t1 m1 out1 ->
+      out_normal_or_continue out1 ->
+      eval_expr e m1 a v ->
+      is_true v (typeof a) ->
+      execinf_stmt e m1 (Sdowhile a s) t2 ->
+      execinf_stmt e m (Sdowhile a s) (t1 *** t2)
+  | execinf_Sfor_start_1: forall e m s a1 a2 a3 t,
+      execinf_stmt e m a1 t ->
+      execinf_stmt e m (Sfor a1 a2 a3 s) t
+  | execinf_Sfor_start_2: forall e m s a1 a2 a3 m1 t1 t2,
+      a1 <> Sskip ->
+      exec_stmt e m a1 t1 m1 Out_normal ->
+      execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 ->
+      execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2)
+  | execinf_Sfor_body: forall e m s a2 a3 v t,
+      eval_expr e m a2 v ->
+      is_true v (typeof a2) ->
+      execinf_stmt e m s t ->
+      execinf_stmt e m (Sfor Sskip a2 a3 s) t
+  | execinf_Sfor_next: forall e m s a2 a3 v m1 t1 t2 out1,
+      eval_expr e m a2 v ->
+      is_true v (typeof a2) ->
+      exec_stmt e m s t1 m1 out1 ->
+      out_normal_or_continue out1 ->
+      execinf_stmt e m1 a3 t2 ->
+      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2)
+  | execinf_Sfor_loop: forall e m s a2 a3 v m1 m2 t1 t2 t3 out1,
+      eval_expr e m a2 v ->
+      is_true v (typeof a2) ->
+      exec_stmt e m s t1 m1 out1 ->
+      out_normal_or_continue out1 ->
+      exec_stmt e m1 a3 t2 m2 Out_normal ->
+      execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 ->
+      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3)
+  | execinf_Sswitch:   forall e m a t n sl,
+      eval_expr e m a (Vint n) ->
+      execinf_lblstmts e m (select_switch n sl) t ->
+      execinf_stmt e m (Sswitch a sl) t
+
+with execinf_lblstmts: env -> mem -> labeled_statements -> traceinf -> Prop :=
+  | execinf_LSdefault: forall e m s t,
+     execinf_stmt e m s t ->
+     execinf_lblstmts e m (LSdefault s) t
+  | execinf_LScase_body: forall e m n s ls t,
+     execinf_stmt e m s t ->
+     execinf_lblstmts e m (LScase n s ls) t
+  | execinf_LScase_fallthrough: forall e m n s ls t1 m1 t2,
+     exec_stmt e m s t1 m1 Out_normal ->
+     execinf_lblstmts e m1 ls t2 ->
+     execinf_lblstmts e m (LScase n s ls) (t1 *** t2)
+
+(** [evalinf_funcall ge m fd args t] holds if the invocation of function
+    [fd] on arguments [args] diverges, with observable trace [t]. *)
+
+with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
+  | evalinf_funcall_internal: forall m f vargs t e m1 lb m2,
+      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 lb ->
+      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      execinf_stmt e m2 f.(fn_body) t ->
+      evalinf_funcall m (Internal f) vargs t.
 
 End RELSEM.
 
-(** Execution of a whole program: [exec_program p t r]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] performs the input/output
-  operations described in the trace [t], and eventually returns value [r].
-*)
-
-Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
-  let ge := Genv.globalenv p in 
-  let m0 := Genv.init_mem p in
-  exists b, exists f, exists m1,
-  Genv.find_symbol ge p.(prog_main) = Some b /\
-  Genv.find_funct_ptr ge b = Some f /\
-  eval_funcall ge m0 f nil t m1 r.
+(** Execution of a whole program.  [exec_program p beh] holds
+  if the application of [p]'s main function to no arguments
+  in the initial memory state for [p] executes without errors and produces
+  the observable behaviour [beh]. *)
+
+Inductive exec_program (p: program): program_behavior -> Prop :=
+  | program_terminates: forall b f m1 t r,
+      let ge := Genv.globalenv p in 
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      eval_funcall ge m0 f nil t m1 (Vint r) ->
+      exec_program p (Terminates t r)
+  | program_diverges: forall b f t,
+      let ge := Genv.globalenv p in 
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      evalinf_funcall ge m0 f nil t ->
+      exec_program p (Diverges t).
+
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 7d805c38..7afe27f2 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -10,6 +10,7 @@ Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
 Require Cminor.
+Require Import Smallstep.
 
 (** Abstract syntax *)
 
@@ -17,10 +18,7 @@ Require Cminor.
   statements, functions and programs.  Expressions include
   reading global or local variables, reading store locations,
   arithmetic operations, function calls, and conditional expressions
-  (similar to [e1 ? e2 : e3] in C).  The [Elet] and [Eletvar] constructs
-  enable sharing the computations of subexpressions.  De Bruijn notation
-  is used: [Eletvar n] refers to the value bound by then [n+1]-th enclosing
-  [Elet] construct.
+  (similar to [e1 ? e2 : e3] in C). 
 
   Unlike in Cminor (the next intermediate language of the back-end),
   Csharpminor local variables reside in memory, and their addresses can
@@ -41,27 +39,19 @@ Inductive expr : Set :=
   | Eunop : unary_operation -> expr -> expr  (**r unary operation *)
   | Ebinop : binary_operation -> expr -> expr -> expr (**r binary operation *)
   | Eload : memory_chunk -> expr -> expr (**r memory read *)
-  | Ecall : signature -> expr -> exprlist -> expr (**r function call *)
-  | Econdition : expr -> expr -> expr -> expr (**r conditional expression *)
-  | Elet : expr -> expr -> expr         (**r let binding  *)
-  | Eletvar : nat -> expr               (**r reference to a let-bound variable *)
-  | Ealloc : expr -> expr               (**r memory allocation *)
-
-with exprlist : Set :=
-  | Enil: exprlist
-  | Econs: expr -> exprlist -> exprlist.
+  | Econdition : expr -> expr -> expr -> expr. (**r conditional expression *)
 
 (** Statements include expression evaluation, variable assignment,
-  memory stores, an if/then/else conditional,
+  memory stores, function calls, an if/then/else conditional,
   infinite loops, blocks and early block exits, and early function returns.
   [Sexit n] terminates prematurely the execution of the [n+1] enclosing
   [Sblock] statements. *)
 
 Inductive stmt : Set :=
   | Sskip: stmt
-  | Sexpr: expr -> stmt
   | Sassign : ident -> expr -> stmt
   | Sstore : memory_chunk -> expr -> expr -> stmt
+  | Scall : option ident -> signature -> expr -> list expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: expr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -136,19 +126,17 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat))
   | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem
   end.
 
-(** Four kinds of evaluation environments are involved:
+(** Three kinds of evaluation environments are involved:
 - [genv]: global environments, define symbols and functions;
 - [gvarenv]: map global variables to variable informations (type [var_kind]);
 - [env]: local environments, map local variables 
-    to memory blocks and variable informations;
-- [lenv]: let environments, map de Bruijn indices to values.
+    to memory blocks and variable informations.
 *)
 
 Definition genv := Genv.t fundef.
 Definition gvarenv := PTree.t var_kind.
 Definition env := PTree.t (block * var_kind).
 Definition empty_env : env := PTree.empty (block * var_kind).
-Definition letenv := list val.
 
 Definition sizeof (lv: var_kind) : Z :=
   match lv with
@@ -252,111 +240,80 @@ Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop :=
       PTree.get id (global_var_env prg) = Some (Vscalar chunk) ->
       eval_var_ref e id b chunk.
 
-(** Evaluation of an expression: [eval_expr prg le e m a t m' v] states
-  that expression [a], in initial memory state [m], evaluates to value
-  [v].  [m'] is the final memory state, respectively, reflecting
-  memory stores possibly performed by [a].  [t] is the trace of input/output
-  events generated during the evaluation.
-  [e] and [le] are the local environment and let environment respectively. *)
-
-Inductive eval_expr:
-         letenv -> env ->
-         mem -> expr -> trace -> mem -> val -> Prop :=
-  | eval_Evar:
-      forall le e m id b chunk v,
+(** Evaluation of an expression: [eval_expr prg e m a v] states
+  that expression [a], in initial memory state [m] and local
+  environment [e], evaluates to value [v]. *)
+
+Section EVAL_EXPR.
+
+Variable e: env.
+Variable m: mem.
+
+Inductive eval_expr: expr -> val -> Prop :=
+  | eval_Evar: forall id b chunk v,
       eval_var_ref e id b chunk ->
       Mem.load chunk m b 0 = Some v ->
-      eval_expr le e m (Evar id) E0 m v
-  | eval_Eaddrof:
-      forall le e m id b,
+      eval_expr (Evar id) v
+  | eval_Eaddrof: forall id b,
       eval_var_addr e id b ->
-      eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero)
-  | eval_Econst:
-      forall le e m cst v,
+      eval_expr (Eaddrof id) (Vptr b Int.zero)
+  | eval_Econst: forall cst v,
       eval_constant cst = Some v ->
-      eval_expr le e m (Econst cst) E0 m v
-  | eval_Eunop:
-      forall le e m op a t m1 v1 v,
-      eval_expr le e m a t m1 v1 ->
+      eval_expr (Econst cst) v
+  | eval_Eunop: forall op a1 v1 v,
+      eval_expr a1 v1 ->
       eval_unop op v1 = Some v ->
-      eval_expr le e m (Eunop op a) t m1 v
-  | eval_Ebinop:
-      forall le e m op a1 a2 t1 m1 v1 t2 m2 v2 t v,
-      eval_expr le e m a1 t1 m1 v1 ->
-      eval_expr le e m1 a2 t2 m2 v2 ->
-      eval_binop op v1 v2 m2 = Some v ->
-      t = t1 ** t2 ->
-      eval_expr le e m (Ebinop op a1 a2) t m2 v
-  | eval_Eload:
-      forall le e m chunk a t m1 v1 v,
-      eval_expr le e m a t m1 v1 ->
-      Mem.loadv chunk m1 v1 = Some v ->
-      eval_expr le e m (Eload chunk a) t m1 v
-  | eval_Ecall:
-      forall le e m sig a bl t1 m1 t2 m2 t3 m3 vf vargs vres f t,
-      eval_expr le e m a t1 m1 vf ->
-      eval_exprlist le e m1 bl t2 m2 vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall m2 f vargs t3 m3 vres ->
-      t = t1 ** t2 ** t3 ->
-      eval_expr le e m (Ecall sig a bl) t m3 vres
-  | eval_Econdition_true:
-      forall le e m a b c t1 m1 v1 t2 m2 v2 t,
-      eval_expr le e m a t1 m1 v1 ->
-      Val.is_true v1 ->
-      eval_expr le e m1 b t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr le e m (Econdition a b c) t m2 v2
-  | eval_Econdition_false:
-      forall le e m a b c t1 m1 v1 t2 m2 v2 t,
-      eval_expr le e m a t1 m1 v1 ->
-      Val.is_false v1 ->
-      eval_expr le e m1 c t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr le e m (Econdition a b c) t m2 v2
-  | eval_Elet:
-      forall le e m a b t1 m1 v1 t2 m2 v2 t,
-      eval_expr le e m a t1 m1 v1 ->
-      eval_expr (v1::le) e m1 b t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr le e m (Elet a b) t m2 v2
-  | eval_Eletvar:
-      forall le e m n v,
-      nth_error le n = Some v ->
-      eval_expr le e m (Eletvar n) E0 m v
-  | eval_Ealloc:
-      forall le e m a t m1 n m2 b,
-      eval_expr le e m a t m1 (Vint n) ->
-      Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
-      eval_expr le e m (Ealloc a) t m2 (Vptr b Int.zero)
+      eval_expr (Eunop op a1) v
+  | eval_Ebinop: forall op a1 a2 v1 v2 v,
+      eval_expr a1 v1 ->
+      eval_expr a2 v2 ->
+      eval_binop op v1 v2 m = Some v ->
+      eval_expr (Ebinop op a1 a2) v
+  | eval_Eload: forall chunk a v1 v,
+      eval_expr a v1 ->
+      Mem.loadv chunk m v1 = Some v ->
+      eval_expr (Eload chunk a) v
+  | eval_Econdition: forall a b c v1 vb1 v2,
+      eval_expr a v1 ->
+      Val.bool_of_val v1 vb1 ->
+      eval_expr (if vb1 then b else c) v2 ->
+      eval_expr (Econdition a b c) v2.
 
 (** Evaluation of a list of expressions:
-  [eval_exprlist prg le al m a t m' vl]
-  states that the list [al] of expressions evaluate 
-  to the list [vl] of values.
-  The other parameters are as in [eval_expr].
-*)
+  [eval_exprlist prg e m al vl] states that the list [al] of
+  expressions evaluate to the list [vl] of values.  The other
+  parameters are as in [eval_expr]. *)
 
-with eval_exprlist:
-         letenv -> env ->
-         mem -> exprlist -> trace ->
-         mem -> list val -> Prop :=
+Inductive eval_exprlist: list expr -> list val -> Prop :=
   | eval_Enil:
-      forall le e m,
-      eval_exprlist le e m Enil E0 m nil
-  | eval_Econs:
-      forall le e m a bl t1 m1 v t2 m2 vl t,
-      eval_expr le e m a t1 m1 v ->
-      eval_exprlist le e m1 bl t2 m2 vl ->
-      t = t1 ** t2 ->
-      eval_exprlist le e m (Econs a bl) t m2 (v :: vl)
+      eval_exprlist nil nil
+  | eval_Econs: forall a1 al v1 vl,
+      eval_expr a1 v1 -> eval_exprlist al vl ->
+      eval_exprlist (a1 :: al) (v1 :: vl).
+
+End EVAL_EXPR.
+
+(** Execution of an assignment to a variable. *)
+
+Inductive exec_assign: env -> mem -> ident -> val -> mem -> Prop :=
+  exec_assign_intro: forall e m id v b chunk m',
+    eval_var_ref e id b chunk ->
+    Mem.store chunk m b 0 v = Some m' ->
+    exec_assign e m id v m'.
+
+Inductive exec_opt_assign: env -> mem -> option ident -> val -> mem -> Prop :=
+  | exec_assign_none: forall e m v,
+      exec_opt_assign e m None v m
+  | exec_assign_some: forall e m id v m',
+      exec_assign e m id v m' ->
+      exec_opt_assign e m (Some id) v m'.
 
 (** Evaluation of a function invocation: [eval_funcall prg m f args t m' res]
   means that the function [f], applied to the arguments [args] in
   memory state [m], returns the value [res] in modified memory state [m'].
-*)
-with eval_funcall:
+  [t] is the trace of observable events performed during the call. *)
+
+Inductive eval_funcall:
         mem -> fundef -> list val -> trace ->
         mem -> val -> Prop :=
   | eval_funcall_internal:
@@ -374,6 +331,8 @@ with eval_funcall:
 
 (** Execution of a statement: [exec_stmt prg e m s t m' out]
   means that statement [s] executes with outcome [out].
+  [m] is the initial memory state, [m'] the final memory state,
+  and [t] the trace of events performed.
   The other parameters are as in [eval_expr]. *)
 
 with exec_stmt:
@@ -383,23 +342,26 @@ with exec_stmt:
   | exec_Sskip:
       forall e m,
       exec_stmt e m Sskip E0 m Out_normal
-  | exec_Sexpr:
-      forall e m a t m1 v,
-      eval_expr nil e m a t m1 v ->
-      exec_stmt e m (Sexpr a) t m1 Out_normal
-  | eval_Sassign:
-      forall e m id a t m1 b chunk v m2,
-      eval_expr nil e m a t m1 v ->
-      eval_var_ref e id b chunk ->
-      Mem.store chunk m1 b 0 v = Some m2 ->
-      exec_stmt e m (Sassign id a) t m2 Out_normal
-  | eval_Sstore:
-      forall e m chunk a b t1 m1 v1 t2 m2 v2 t3 m3,
-      eval_expr nil e m a t1 m1 v1 ->
-      eval_expr nil e m1 b t2 m2 v2 ->
-      Mem.storev chunk m2 v1 v2 = Some m3 ->
-      t3 = t1 ** t2 ->
-      exec_stmt e m (Sstore chunk a b) t3 m3 Out_normal
+  | exec_Sassign:
+      forall e m id a v m',
+      eval_expr e m a v ->
+      exec_assign e m id v m' ->
+      exec_stmt e m (Sassign id a) E0 m' Out_normal
+  | exec_Sstore:
+      forall e m chunk a b v1 v2 m',
+      eval_expr e m a v1 ->
+      eval_expr e m b v2 ->
+      Mem.storev chunk m v1 v2 = Some m' ->
+      exec_stmt e m (Sstore chunk a b) E0 m' Out_normal
+  | exec_Scall:
+      forall e m optid sig a bl vf vargs f t m1 vres m2,
+      eval_expr e m a vf ->
+      eval_exprlist e m bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      eval_funcall m f vargs t m1 vres ->
+      exec_opt_assign e m1 optid vres m2 ->
+      exec_stmt e m (Scall optid sig a bl) t m2 Out_normal
   | exec_Sseq_continue:
       forall e m s1 s2 t1 t2 m1 m2 t out,
       exec_stmt e m s1 t1 m1 Out_normal ->
@@ -411,20 +373,12 @@ with exec_stmt:
       exec_stmt e m s1 t1 m1 out ->
       out <> Out_normal ->
       exec_stmt e m (Sseq s1 s2) t1 m1 out
-  | exec_Sifthenelse_true:
-      forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t,
-      eval_expr nil e m a t1 m1 v1 ->
-      Val.is_true v1 ->
-      exec_stmt e m1 sl1 t2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out
-  | exec_Sifthenelse_false:
-      forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t,
-      eval_expr nil e m a t1 m1 v1 ->
-      Val.is_false v1 ->
-      exec_stmt e m1 sl2 t2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out
+  | exec_Sifthenelse:
+      forall e m a sl1 sl2 v vb t m' out,
+      eval_expr e m a v ->
+      Val.bool_of_val v vb ->
+      exec_stmt e m (if vb then sl1 else sl2) t m' out ->
+      exec_stmt e m (Sifthenelse a sl1 sl2) t m' out
   | exec_Sloop_loop:
       forall e m sl t1 m1 t2 m2 out t,
       exec_stmt e m sl t1 m1 Out_normal ->
@@ -444,35 +398,166 @@ with exec_stmt:
       forall e m n,
       exec_stmt e m (Sexit n) E0 m (Out_exit n)
   | exec_Sswitch:
-      forall e m a cases default t1 m1 n,
-      eval_expr nil e m a t1 m1 (Vint n) ->
+      forall e m a cases default n,
+      eval_expr e m a (Vint n) ->
       exec_stmt e m (Sswitch a cases default)
-               t1 m1 (Out_exit (switch_target n default cases))
+               E0 m (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
       forall e m,
       exec_stmt e m (Sreturn None) E0 m (Out_return None)
   | exec_Sreturn_some:
-      forall e m a t1 m1 v,
-      eval_expr nil e m a t1 m1 v ->
-      exec_stmt e m (Sreturn (Some a)) t1 m1 (Out_return (Some v)).
-
-Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop
-  with eval_exprlist_ind4 := Minimality for eval_exprlist Sort Prop
-  with eval_funcall_ind4 := Minimality for eval_funcall Sort Prop
-  with exec_stmt_ind4 := Minimality for exec_stmt Sort Prop.
+      forall e m a v,
+      eval_expr e m a v ->
+      exec_stmt e m (Sreturn (Some a)) E0 m (Out_return (Some v)).
+
+Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop
+  with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop.
+
+(** Coinductive semantics for divergence. *)
+
+Inductive block_seq_context: (stmt -> stmt) -> Prop :=
+  | block_seq_context_base_1:
+      block_seq_context (fun x => Sblock x)
+  | block_seq_context_base_2: forall s,
+      block_seq_context (fun x => Sseq x s)
+  | block_seq_context_ctx_1: forall ctx,
+      block_seq_context ctx ->
+      block_seq_context (fun x => Sblock (ctx x))
+  | block_seq_context_ctx_2: forall s ctx,
+      block_seq_context ctx ->
+      block_seq_context (fun x => Sseq (ctx x) s).
+
+CoInductive evalinf_funcall:
+        mem -> fundef -> list val -> traceinf -> Prop :=
+  | evalinf_funcall_internal:
+      forall m f vargs e m1 lb m2 t,
+      list_norepet (fn_params_names f ++ fn_vars_names f) ->
+      alloc_variables empty_env m (fn_variables f) e m1 lb ->
+      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      execinf_stmt e m2 f.(fn_body) t ->
+      evalinf_funcall m (Internal f) vargs t
+
+with execinf_stmt:
+         env -> mem -> stmt -> traceinf -> Prop :=
+  | execinf_Scall:
+      forall e m optid sig a bl vf vargs f t,
+      eval_expr e m a vf ->
+      eval_exprlist e m bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      evalinf_funcall m f vargs t ->
+      execinf_stmt e m (Scall optid sig a bl) t
+  | execinf_Sseq_1:
+      forall e m s1 s2 t,
+      execinf_stmt e m s1 t ->
+      execinf_stmt e m (Sseq s1 s2) t
+  | execinf_Sseq_2:
+      forall e m s1 s2 t1 t2 m1 t,
+      exec_stmt e m s1 t1 m1 Out_normal ->
+      execinf_stmt e m1 s2 t2 ->
+      t = t1 *** t2 ->
+      execinf_stmt e m (Sseq s1 s2) t
+  | execinf_Sifthenelse:
+      forall e m a sl1 sl2 v vb t,
+      eval_expr e m a v ->
+      Val.bool_of_val v vb ->
+      execinf_stmt e m (if vb then sl1 else sl2) t ->
+      execinf_stmt e m (Sifthenelse a sl1 sl2) t
+  | execinf_Sloop_body:
+      forall e m sl t,
+      execinf_stmt e m sl t ->
+      execinf_stmt e m (Sloop sl) t
+  | execinf_Sloop_loop:
+      forall e m sl t1 m1 t2 t,
+      exec_stmt e m sl t1 m1 Out_normal ->
+      execinf_stmt e m1 (Sloop sl) t2 ->
+      t = t1 *** t2 ->
+      execinf_stmt e m (Sloop sl) t
+  | execinf_Sblock:
+      forall e m sl t,
+      execinf_stmt e m sl t ->
+      execinf_stmt e m (Sblock sl) t
+  | execinf_stutter:
+      forall n e m s t,
+      execinf_stmt_N n e m s t ->
+      execinf_stmt e m s t
+  | execinf_Sloop_block:
+      forall e m sl t1 m1 t2 t,
+      exec_stmt e m sl t1 m1 Out_normal ->
+      execinf_stmt e m1 (Sblock (Sloop sl)) t2 ->
+      t = t1 *** t2 ->
+      execinf_stmt e m (Sloop sl) t
+
+with execinf_stmt_N:
+         nat -> env -> mem -> stmt -> traceinf -> Prop :=
+  | execinf_context: forall n e m s t ctx,
+      execinf_stmt e m s t -> block_seq_context ctx ->
+      execinf_stmt_N n e m (ctx s) t
+  | execinf_sleep: forall n e m s t,
+      execinf_stmt_N n e m s t ->
+      execinf_stmt_N (S n) e m s t.
+
+Lemma execinf_stmt_N_inv:
+  forall n e m s t,
+  execinf_stmt_N n e m s t ->
+  match s with
+  | Sblock s1 => execinf_stmt e m s1 t
+  | Sseq s1 s2 => execinf_stmt e m s1 t
+  | _ => False
+  end.
+Proof.
+  assert (BASECASE: forall e m s t ctx,
+          execinf_stmt e m s t -> block_seq_context ctx ->
+          match ctx s with
+          | Sblock s1 => execinf_stmt e m s1 t
+          | Sseq s1 s2 => execinf_stmt e m s1 t
+          | _ => False
+          end).
+  intros. inv H0.
+  auto.
+  auto.
+  apply execinf_stutter with O. apply execinf_context; eauto. 
+  apply execinf_stutter with O. apply execinf_context; eauto.
+
+  induction n; intros; inv H.
+  apply BASECASE; auto.
+  apply BASECASE; auto.
+  eapply IHn; eauto.
+Qed.
+
+Lemma execinf_Sblock_inv:
+  forall e m s t,
+  execinf_stmt e m (Sblock s) t ->
+  execinf_stmt e m s t.
+Proof.
+  intros. inv H.
+  auto.
+  exact (execinf_stmt_N_inv _ _ _ _ _ H0). 
+Qed.
 
 End RELSEM.
 
-(** Execution of a whole program: [exec_program p t r]
+(** Execution of a whole program: [exec_program p beh]
   holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] performs the events described
-  in trace [t] and eventually returns value [r]. *)
-
-Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
-  let ge := Genv.globalenv p in
-  let m0 := Genv.init_mem p in
-  exists b, exists f, exists m,
-  Genv.find_symbol ge p.(prog_main) = Some b /\
-  Genv.find_funct_ptr ge b = Some f /\
-  funsig f = mksignature nil (Some Tint) /\
-  eval_funcall p m0 f nil t m r.
+  in the initial memory state for [p] has [beh] as observable
+  behavior. *)
+
+Inductive exec_program (p: program): program_behavior -> Prop :=
+  | program_terminates:
+      forall b f t m r,
+      let ge := Genv.globalenv p in
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = mksignature nil (Some Tint) ->
+      eval_funcall p m0 f nil t m (Vint r) ->
+      exec_program p (Terminates t r)
+  | program_diverges:
+      forall b f t,
+      let ge := Genv.globalenv p in
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = mksignature nil (Some Tint) ->
+      evalinf_funcall p m0 f nil t ->
+      exec_program p (Diverges t).
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 937ea78a..6ec3757b 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -253,6 +253,14 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
 
 (** * Reading and writing variables *)
 
+(** Determine if a C expression is a variable *)
+
+Definition is_variable (e: Csyntax.expr) : option ident :=
+  match e with
+  | Expr (Csyntax.Evar id) _ => Some id
+  | _ => None
+  end.
+
 (** [var_get id ty] returns Csharpminor code that evaluates to the
    value of C variable [id] with type [ty].  Note that 
    C variables of array or function type evaluate to the address
@@ -277,7 +285,19 @@ Definition var_set (id: ident) (ty: type) (rhs: expr) :=
   | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil)
   end.
 
-(** * Translation of operators *)
+(** Auxiliary for translating call statements *)
+
+Definition transl_lhs_call (opta: option Csyntax.expr) : res (option ident) :=
+  match opta with
+  | None => OK None
+  | Some a =>
+      match is_variable a with
+      | None => Error (msg "LHS of function call is not a variable")
+      | Some id => OK (Some id)
+      end
+  end.
+
+(** ** Translation of operators *)
 
 Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr :=
   match op with
@@ -350,15 +370,6 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr :=
       do tc <- transl_expr c;
       do ts <- make_add tb (typeof b) tc (typeof c);
       make_load ts ty
-  | Expr (Csyntax.Ecall b cl) _ =>
-      match (classify_fun (typeof b)) with
-      | fun_case_f args res =>
-          do tb <- transl_expr b;
-          do tcl <- transl_exprlist cl;
-          OK(Ecall (signature_of_type args res) tb tcl)
-      | _ =>
-          Error(msg "Cshmgen.transl_expr(call)")
-      end 
   | Expr (Csyntax.Eandbool b c) _ =>
       do tb <- transl_expr b;
       do tc <- transl_expr c;
@@ -413,31 +424,23 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : res expr :=
       end
   | _ => 
       Error(msg "Cshmgen.transl_lvalue")
-  end
+  end.
 
 (** [transl_exprlist al] returns a list of Csharpminor expressions
    that compute the values of the list [al] of Csyntax expressions.
    Used for function applications. *)
 
-with transl_exprlist (al: Csyntax.exprlist): res exprlist :=
+Fixpoint transl_exprlist (al: list Csyntax.expr): res (list expr) :=
   match al with
-  | Csyntax.Enil => OK Enil
-  | Csyntax.Econs a1 a2 =>
+  | nil => OK nil
+  | a1 :: a2 =>
       do ta1 <- transl_expr a1;
       do ta2 <- transl_exprlist a2;
-      OK (Econs ta1 ta2)
+      OK (ta1 :: ta2)
   end.
 
 (** * Translation of statements *)
 
-(** Determine if a C expression is a variable *)
-
-Definition is_variable (e: Csyntax.expr) : option ident :=
-  match e with
-  | Expr (Csyntax.Evar id) _ => Some id
-  | _ => None
-  end.
-
 (** [exit_if_false e] return the statement that tests the boolean
    value of the Clight expression [e].  If [e] evaluates to false,
    an [exit 0] is performed.  If [e] evaluates to true, the generated
@@ -512,15 +515,18 @@ Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int
   | LScase ni _ rem => (ni, k) :: switch_table rem (k+1)
   end.
 
+Definition is_Sskip:
+  forall (s: Csyntax.statement), {s = Csyntax.Sskip} + {s <> Csyntax.Sskip}.
+Proof.
+  destruct s; ((left; reflexivity) || (right; congruence)).
+Qed.
+
 Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : res stmt :=
   match s with
   | Csyntax.Sskip =>
       OK Sskip
-  | Csyntax.Sexpr e =>
-      do te <- transl_expr e;
-      OK (Sexpr te)
   | Csyntax.Sassign b c =>
-      match (is_variable b) with
+      match is_variable b with
       | Some id =>
           do tc <- transl_expr c;
           var_set id (typeof b) tc
@@ -529,6 +535,15 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : r
           do tc <- transl_expr c;
           make_store tb (typeof b) tc
       end 
+  | Csyntax.Scall opta b cl =>
+      match classify_fun (typeof b) with
+      | fun_case_f args res =>
+          do optid <- transl_lhs_call opta;
+          do tb <- transl_expr b;
+          do tcl <- transl_exprlist cl;
+          OK(Scall optid (signature_of_type args res) tb tcl)
+      | _ => Error(msg "Cshmgen.transl_stmt(call)")
+      end
   | Csyntax.Ssequence s1 s2 =>
       do ts1 <- transl_statement nbrk ncnt s1;
       do ts2 <- transl_statement nbrk ncnt s2;
@@ -547,11 +562,17 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : r
       do ts1 <- transl_statement 1%nat 0%nat s1;
       OK (Sblock (Sloop (Sseq (Sblock ts1) te)))
   | Csyntax.Sfor e1 e2 e3 s1 =>
-      do te1 <- transl_statement nbrk ncnt e1;
-      do te2 <- exit_if_false e2;
-      do te3 <- transl_statement nbrk ncnt e3;
-      do ts1 <- transl_statement 1%nat 0%nat s1;
-      OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))
+      if is_Sskip e1 then
+       (do te2 <- exit_if_false e2;
+        do te3 <- transl_statement nbrk ncnt e3;
+        do ts1 <- transl_statement 1%nat 0%nat s1;
+        OK (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))
+      else
+       (do te1 <- transl_statement nbrk ncnt e1;
+        do te2 <- exit_if_false e2;
+        do te3 <- transl_statement nbrk ncnt e3;
+        do ts1 <- transl_statement 1%nat 0%nat s1;
+        OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))))
   | Csyntax.Sbreak =>
       OK (Sexit nbrk)
   | Csyntax.Scontinue =>
@@ -579,7 +600,7 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt)
       transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts))
   end.
 
-(** * Translation of functions and programs *)
+(*** Translation of functions *)
 
 Definition prefix_var_name (id: ident) : errmsg :=
   MSG "In local variable " :: CTX id :: MSG ":\n" :: nil.
@@ -603,6 +624,8 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef :=
       OK(AST.External (external_function id args res))
   end.
 
+(** ** Translation of programs *)
+
 Definition transl_globvar (ty: type) := var_kind_of_type ty.
 
 Definition transl_program (p: Csyntax.program) : res program :=
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index b86b09bf..9930ef80 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -175,8 +175,8 @@ Proof.
 Qed.
 
 Lemma transl_expr_lvalue:
-  forall ge e m1 a ty t m2 loc ofs ta,
-  Csem.eval_lvalue ge e m1 (Expr a ty) t m2 loc ofs ->
+  forall ge e m a ty loc ofs ta,
+  Csem.eval_lvalue ge e m (Expr a ty) loc ofs ->
   transl_expr (Expr a ty) = OK ta ->
   (exists id, a = Csyntax.Evar id /\ var_get id ty = OK ta) \/
   (exists tb, transl_lvalue (Expr a ty) = OK tb /\
@@ -188,28 +188,44 @@ Proof.
   monadInv H0. right. exists x; split; auto. 
   simpl. monadInv H0. right. exists x1; split; auto. 
   simpl. rewrite EQ; rewrite EQ1. simpl. auto.
-  rewrite H6 in H0. monadInv H0. right.  
+  rewrite H4 in H0. monadInv H0. right.  
   exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto.
-  simpl. rewrite H6. rewrite EQ. rewrite EQ1. auto.
-  rewrite H10 in H0. monadInv H0. right.
+  simpl. rewrite H4. rewrite EQ. rewrite EQ1. auto.
+  rewrite H6 in H0. monadInv H0. right.
   exists x; split; auto. 
-  simpl. rewrite H10. auto.
+  simpl. rewrite H6. auto.
 Qed.
 
 Lemma transl_stmt_Sfor_start:
   forall nbrk ncnt s1 e2 s3 s4 ts,
   transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = OK ts ->
+  s1 <> Csyntax.Sskip ->
   exists ts1, exists ts2,
     ts = Sseq ts1 ts2
   /\ transl_statement nbrk ncnt s1 = OK ts1
-  /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = OK (Sseq Sskip ts2).
+  /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = OK ts2.
 Proof.
-  intros. monadInv H. econstructor; econstructor.
+  intros. simpl in H. destruct (is_Sskip s1). contradiction.
+  monadInv H. econstructor; econstructor.
   split. reflexivity. split. auto. simpl.
+  destruct (is_Sskip Csyntax.Sskip). 2: tauto. 
   rewrite EQ1; rewrite EQ0; rewrite EQ2; auto.
 Qed.
 
-(** Properties related to [switch] constructs. *)
+Open Local Scope error_monad_scope.
+
+Lemma transl_stmt_Sfor_not_start:
+  forall nbrk ncnt e2 e3 s1,
+  transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 e3 s1) =
+    (do te2 <- exit_if_false e2;
+     do te3 <- transl_statement nbrk ncnt e3;
+     do ts1 <- transl_statement 1%nat 0%nat s1;
+     OK (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))).
+Proof.
+  intros. simpl. destruct (is_Sskip Csyntax.Sskip). auto. congruence.
+Qed.
+
+(** Properties related to switch constructs *)
 
 Fixpoint lblstmts_length (sl: labeled_statements) : nat :=
   match sl with
@@ -233,4 +249,33 @@ Proof.
   induction sl; intro; simpl. auto. decEq; auto. 
 Qed.
 
+Lemma block_seq_context_compose:
+  forall ctx2 ctx1,
+  block_seq_context ctx1 ->
+  block_seq_context ctx2 ->
+  block_seq_context (fun x => ctx1 (ctx2 x)).
+Proof.
+  induction 1; intros; constructor; auto.
+Qed.
+
+Lemma transl_lblstmts_context:
+  forall sl nbrk ncnt body s,
+  transl_lblstmts nbrk ncnt sl body = OK s ->
+  exists ctx, block_seq_context ctx /\ s = ctx body.
+Proof.
+  induction sl; simpl; intros.
+  monadInv H. exists (fun y => Sblock (Sseq y x)); split.
+  apply block_seq_context_ctx_1. apply block_seq_context_base_2.
+  auto.
+  monadInv H. exploit IHsl; eauto. intros [ctx [A B]].
+  exists (fun y => ctx (Sblock (Sseq y x))); split.
+  apply block_seq_context_compose with
+    (ctx1 := ctx)
+    (ctx2 := fun y => Sblock (Sseq y x)).
+  auto. apply block_seq_context_ctx_1. apply block_seq_context_base_2. 
+  auto.
+Qed.
+
+
+
 
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index a75621ca..aa4e391a 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -60,17 +60,17 @@ Qed.
 (** * Correctness of Csharpminor construction functions *)
 
 Lemma make_intconst_correct:
-  forall n le e m1,
-  Csharpminor.eval_expr tprog le e m1 (make_intconst n) E0 m1 (Vint n).
+  forall n e m,
+  eval_expr tprog e m (make_intconst n) (Vint n).
 Proof.
-  intros. unfold make_intconst. econstructor. constructor.  
+  intros. unfold make_intconst. econstructor. reflexivity. 
 Qed.
 
 Lemma make_floatconst_correct:
-  forall n le e m1,
-  Csharpminor.eval_expr tprog le e m1 (make_floatconst n) E0 m1 (Vfloat n).
+  forall n e m,
+  eval_expr tprog e m (make_floatconst n) (Vfloat n).
 Proof.
-  intros. unfold make_floatconst. econstructor. constructor.  
+  intros. unfold make_floatconst. econstructor. reflexivity. 
 Qed.
 
 Hint Resolve make_intconst_correct make_floatconst_correct
@@ -88,18 +88,18 @@ Proof.
 Qed.
 
 Lemma make_boolean_correct_true:
- forall le e m1 a t m2 v ty,
-  Csharpminor.eval_expr tprog le e m1 a t m2 v ->
+ forall e m a v ty,
+  eval_expr tprog e m a v ->
   is_true v ty ->
   exists vb,
-    Csharpminor.eval_expr tprog le e m1 (make_boolean a ty) t m2 vb
+    eval_expr tprog e m (make_boolean a ty) vb
     /\ Val.is_true vb.
 Proof.
   intros until ty; intros EXEC VTRUE.
   destruct ty; simpl;
   try (exists v; intuition; inversion VTRUE; simpl; auto; fail).
   exists Vtrue; split.
-  econstructor; eauto with cshm. 
+  eapply eval_Ebinop; eauto with cshm. 
   inversion VTRUE; simpl. 
   replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)).
   rewrite Float.eq_zero_false. reflexivity. auto.
@@ -108,18 +108,18 @@ Proof.
 Qed.
 
 Lemma make_boolean_correct_false:
- forall le e m1 a t m2 v ty,
-  Csharpminor.eval_expr tprog le e m1 a t m2 v ->
+ forall e m a v ty,
+  eval_expr tprog e m a v ->
   is_false v ty ->
   exists vb,
-    Csharpminor.eval_expr tprog le e m1 (make_boolean a ty) t m2 vb
+    eval_expr tprog e m (make_boolean a ty) vb
     /\ Val.is_false vb.
 Proof.
   intros until ty; intros EXEC VFALSE.
   destruct ty; simpl;
   try (exists v; intuition; inversion VFALSE; simpl; auto; fail).
   exists Vfalse; split.
-  econstructor; eauto with cshm. 
+  eapply eval_Ebinop; eauto with cshm. 
   inversion VFALSE; simpl. 
   replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)).
   rewrite Float.eq_zero_true. reflexivity. 
@@ -128,38 +128,38 @@ Proof.
 Qed.
 
 Lemma make_neg_correct:
-  forall a tya c ta va v le e m1 m2,
+  forall a tya c va v e m,
   sem_neg va tya = Some v ->
   make_neg a tya = OK c ->  
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m1 c ta m2 v.
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m c v.
 Proof.
-  intros until m2; intro SEM. unfold make_neg. 
+  intros until m; intro SEM. unfold make_neg. 
   functional inversion SEM; intros.
-  inversion H4. econstructor; eauto with cshm.
+  inversion H4. eapply eval_Eunop; eauto with cshm.
   inversion H4. eauto with cshm.
 Qed.
 
 Lemma make_notbool_correct:
-  forall a tya c ta va v le e m1 m2,
+  forall a tya c va v e m,
   sem_notbool va tya = Some v ->
   make_notbool a tya = c ->  
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m1 c ta m2 v.
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m c v.
 Proof.
-  intros until m2; intro SEM. unfold make_notbool. 
+  intros until m; intro SEM. unfold make_notbool. 
   functional inversion SEM; intros; inversion H4; simpl;
   eauto with cshm.
 Qed.
 
 Lemma make_notint_correct:
-  forall a tya c ta va v le e m1 m2,
+  forall a tya c va v e m,
   sem_notint va = Some v ->
   make_notint a tya = c ->  
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m1 c ta m2 v.
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m c v.
 Proof.
-  intros until m2; intro SEM. unfold make_notint. 
+  intros until m; intro SEM. unfold make_notint. 
   functional inversion SEM; intros. 
   inversion H2; eauto with cshm.
 Qed.
@@ -167,143 +167,141 @@ Qed.
 Definition binary_constructor_correct
     (make: expr -> type -> expr -> type -> res expr)
     (sem: val -> type -> val -> type -> option val): Prop :=
-  forall a tya b tyb c ta va tb vb v le e m1 m2 m3,
+  forall a tya b tyb c va vb v e m,
   sem va tya vb tyb = Some v ->
   make a tya b tyb = OK c ->  
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m2 b tb m3 vb ->
-  eval_expr tprog le e m1 c (ta ** tb) m3 v.
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m b vb ->
+  eval_expr tprog e m c v.
 
 Definition binary_constructor_correct'
     (make: expr -> type -> expr -> type -> res expr)
     (sem: val -> val -> option val): Prop :=
-  forall a tya b tyb c ta va tb vb v le e m1 m2 m3,
+  forall a tya b tyb c va vb v e m,
   sem va vb = Some v ->
   make a tya b tyb = OK c ->  
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m2 b tb m3 vb ->
-  eval_expr tprog le e m1 c (ta ** tb) m3 v.
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m b vb ->
+  eval_expr tprog e m c v.
 
 Lemma make_add_correct: binary_constructor_correct make_add sem_add.
 Proof.
-  red; intros until m3. intro SEM. unfold make_add. 
+  red; intros until m. intro SEM. unfold make_add. 
   functional inversion SEM; rewrite H0; intros.
   inversion H7. eauto with cshm. 
   inversion H7. eauto with cshm.
   inversion H7. 
-  econstructor. eauto. 
-  econstructor. eauto with cshm. eauto.
+  eapply eval_Ebinop. eauto. 
+  eapply eval_Ebinop. eauto with cshm. eauto.
   simpl. reflexivity. reflexivity. 
-  simpl. reflexivity. traceEq.
 Qed.
 
 Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub.
 Proof.
-  red; intros until m3. intro SEM. unfold make_sub. 
+  red; intros until m. intro SEM. unfold make_sub. 
   functional inversion SEM; rewrite H0; intros;
   inversion H7; eauto with cshm. 
-  econstructor. eauto. 
-  econstructor. eauto with cshm. eauto.
+  eapply eval_Ebinop. eauto. 
+  eapply eval_Ebinop. eauto with cshm. eauto.
   simpl. reflexivity. reflexivity. 
-  simpl. reflexivity. traceEq.
-  inversion H9. econstructor. 
-  econstructor; eauto. 
+  inversion H9. eapply eval_Ebinop. 
+  eapply eval_Ebinop; eauto. 
   simpl. unfold eq_block; rewrite H3. reflexivity.
-  eauto with cshm. simpl. rewrite H8. reflexivity. traceEq.
+  eauto with cshm. simpl. rewrite H8. reflexivity.
 Qed.
 
 Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul.
 Proof.
-  red; intros until m3. intro SEM. unfold make_mul. 
+  red; intros until m. intro SEM. unfold make_mul. 
   functional inversion SEM; rewrite H0; intros;
   inversion H7; eauto with cshm. 
 Qed.
 
 Lemma make_div_correct: binary_constructor_correct make_div sem_div.
 Proof.
-  red; intros until m3. intro SEM. unfold make_div. 
+  red; intros until m. intro SEM. unfold make_div. 
   functional inversion SEM; rewrite H0; intros.
-  inversion H8. econstructor; eauto with cshm. 
+  inversion H8. eapply eval_Ebinop; eauto with cshm. 
   simpl. rewrite H7; auto.
-  inversion H8. econstructor; eauto with cshm. 
+  inversion H8. eapply eval_Ebinop; eauto with cshm. 
   simpl. rewrite H7; auto.
   inversion H7; eauto with cshm. 
 Qed.
 
 Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod.
-  red; intros until m3. intro SEM. unfold make_mod. 
+  red; intros until m. intro SEM. unfold make_mod. 
   functional inversion SEM; rewrite H0; intros.
-  inversion H8. econstructor; eauto with cshm. 
+  inversion H8. eapply eval_Ebinop; eauto with cshm. 
   simpl. rewrite H7; auto.
-  inversion H8. econstructor; eauto with cshm. 
+  inversion H8. eapply eval_Ebinop; eauto with cshm. 
   simpl. rewrite H7; auto.
 Qed.
 
 Lemma make_and_correct: binary_constructor_correct' make_and sem_and.
 Proof.
-  red; intros until m3. intro SEM. unfold make_and. 
+  red; intros until m. intro SEM. unfold make_and. 
   functional inversion SEM. intros. inversion H4. 
   eauto with cshm. 
 Qed.
 
 Lemma make_or_correct: binary_constructor_correct' make_or sem_or.
 Proof.
-  red; intros until m3. intro SEM. unfold make_or. 
+  red; intros until m. intro SEM. unfold make_or. 
   functional inversion SEM. intros. inversion H4. 
   eauto with cshm. 
 Qed.
 
 Lemma make_xor_correct: binary_constructor_correct' make_xor sem_xor.
 Proof.
-  red; intros until m3. intro SEM. unfold make_xor. 
+  red; intros until m. intro SEM. unfold make_xor. 
   functional inversion SEM. intros. inversion H4. 
   eauto with cshm. 
 Qed.
 
 Lemma make_shl_correct: binary_constructor_correct' make_shl sem_shl.
 Proof.
-  red; intros until m3. intro SEM. unfold make_shl. 
+  red; intros until m. intro SEM. unfold make_shl. 
   functional inversion SEM. intros. inversion H5. 
-  econstructor; eauto with cshm. 
+  eapply eval_Ebinop; eauto with cshm. 
   simpl. rewrite H4. auto.
 Qed.
 
 Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr.
 Proof.
-  red; intros until m3. intro SEM. unfold make_shr. 
+  red; intros until m. intro SEM. unfold make_shr. 
   functional inversion SEM; intros; rewrite H0 in H8; inversion H8.
-  econstructor; eauto with cshm.
+  eapply eval_Ebinop; eauto with cshm.
   simpl; rewrite H7; auto.
-  econstructor; eauto with cshm.
+  eapply eval_Ebinop; eauto with cshm.
   simpl; rewrite H7; auto.
 Qed.
 
 Lemma make_cmp_correct:
-  forall cmp a tya b tyb c ta va tb vb v le e m1 m2 m3,
-  sem_cmp cmp va tya vb tyb m3 = Some v ->
+  forall cmp a tya b tyb c va vb v e m,
+  sem_cmp cmp va tya vb tyb m = Some v ->
   make_cmp cmp a tya b tyb = OK c ->  
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m2 b tb m3 vb ->
-  eval_expr tprog le e m1 c (ta ** tb) m3 v.
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m b vb ->
+  eval_expr tprog e m c v.
 Proof.
-  intros until m3. intro SEM. unfold make_cmp.
+  intros until m. intro SEM. unfold make_cmp.
   functional inversion SEM; rewrite H0; intros. 
   inversion H8. eauto with cshm.
   inversion H8. eauto with cshm.
   inversion H8. eauto with cshm.
-  inversion H9. econstructor; eauto with cshm.
+  inversion H9. eapply eval_Ebinop; eauto with cshm.
   simpl. functional inversion H; subst; unfold eval_compare_null;
   rewrite H8; auto.
-  inversion H10. econstructor; eauto with cshm.
+  inversion H10. eapply eval_Ebinop; eauto with cshm.
   simpl. rewrite H3. unfold eq_block; rewrite H9. auto.
 Qed.
 
 Lemma transl_unop_correct:
-  forall op a tya c ta va v le e m1 m2, 
+  forall op a tya c va v e m, 
   transl_unop op a tya = OK c ->
   sem_unary_operation op va tya = Some v ->
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m1 c ta m2 v.
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m c v.
 Proof.
   intros. destruct op; simpl in *.
   eapply make_notbool_correct; eauto. congruence.
@@ -312,12 +310,12 @@ Proof.
 Qed.
 
 Lemma transl_binop_correct:
-forall op a tya b tyb c ta va tb vb v le e m1 m2 m3,
+  forall op a tya b tyb c va vb v e m,
   transl_binop op a tya b tyb = OK c ->  
-  sem_binary_operation op va tya vb tyb m3 = Some v ->
-  eval_expr tprog le e m1 a ta m2 va ->
-  eval_expr tprog le e m2 b tb m3 vb ->
-  eval_expr tprog le e m1 c (ta ** tb) m3 v.
+  sem_binary_operation op va tya vb tyb m = Some v ->
+  eval_expr tprog e m a va ->
+  eval_expr tprog e m b vb ->
+  eval_expr tprog e m c v.
 Proof.
   intros. destruct op; simpl in *.
   eapply make_add_correct; eauto.
@@ -339,10 +337,10 @@ Proof.
 Qed. 
 
 Lemma make_cast_correct:
-  forall le e m1 a t m2 v ty1 ty2 v',
-   eval_expr tprog le e m1 a t m2 v ->
+  forall e m a v ty1 ty2 v',
+   eval_expr tprog e m a v ->
    cast v ty1 ty2 v' ->
-   eval_expr tprog le e m1 (make_cast ty1 ty2 a) t m2 v'.
+   eval_expr tprog e m (make_cast ty1 ty2 a) v'.
 Proof.
   unfold make_cast, make_cast1, make_cast2.
   intros until v'; intros EVAL CAST.
@@ -362,14 +360,14 @@ Proof.
 Qed.
 
 Lemma make_load_correct:
-  forall addr ty code b ofs v le e m1 t m2,
+  forall addr ty code b ofs v e m,
   make_load addr ty = OK code ->
-  eval_expr tprog le e m1 addr t m2 (Vptr b ofs) ->
-  load_value_of_type ty m2 b ofs = Some v ->
-  eval_expr tprog le e m1 code t m2 v.
+  eval_expr tprog e m addr (Vptr b ofs) ->
+  load_value_of_type ty m b ofs = Some v ->
+  eval_expr tprog e m code v.
 Proof.
   unfold make_load, load_value_of_type.
-  intros until m2; intros MKLOAD EVEXP LDVAL.
+  intros until m; intros MKLOAD EVEXP LDVAL.
   destruct (access_mode ty); inversion MKLOAD.
   (* access_mode ty = By_value m *)
   apply eval_Eload with (Vptr b ofs); auto.
@@ -378,18 +376,18 @@ Proof.
 Qed.
 
 Lemma make_store_correct:
-  forall addr ty rhs code e m1 t1 m2 b ofs t2 m3 v m4,
+  forall addr ty rhs code e m b ofs v m',
   make_store addr ty rhs = OK code ->
-  eval_expr tprog nil e m1 addr t1 m2 (Vptr b ofs) ->
-  eval_expr tprog nil e m2 rhs t2 m3 v ->
-  store_value_of_type ty m3 b ofs v = Some m4 ->
-  exec_stmt tprog e m1 code (t1 ** t2) m4 Out_normal.
+  eval_expr tprog e m addr (Vptr b ofs) ->
+  eval_expr tprog e m rhs v ->
+  store_value_of_type ty m b ofs v = Some m' ->
+  exec_stmt tprog e m code E0 m' Out_normal.
 Proof.
   unfold make_store, store_value_of_type.
-  intros until m4; intros MKSTORE EV1 EV2 STVAL.
+  intros until m'; intros MKSTORE EV1 EV2 STVAL.
   destruct (access_mode ty); inversion MKSTORE.
   (* access_mode ty = By_value m *)
-  eapply eval_Sstore; eauto. 
+  eapply exec_Sstore; eauto. 
 Qed.
 
 End CONSTRUCTORS.
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 10f48f61..54f9b772 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -10,6 +10,7 @@ Require Import Values.
 Require Import Events.
 Require Import Mem.
 Require Import Globalenvs.
+Require Import Smallstep.
 Require Import Csyntax.
 Require Import Csem.
 Require Import Ctyping.
@@ -307,13 +308,13 @@ Qed.
 (** Correctness of the code generated by [var_get]. *)
 
 Lemma var_get_correct:
-  forall e m id ty loc ofs v tyenv code te le,
-  Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) E0 m loc ofs ->
+  forall e m id ty loc ofs v tyenv code te,
+  Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) loc ofs ->
   load_value_of_type ty m loc ofs = Some v ->
   wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
   var_get id ty = OK code ->
   match_env tyenv e te ->
-  eval_expr tprog le te m code E0 m v.
+  eval_expr tprog te m code v.
 Proof.
   intros. inversion H1; subst; clear H1. 
   unfold load_value_of_type in H0.
@@ -356,14 +357,14 @@ Qed.
 (** Correctness of the code generated by [var_set]. *)
 
 Lemma var_set_correct:
-  forall e m id ty m1 loc ofs t1 m2 v t2 m3 tyenv code te rhs, 
-  Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) t1 m1 loc ofs ->
-  store_value_of_type ty m2 loc ofs v = Some m3 ->
+  forall e m id ty loc ofs v m' tyenv code te rhs, 
+  Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) loc ofs ->
+  store_value_of_type ty m loc ofs v = Some m' ->
   wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
   var_set id ty rhs = OK code ->
   match_env tyenv e te ->
-  eval_expr tprog nil te m1 rhs t2 m2 v ->
-  exec_stmt tprog te m code (t1 ** t2) m3 Out_normal.
+  eval_expr tprog te m rhs v ->
+  exec_stmt tprog te m code E0 m' Out_normal.
 Proof.
   intros. inversion H1; subst; clear H1. 
   unfold store_value_of_type in H0.
@@ -372,16 +373,16 @@ Proof.
   (* access mode By_value *)
   intros chunk ACC. rewrite ACC in H0. rewrite ACC in H2. 
   inversion H2; clear H2; subst.
-  inversion H; subst; clear H; rewrite E0_left.
+  inversion H; subst; clear H. 
     (* local variable *)
     exploit me_local; eauto. intros [vk [A B]].
     red in A; rewrite ACC in A; subst vk.
-    eapply eval_Sassign. eauto. 
-    eapply eval_var_ref_local. eauto. assumption. 
+    eapply exec_Sassign. eauto.
+    econstructor. eapply eval_var_ref_local. eauto. assumption. 
     (* global variable *)
     exploit me_global; eauto. intros [A B].
-    eapply eval_Sassign. eauto.
-    eapply eval_var_ref_global. auto. 
+    eapply exec_Sassign. eauto.
+    econstructor. eapply eval_var_ref_global. auto. 
     fold tge. rewrite symbols_preserved. eauto.
     eauto. assumption. 
   (* access mode By_reference *)
@@ -390,158 +391,145 @@ Proof.
   intros. rewrite H1 in H0; discriminate.
 Qed.
 
-(** * Proof of semantic simulation *)
+Lemma call_dest_set_correct:
+  forall e m0 lhs loc ofs m1 v m2 tyenv optid te,
+  Csem.eval_lvalue ge e m0 lhs loc ofs ->
+  store_value_of_type (typeof lhs) m1 loc ofs v = Some m2 ->
+  wt_expr tyenv lhs ->
+  transl_lhs_call (Some lhs) = OK optid ->
+  match_env tyenv e te ->
+  exec_opt_assign tprog te m1 optid v m2.
+Proof.
+  intros. generalize H2. simpl. caseEq (is_variable lhs). 2: congruence. 
+  intros. inv H5. 
+  exploit is_variable_correct; eauto. intro.
+  rewrite H5 in H. rewrite H5 in H1. inversion H1. subst i ty.
+  constructor.  
+  generalize H0. unfold store_value_of_type. 
+  caseEq (access_mode (typeof lhs)); intros; try discriminate.
+  (* access mode By_value *)
+  inversion H. 
+  (* local variable *)
+  subst id0 ty l ofs. exploit me_local; eauto. 
+  intros [vk [A B]]. red in A. rewrite H6 in A. subst vk.
+  econstructor. eapply eval_var_ref_local; eauto. assumption.
+  (* global variable *)
+  subst id0 ty l ofs. exploit me_global; eauto. 
+  intros [A B]. 
+  econstructor. eapply eval_var_ref_global; eauto. 
+  rewrite symbols_preserved. eauto. assumption. 
+Qed.
+
+(** * Proof of semantic preservation *)
+
+(** ** Semantic preservation for expressions *)
 
-(** The proof of semantic preservation for this compiler pass relies
-  on simulation diagrams of the following form:
+(** The proof of semantic preservation for the translation of expressions
+  relies on simulation diagrams of the following form:
 <<
-         e, m1, a ------------------- te, m1, ta
+         e, m, a ------------------- te, m, ta
             |                           |
            t|                           |t
             |                           |
             v                           v
-         e, m2, v ------------------- te, m2, v
+         e, m, v ------------------- te, m, v
 >>
-  Left: evaluation of expression [a] in Clight.
+  Left: evaluation of r-value expression [a] in Clight.
   Right: evaluation of its translation [ta] in Csharpminor.
   Top (precondition): matching between environments [e], [te], 
     plus well-typedness of expression [a].
-  Bottom (postcondition): the result values [v] and final memory states [m2]
+  Bottom (postcondition): the result values [v] 
     are identical in both evaluations.
 
   We state these diagrams as the following properties, parameterized
   by the Clight evaluation. *)
 
-Definition eval_expr_prop 
-    (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) (m2: mem) (v: val) : Prop :=
-  forall tyenv ta te tle
+Section EXPR.
+
+Variable e: Csem.env.
+Variable m: mem.
+Variable te: Csharpminor.env.
+Variable tyenv: typenv.
+Hypothesis MENV: match_env tyenv e te.
+
+Definition eval_expr_prop (a: Csyntax.expr) (v: val) : Prop :=
+  forall ta
     (WT: wt_expr tyenv a)
-    (TR: transl_expr a = OK ta)
-    (MENV: match_env tyenv e te),
-  Csharpminor.eval_expr tprog tle te m1 ta t m2 v.
+    (TR: transl_expr a = OK ta),
+  Csharpminor.eval_expr tprog te m ta v.
 
-Definition eval_lvalue_prop
-    (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace)
-    (m2: mem) (b: block) (ofs: int) : Prop :=
-  forall tyenv ta te tle
+Definition eval_lvalue_prop (a: Csyntax.expr) (b: block) (ofs: int) : Prop :=
+  forall ta
     (WT: wt_expr tyenv a)
-    (TR: transl_lvalue a = OK ta)
-    (MENV: match_env tyenv e te),
-  Csharpminor.eval_expr tprog tle te m1 ta t m2 (Vptr b ofs).
+    (TR: transl_lvalue a = OK ta),
+  Csharpminor.eval_expr tprog te m ta (Vptr b ofs).
 
-Definition eval_exprlist_prop
-    (e: Csem.env) (m1: mem) (al: Csyntax.exprlist) (t: trace)
-    (m2: mem) (vl: list val) : Prop :=
-  forall tyenv tal te tle
+Definition eval_exprlist_prop (al: list Csyntax.expr) (vl: list val) : Prop :=
+  forall tal
     (WT: wt_exprlist tyenv al)
-    (TR: transl_exprlist al = OK tal)
-    (MENV: match_env tyenv e te),
-  Csharpminor.eval_exprlist tprog tle te m1 tal t m2 vl.
-
-Definition transl_outcome (nbrk ncnt: nat) (out: Csem.outcome): Csharpminor.outcome :=
-  match out with
-  | Csem.Out_normal => Csharpminor.Out_normal
-  | Csem.Out_break  => Csharpminor.Out_exit nbrk
-  | Csem.Out_continue => Csharpminor.Out_exit ncnt
-  | Csem.Out_return vopt => Csharpminor.Out_return vopt
-  end.
-
-Definition exec_stmt_prop
-    (e: Csem.env) (m1: mem) (s: Csyntax.statement) (t: trace)
-    (m2: mem) (out: Csem.outcome) : Prop :=
-  forall tyenv nbrk ncnt ts te
-    (WT: wt_stmt tyenv s)
-    (TR: transl_statement nbrk ncnt s = OK ts)   
-    (MENV: match_env tyenv e te),
-  Csharpminor.exec_stmt tprog te m1 ts t m2 (transl_outcome nbrk ncnt out).
-
-Definition exec_lblstmts_prop
-    (e: Csem.env) (m1: mem) (s: Csyntax.labeled_statements)
-    (t: trace) (m2: mem) (out: Csem.outcome) : Prop :=
-  forall tyenv nbrk ncnt body ts te m0 t0
-    (WT: wt_lblstmts tyenv s)
-    (TR: transl_lblstmts (lblstmts_length s)
-                         (1 + lblstmts_length s + ncnt)
-                         s body = OK ts)   
-    (MENV: match_env tyenv e te)
-    (BODY: Csharpminor.exec_stmt tprog te m0 body t0 m1 Out_normal),
-  Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 
-       (transl_outcome nbrk ncnt (outcome_switch out)).
-
-Definition eval_funcall_prop
-    (m1: mem) (f: Csyntax.fundef) (params: list val)
-    (t: trace) (m2: mem) (res: val) : Prop :=
-  forall tf
-    (WT: wt_fundef (global_typenv prog) f)
-    (TR: transl_fundef f = OK tf),
-   Csharpminor.eval_funcall tprog m1 tf params t m2 res.
+    (TR: transl_exprlist al = OK tal),
+  Csharpminor.eval_exprlist tprog te m tal vl.
 
-(** The proof of semantic preservation is by induction on the Clight
-  evaluation derivation.  Since this proof is large, we break it
-  into one lemma for each Clight evaluation rule. *)
+(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop).*)
 
 Lemma transl_Econst_int_correct:
-       (forall (e : Csem.env) (m : mem) (i : int) (ty : type),
-        eval_expr_prop e m (Expr (Econst_int i) ty) E0 m (Vint i)).
+  forall (i : int) (ty : type),
+  eval_expr_prop (Expr (Econst_int i) ty) (Vint i).
 Proof.
   intros; red; intros.
   monadInv TR. apply make_intconst_correct.
 Qed.
 
 Lemma transl_Econst_float_correct:
-       (forall (e : Csem.env) (m : mem) (f0 : float) (ty : type),
-        eval_expr_prop e m (Expr (Econst_float f0) ty) E0 m (Vfloat f0)).
+  forall (f0 : float) (ty : type),
+  eval_expr_prop (Expr (Econst_float f0) ty) (Vfloat f0).
 Proof.
   intros; red; intros.
   monadInv TR. apply make_floatconst_correct.
 Qed.
 
 Lemma transl_Elvalue_correct:
-       (forall (e : Csem.env) (m : mem) (a : expr_descr) (ty : type)
-          (t : trace) (m1 : mem) (loc : block) (ofs : int) (v : val),
-        eval_lvalue ge e m (Expr a ty) t m1 loc ofs ->
-        eval_lvalue_prop e m (Expr a ty) t m1 loc ofs ->
-        load_value_of_type ty m1 loc ofs = Some v ->
-        eval_expr_prop e m (Expr a ty) t m1 v).
+  forall (a : expr_descr) (ty : type) (loc : block) (ofs : int)
+         (v : val),
+  eval_lvalue ge e m (Expr a ty) loc ofs ->
+  eval_lvalue_prop (Expr a ty) loc ofs ->
+  load_value_of_type ty m loc ofs = Some v ->
+  eval_expr_prop (Expr a ty) v.
 Proof.
   intros; red; intros.
   exploit transl_expr_lvalue; eauto. 
   intros [[id [EQ VARGET]] | [tb [TRLVAL MKLOAD]]].
   (* Case a is a variable *)
-  subst a. 
-  assert (t = E0 /\ m1 = m). inversion H; auto. 
-  destruct H2; subst t m1.
-  eapply var_get_correct; eauto.
+  subst a. eapply var_get_correct; eauto.
   (* Case a is another lvalue *)
   eapply make_load_correct; eauto. 
 Qed.
 
 Lemma transl_Eaddrof_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
-          (m1 : mem) (loc : block) (ofs : int) (ty : type),
-        eval_lvalue ge e m a t m1 loc ofs ->
-        eval_lvalue_prop e m a t m1 loc ofs ->
-        eval_expr_prop e m (Expr (Csyntax.Eaddrof a) ty) t m1 (Vptr loc ofs)).
+  forall (a : Csyntax.expr) (ty : type) (loc : block) (ofs : int),
+  eval_lvalue ge e m a loc ofs ->
+  eval_lvalue_prop a loc ofs ->
+  eval_expr_prop (Expr (Csyntax.Eaddrof a) ty) (Vptr loc ofs).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR. 
   eauto.
 Qed.
 
 Lemma transl_Esizeof_correct:
-       (forall (e : Csem.env) (m : mem) (ty' ty : type),
-        eval_expr_prop e m (Expr (Esizeof ty') ty) E0 m
-          (Vint (Int.repr (Csyntax.sizeof ty')))).
+  forall ty' ty : type,
+  eval_expr_prop (Expr (Esizeof ty') ty)
+                 (Vint (Int.repr (Csyntax.sizeof ty'))).
 Proof.
   intros; red; intros. monadInv TR. apply make_intconst_correct. 
 Qed.
 
 Lemma transl_Eunop_correct:
-       (forall (e : Csem.env) (m : mem) (op : Csyntax.unary_operation)
-          (a : Csyntax.expr) (ty : type) (t : trace) (m1 : mem) (v1 v : val),
-        Csem.eval_expr ge e m a t m1 v1 ->
-        eval_expr_prop e m a t m1 v1 ->
-        sem_unary_operation op v1 (typeof a) = Some v ->
-        eval_expr_prop e m (Expr (Csyntax.Eunop op a) ty) t m1 v).
+  forall (op : Csyntax.unary_operation) (a : Csyntax.expr) (ty : type)
+         (v1 v : val),
+  Csem.eval_expr ge e m a v1 ->
+  eval_expr_prop a v1 ->
+  sem_unary_operation op v1 (typeof a) = Some v ->
+  eval_expr_prop (Expr (Csyntax.Eunop op a) ty) v.
 Proof.
   intros; red; intros.
   inversion WT; clear WT; subst.
@@ -550,15 +538,14 @@ Proof.
 Qed.
 
 Lemma transl_Ebinop_correct:
-       (forall (e : Csem.env) (m : mem) (op : Csyntax.binary_operation)
-          (a1 a2 : Csyntax.expr) (ty : type) (t1 : trace) (m1 : mem)
-          (v1 : val) (t2 : trace) (m2 : mem) (v2 v : val),
-        Csem.eval_expr ge e m a1 t1 m1 v1 ->
-        eval_expr_prop e m a1 t1 m1 v1 ->
-        Csem.eval_expr ge e m1 a2 t2 m2 v2 ->
-        eval_expr_prop e m1 a2 t2 m2 v2 ->
-        sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m2 = Some v ->
-        eval_expr_prop e m (Expr (Csyntax.Ebinop op a1 a2) ty) (t1 ** t2) m2 v).
+  forall (op : Csyntax.binary_operation) (a1 a2 : Csyntax.expr)
+         (ty : type) (v1 v2 v : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  Csem.eval_expr ge e m a2 v2 ->
+  eval_expr_prop a2 v2 ->
+  sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
+  eval_expr_prop (Expr (Csyntax.Ebinop op a1 a2) ty) v.
 Proof.
   intros; red; intros.
   inversion WT; clear WT; subst.
@@ -567,137 +554,93 @@ Proof.
 Qed.
 
 Lemma transl_Eorbool_1_correct:
-       (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (t : trace)
-          (m1 : mem) (v1 : val) (ty : type),
-        Csem.eval_expr ge e m a1 t m1 v1 ->
-        eval_expr_prop e m a1 t m1 v1 ->
-        is_true v1 (typeof a1) ->
-        eval_expr_prop e m (Expr (Eorbool a1 a2) ty) t m1 Vtrue).
+  forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_true v1 (typeof a1) ->
+  eval_expr_prop (Expr (Eorbool a1 a2) ty) Vtrue.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   unfold make_orbool.
   exploit make_boolean_correct_true; eauto. intros [vb [EVAL ISTRUE]].
-  eapply eval_Econdition_true; eauto.
-  unfold Vtrue; apply make_intconst_correct. traceEq.
+  eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto.
+  simpl. unfold Vtrue; apply make_intconst_correct. 
 Qed.
 
 Lemma transl_Eorbool_2_correct:
-       (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (ty : type)
-          (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem)
-          (v2 v : val),
-        Csem.eval_expr ge e m a1 t1 m1 v1 ->
-        eval_expr_prop e m a1 t1 m1 v1 ->
-        is_false v1 (typeof a1) ->
-        Csem.eval_expr ge e m1 a2 t2 m2 v2 ->
-        eval_expr_prop e m1 a2 t2 m2 v2 ->
-        bool_of_val v2 (typeof a2) v ->
-        eval_expr_prop e m (Expr (Eorbool a1 a2) ty) (t1 ** t2) m2 v).
+  forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 v : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_false v1 (typeof a1) ->
+  Csem.eval_expr ge e m a2 v2 ->
+  eval_expr_prop a2 v2 ->
+  bool_of_val v2 (typeof a2) v ->
+  eval_expr_prop (Expr (Eorbool a1 a2) ty) v.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   unfold make_orbool.
   exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]].
-  eapply eval_Econdition_false; eauto.
-  inversion H4; subst.
+  eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto.
+  simpl. inversion H4; subst.
   exploit make_boolean_correct_true. eapply H3; eauto. eauto. intros [vc [EVAL' ISTRUE']].
-  eapply eval_Econdition_true; eauto. 
-  unfold Vtrue; apply make_intconst_correct. traceEq.
+  eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. 
+  unfold Vtrue; apply make_intconst_correct.
   exploit make_boolean_correct_false. eapply H3; eauto. eauto. intros [vc [EVAL' ISFALSE']].
-  eapply eval_Econdition_false; eauto.
-  unfold Vfalse; apply make_intconst_correct. traceEq.
+  eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. 
+  unfold Vfalse; apply make_intconst_correct. 
 Qed.
 
 Lemma transl_Eandbool_1_correct:
-       (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (t : trace)
-          (m1 : mem) (v1 : val) (ty : type),
-        Csem.eval_expr ge e m a1 t m1 v1 ->
-        eval_expr_prop e m a1 t m1 v1 ->
-        is_false v1 (typeof a1) ->
-        eval_expr_prop e m (Expr (Eandbool a1 a2) ty) t m1 Vfalse).
+  forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_false v1 (typeof a1) ->
+  eval_expr_prop (Expr (Eandbool a1 a2) ty) Vfalse.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   unfold make_andbool.
   exploit make_boolean_correct_false; eauto. intros [vb [EVAL ISFALSE]].
-  eapply eval_Econdition_false; eauto.
-  unfold Vfalse; apply make_intconst_correct. traceEq.
+  eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. 
+  unfold Vfalse; apply make_intconst_correct. 
 Qed.
 
 Lemma transl_Eandbool_2_correct:
-       (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (ty : type)
-          (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem)
-          (v2 v : val),
-        Csem.eval_expr ge e m a1 t1 m1 v1 ->
-        eval_expr_prop e m a1 t1 m1 v1 ->
-        is_true v1 (typeof a1) ->
-        Csem.eval_expr ge e m1 a2 t2 m2 v2 ->
-        eval_expr_prop e m1 a2 t2 m2 v2 ->
-        bool_of_val v2 (typeof a2) v ->
-        eval_expr_prop e m (Expr (Eandbool a1 a2) ty) (t1 ** t2) m2 v).
+  forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 v : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_true v1 (typeof a1) ->
+  Csem.eval_expr ge e m a2 v2 ->
+  eval_expr_prop a2 v2 ->
+  bool_of_val v2 (typeof a2) v ->
+  eval_expr_prop (Expr (Eandbool a1 a2) ty) v.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   unfold make_andbool.
   exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]].
-  eapply eval_Econdition_true; eauto.
-  inversion H4; subst.
+  eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. 
+  simpl. inversion H4; subst.
   exploit make_boolean_correct_true. eapply H3; eauto. eauto. intros [vc [EVAL' ISTRUE']].
-  eapply eval_Econdition_true; eauto. 
-  unfold Vtrue; apply make_intconst_correct. traceEq.
+  eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto.
+  unfold Vtrue; apply make_intconst_correct.
   exploit make_boolean_correct_false. eapply H3; eauto. eauto. intros [vc [EVAL' ISFALSE']].
-  eapply eval_Econdition_false; eauto.
-  unfold Vfalse; apply make_intconst_correct. traceEq.
+  eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto.
+  unfold Vfalse; apply make_intconst_correct.
 Qed.
 
 Lemma transl_Ecast_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (ty : type)
-          (t : trace) (m1 : mem) (v1 v : val),
-        Csem.eval_expr ge e m a t m1 v1 ->
-        eval_expr_prop e m a t m1 v1 ->
-        cast v1 (typeof a) ty v ->
-        eval_expr_prop e m (Expr (Ecast ty a) ty) t m1 v).
+  forall (a : Csyntax.expr) (ty : type) (v1 v : val),
+  Csem.eval_expr ge e m a v1 ->
+  eval_expr_prop a v1 ->
+  cast v1 (typeof a) ty v -> eval_expr_prop (Expr (Ecast ty a) ty) v.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   eapply make_cast_correct; eauto.
 Qed.
 
-Lemma transl_Ecall_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr)
-          (bl : Csyntax.exprlist) (ty : type) (m3 : mem) (vres : val)
-          (t1 : trace) (m1 : mem) (vf : val) (t2 : trace) (m2 : mem)
-          (vargs : list val) (f : Csyntax.fundef) (t3 : trace),
-        Csem.eval_expr ge e m a t1 m1 vf ->
-        eval_expr_prop e m a t1 m1 vf ->
-        Csem.eval_exprlist ge e m1 bl t2 m2 vargs ->
-        eval_exprlist_prop e m1 bl t2 m2 vargs ->
-        Genv.find_funct ge vf = Some f ->
-        type_of_fundef f = typeof a ->
-        Csem.eval_funcall ge m2 f vargs t3 m3 vres ->
-        eval_funcall_prop m2 f vargs t3 m3 vres ->
-        eval_expr_prop e m (Expr (Csyntax.Ecall a bl) ty) (t1 ** t2 ** t3) m3
-          vres).
-Proof.
-  intros; red; intros.
-  inversion WT; clear WT; subst.
-  simpl in TR. 
-  caseEq (classify_fun (typeof a)).
-  2: intros; rewrite H7 in TR; discriminate.
-  intros targs tres EQ. rewrite EQ in TR. 
-  monadInv TR. 
-  rewrite <- H4 in EQ.
-  exploit functions_translated; eauto. intros [tf [FIND TRL]].
-  econstructor.
-  eapply H0; eauto.
-  eapply H2; eauto.
-  eexact FIND. 
-  eapply transl_fundef_sig1; eauto. 
-  eapply H6; eauto. 
-  eapply functions_well_typed; eauto.
-  auto.
-Qed.
-
 Lemma transl_Evar_local_correct:
-       (forall (e : Csem.env) (m : mem) (id : positive) (l : block)
-          (ty : type),
-        e ! id = Some l ->
-        eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero).
+  forall (id : ident) (l : block) (ty : type),
+  e ! id = Some l ->
+  eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   exploit (me_local _ _ _ MENV); eauto. intros [vk [A B]].
@@ -705,11 +648,10 @@ Proof.
 Qed.
 
 Lemma transl_Evar_global_correct:
-       (forall (e : PTree.t block) (m : mem) (id : positive) (l : block)
-          (ty : type),
-        e ! id = None ->
-        Genv.find_symbol ge id = Some l ->
-        eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero).
+  forall (id : ident) (l : block) (ty : type),
+  e ! id = None ->
+  Genv.find_symbol ge id = Some l ->
+  eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR. 
   exploit (me_global _ _ _ MENV); eauto. intros [A B].
@@ -718,83 +660,183 @@ Proof.
 Qed.
 
 Lemma transl_Ederef_correct:
-       (forall (e : Csem.env) (m m1 : mem) (a : Csyntax.expr) (t : trace)
-          (ofs : int) (ty : type) (l : block),
-        Csem.eval_expr ge e m a t m1 (Vptr l ofs) ->
-        eval_expr_prop e m a t m1 (Vptr l ofs) ->
-        eval_lvalue_prop e m (Expr (Ederef a) ty) t m1 l ofs).
+  forall (a : Csyntax.expr) (ty : type) (l : block) (ofs : int),
+  Csem.eval_expr ge e m a (Vptr l ofs) ->
+  eval_expr_prop a (Vptr l ofs) ->
+  eval_lvalue_prop (Expr (Ederef a) ty) l ofs.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR. 
   eauto.
 Qed.
 
 Lemma transl_Eindex_correct:
-       (forall (e : Csem.env) (m : mem) (a1 : Csyntax.expr) (t1 : trace)
-          (m1 : mem) (v1 : val) (a2 : Csyntax.expr) (t2 : trace) (m2 : mem)
-          (v2 : val) (l : block) (ofs : int) (ty : type),
-        Csem.eval_expr ge e m a1 t1 m1 v1 ->
-        eval_expr_prop e m a1 t1 m1 v1 ->
-        Csem.eval_expr ge e m1 a2 t2 m2 v2 ->
-        eval_expr_prop e m1 a2 t2 m2 v2 ->
-        sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
-        eval_lvalue_prop e m (Expr (Eindex a1 a2) ty) (t1 ** t2) m2 l ofs).
+  forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 : val) (l : block)
+         (ofs : int),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  Csem.eval_expr ge e m a2 v2 ->
+  eval_expr_prop a2 v2 ->
+  sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
+  eval_lvalue_prop (Expr (Eindex a1 a2) ty) l ofs.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR. monadInv TR.
   eapply (make_add_correct tprog); eauto. 
 Qed.
 
 Lemma transl_Efield_struct_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
-          (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident)
-          (ty : type) (delta : Z),
-        eval_lvalue ge e m a t m1 l ofs ->
-        eval_lvalue_prop e m a t m1 l ofs ->
-        typeof a = Tstruct id fList ->
-        field_offset i fList = OK delta ->
-        eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l
-          (Int.add ofs (Int.repr delta))).
+  forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block)
+         (ofs : int) (id : ident) (fList : fieldlist) (delta : Z),
+  eval_lvalue ge e m a l ofs ->
+  eval_lvalue_prop a l ofs ->
+  typeof a = Tstruct id fList ->
+  field_offset i fList = OK delta ->
+  eval_lvalue_prop (Expr (Efield a i) ty) l (Int.add ofs (Int.repr delta)).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. 
   simpl in TR. rewrite H1 in TR. monadInv TR.
-  econstructor; eauto.
+  eapply eval_Ebinop; eauto.
   apply make_intconst_correct. 
-  simpl. congruence. traceEq.
+  simpl. congruence.
 Qed.
 
 Lemma transl_Efield_union_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
-          (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident)
-          (ty : type),
-        eval_lvalue ge e m a t m1 l ofs ->
-        eval_lvalue_prop e m a t m1 l ofs ->
-        typeof a = Tunion id fList ->
-        eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l ofs).
+  forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block)
+         (ofs : int) (id : ident) (fList : fieldlist),
+  eval_lvalue ge e m a l ofs ->
+  eval_lvalue_prop a l ofs ->
+  typeof a = Tunion id fList ->
+  eval_lvalue_prop (Expr (Efield a i) ty) l ofs.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. 
   simpl in TR. rewrite H1 in TR. eauto.
 Qed.
 
-Lemma transl_Enil_correct:
-       (forall (e : Csem.env) (m : mem),
-        eval_exprlist_prop e m Csyntax.Enil E0 m nil).
-Proof.
-  intros; red; intros. monadInv TR. constructor.
-Qed.
+Lemma transl_expr_correct:
+  forall a v,
+  Csem.eval_expr ge e m a v ->
+  eval_expr_prop a v.
+Proof
+  (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop
+         transl_Econst_int_correct
+         transl_Econst_float_correct
+         transl_Elvalue_correct
+         transl_Eaddrof_correct
+         transl_Esizeof_correct
+         transl_Eunop_correct
+         transl_Ebinop_correct
+         transl_Eorbool_1_correct
+         transl_Eorbool_2_correct
+         transl_Eandbool_1_correct
+         transl_Eandbool_2_correct
+         transl_Ecast_correct
+         transl_Evar_local_correct
+         transl_Evar_global_correct
+         transl_Ederef_correct
+         transl_Eindex_correct
+         transl_Efield_struct_correct
+         transl_Efield_union_correct).
 
-Lemma transl_Econs_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr)
-          (bl : Csyntax.exprlist) (t1 : trace) (m1 : mem) (v : val)
-          (t2 : trace) (m2 : mem) (vl : list val),
-        Csem.eval_expr ge e m a t1 m1 v ->
-        eval_expr_prop e m a t1 m1 v ->
-        Csem.eval_exprlist ge e m1 bl t2 m2 vl ->
-        eval_exprlist_prop e m1 bl t2 m2 vl ->
-        eval_exprlist_prop e m (Csyntax.Econs a bl) (t1 ** t2) m2 (v :: vl)).
+Lemma transl_lvalue_correct:
+  forall a blk ofs,
+  Csem.eval_lvalue ge e m a blk ofs ->
+  eval_lvalue_prop a blk ofs.
+Proof
+  (eval_lvalue_ind2 ge e m eval_expr_prop eval_lvalue_prop
+         transl_Econst_int_correct
+         transl_Econst_float_correct
+         transl_Elvalue_correct
+         transl_Eaddrof_correct
+         transl_Esizeof_correct
+         transl_Eunop_correct
+         transl_Ebinop_correct
+         transl_Eorbool_1_correct
+         transl_Eorbool_2_correct
+         transl_Eandbool_1_correct
+         transl_Eandbool_2_correct
+         transl_Ecast_correct
+         transl_Evar_local_correct
+         transl_Evar_global_correct
+         transl_Ederef_correct
+         transl_Eindex_correct
+         transl_Efield_struct_correct
+         transl_Efield_union_correct).
+
+Lemma transl_exprlist_correct:
+  forall al vl,
+  Csem.eval_exprlist ge e m al vl ->
+  eval_exprlist_prop al vl.
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. 
-  econstructor; eauto. 
+  induction 1; red; intros; monadInv TR; inv WT.
+  constructor.
+  constructor. eapply (transl_expr_correct _ _ H); eauto. eauto.
 Qed.
 
+End EXPR.
+
+(** ** Semantic preservation for statements *)
+
+(** The simulation diagrams for terminating statements and function
+  calls are of the following form:
+  relies on simulation diagrams of the following form:
+<<
+         e, m1, s ------------------- te, m1, ts
+            |                           |
+           t|                           |t
+            |                           |
+            v                           v
+         e, m2, out ----------------- te, m2, tout
+>>
+  Left: execution of statement [s] in Clight.
+  Right: execution of its translation [ts] in Csharpminor.
+  Top (precondition): matching between environments [e], [te], 
+    plus well-typedness of statement [s].
+  Bottom (postcondition): the outcomes [out] and [tout] are
+    related per the following function [transl_outcome].
+*)
+
+Definition transl_outcome (nbrk ncnt: nat) (out: Csem.outcome): Csharpminor.outcome :=
+  match out with
+  | Csem.Out_normal => Csharpminor.Out_normal
+  | Csem.Out_break  => Csharpminor.Out_exit nbrk
+  | Csem.Out_continue => Csharpminor.Out_exit ncnt
+  | Csem.Out_return vopt => Csharpminor.Out_return vopt
+  end.
+
+Definition exec_stmt_prop
+    (e: Csem.env) (m1: mem) (s: Csyntax.statement) (t: trace)
+    (m2: mem) (out: Csem.outcome) : Prop :=
+  forall tyenv nbrk ncnt ts te
+    (WT: wt_stmt tyenv s)
+    (TR: transl_statement nbrk ncnt s = OK ts)   
+    (MENV: match_env tyenv e te),
+  Csharpminor.exec_stmt tprog te m1 ts t m2 (transl_outcome nbrk ncnt out).
+
+Definition exec_lblstmts_prop
+    (e: Csem.env) (m1: mem) (s: Csyntax.labeled_statements)
+    (t: trace) (m2: mem) (out: Csem.outcome) : Prop :=
+  forall tyenv nbrk ncnt body ts te m0 t0
+    (WT: wt_lblstmts tyenv s)
+    (TR: transl_lblstmts (lblstmts_length s)
+                         (1 + lblstmts_length s + ncnt)
+                         s body = OK ts)   
+    (MENV: match_env tyenv e te)
+    (BODY: Csharpminor.exec_stmt tprog te m0 body t0 m1 Out_normal),
+  Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 
+       (transl_outcome nbrk ncnt (outcome_switch out)).
+
+Definition eval_funcall_prop
+    (m1: mem) (f: Csyntax.fundef) (params: list val)
+    (t: trace) (m2: mem) (res: val) : Prop :=
+  forall tf
+    (WT: wt_fundef (global_typenv prog) f)
+    (TR: transl_fundef f = OK tf),
+   Csharpminor.eval_funcall tprog m1 tf params t m2 res.
+
+(*
+Set Printing Depth 100.
+Check (Csem.eval_funcall_ind3 ge exec_stmt_prop exec_lblstmts_prop eval_funcall_prop).
+*)
+
 Lemma transl_Sskip_correct:
        (forall (e : Csem.env) (m : mem),
         exec_stmt_prop e m Csyntax.Sskip E0 m Csem.Out_normal).
@@ -802,28 +844,13 @@ Proof.
   intros; red; intros. monadInv TR. simpl. constructor.
 Qed.
 
-Lemma transl_Sexpr_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
-          (m1 : mem) (v : val),
-        Csem.eval_expr ge e m a t m1 v ->
-        eval_expr_prop e m a t m1 v ->
-        exec_stmt_prop e m (Csyntax.Sexpr a) t m1 Csem.Out_normal).
-Proof.
-  intros; red; intros; simpl. inversion WT; clear WT; subst. 
-  monadInv TR. econstructor; eauto.
-Qed.
-
 Lemma transl_Sassign_correct:
-       (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (t1 : trace)
-          (m1 : mem) (loc : block) (ofs : int) (t2 : trace) (m2 : mem)
-          (v2 : val) (m3 : mem),
-        eval_lvalue ge e m a1 t1 m1 loc ofs ->
-        eval_lvalue_prop e m a1 t1 m1 loc ofs ->
-        Csem.eval_expr ge e m1 a2 t2 m2 v2 ->
-        eval_expr_prop e m1 a2 t2 m2 v2 ->
-        store_value_of_type (typeof a1) m2 loc ofs v2 = Some m3 ->
-        exec_stmt_prop e m (Csyntax.Sassign a1 a2) (t1 ** t2) m3
-          Csem.Out_normal).
+  forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (loc : block)
+         (ofs : int) (v2 : val) (m' : mem),
+  eval_lvalue ge e m a1 loc ofs ->
+  Csem.eval_expr ge e m a2 v2 ->
+  store_value_of_type (typeof a1) m loc ofs v2 = Some m' ->
+  exec_stmt_prop e m (Csyntax.Sassign a1 a2) E0 m' Csem.Out_normal.
 Proof.
   intros; red; intros.
   inversion WT; subst; clear WT.
@@ -832,12 +859,70 @@ Proof.
   (* a = variable id *)
   intros id ISVAR. rewrite ISVAR in TR. 
   generalize (is_variable_correct _ _ ISVAR). intro EQ. 
-  rewrite EQ in H; rewrite EQ in H0; rewrite EQ in H6.
+  rewrite EQ in H; rewrite EQ in H4.
   monadInv TR.
-  eapply var_set_correct; eauto. 
+  eapply var_set_correct; eauto.
+  eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.  
   (* a is not a variable *)
   intro ISVAR; rewrite ISVAR in TR. monadInv TR.
   eapply make_store_correct; eauto.
+  eapply (transl_lvalue_correct _ _ _ _ MENV _ _ _ H); eauto.
+  eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.  
+Qed.
+
+Lemma transl_Scall_None_correct:
+  forall (e : Csem.env) (m : mem) (a : Csyntax.expr)
+         (al : list Csyntax.expr) (vf : val) (vargs : list val)
+         (f : Csyntax.fundef) (t : trace) (m' : mem) (vres : val),
+  Csem.eval_expr ge e m a vf ->
+  Csem.eval_exprlist ge e m al vargs ->
+  Genv.find_funct ge vf = Some f ->
+  type_of_fundef f = typeof a ->
+  Csem.eval_funcall ge m f vargs t m' vres ->
+  eval_funcall_prop m f vargs t m' vres ->
+  exec_stmt_prop e m (Csyntax.Scall None a al) t m' Csem.Out_normal.
+Proof.
+  intros; red; intros; simpl.
+  inv WT. simpl in TR. 
+  caseEq (classify_fun (typeof a)); intros; rewrite H5 in TR; monadInv TR.
+  exploit functions_translated; eauto. intros [tf [TFIND TFD]].
+  econstructor. 
+  eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto.
+  eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H0); eauto.
+  eauto. 
+  eapply transl_fundef_sig1; eauto. rewrite H2; auto. 
+  eapply H4; eauto. 
+  eapply functions_well_typed; eauto.
+  constructor. 
+Qed.
+
+Lemma transl_Scall_Some_correct:
+  forall (e : Csem.env) (m : mem) (lhs a : Csyntax.expr)
+         (al : list Csyntax.expr) (loc : block) (ofs : int) (vf : val)
+         (vargs : list val) (f : Csyntax.fundef) (t : trace) (m' : mem)
+         (vres : val) (m'' : mem),
+  eval_lvalue ge e m lhs loc ofs ->
+  Csem.eval_expr ge e m a vf ->
+  Csem.eval_exprlist ge e m al vargs ->
+  Genv.find_funct ge vf = Some f ->
+  type_of_fundef f = typeof a ->
+  Csem.eval_funcall ge m f vargs t m' vres ->
+  eval_funcall_prop m f vargs t m' vres ->
+  store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' ->
+  exec_stmt_prop e m (Csyntax.Scall (Some lhs) a al) t m'' Csem.Out_normal.
+Proof.
+  intros; red; intros; simpl.
+  inv WT. inv H10. unfold transl_statement in TR.
+  caseEq (classify_fun (typeof a)); intros; rewrite H7 in TR; monadInv TR.
+  exploit functions_translated; eauto. intros [tf [TFIND TFD]].
+  econstructor. 
+  eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
+  eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto.
+  eauto. 
+  eapply transl_fundef_sig1; eauto. rewrite H3; auto. 
+  eapply H5; eauto. 
+  eapply functions_well_typed; eauto.
+  eapply call_dest_set_correct; eauto. 
 Qed.
 
 Lemma transl_Ssequence_1_correct:
@@ -867,35 +952,39 @@ Proof.
 Qed.
 
 Lemma transl_Sifthenelse_true_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr)
-          (s1 s2 : statement) (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace)
-          (m2 : mem) (out : Csem.outcome),
-        Csem.eval_expr ge e m a t1 m1 v1 ->
-        eval_expr_prop e m a t1 m1 v1 ->
+        (forall (e : Csem.env) (m : mem) (a : Csyntax.expr)
+          (s1 s2 : statement) (v1 : val) (t : trace) (m' : mem)
+          (out : Csem.outcome),
+        Csem.eval_expr ge e m a v1 ->
         is_true v1 (typeof a) ->
-        Csem.exec_stmt ge e m1 s1 t2 m2 out ->
-        exec_stmt_prop e m1 s1 t2 m2 out ->
-        exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) (t1 ** t2) m2 out).
+        Csem.exec_stmt ge e m s1 t m' out ->
+        exec_stmt_prop e m s1 t m' out ->
+        exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) t m' out).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]].
-  eapply exec_Sifthenelse_true; eauto. 
+  exploit make_boolean_correct_true.
+    eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto.
+    eauto.
+  intros [vb [EVAL ISTRUE]].
+  eapply exec_Sifthenelse; eauto. apply Val.bool_of_true_val; eauto. simpl; eauto. 
 Qed.
 
 Lemma transl_Sifthenelse_false_correct:
        (forall (e : Csem.env) (m : mem) (a : Csyntax.expr)
-          (s1 s2 : statement) (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace)
-          (m2 : mem) (out : Csem.outcome),
-        Csem.eval_expr ge e m a t1 m1 v1 ->
-        eval_expr_prop e m a t1 m1 v1 ->
+          (s1 s2 : statement) (v1 : val) (t : trace) (m' : mem)
+          (out : Csem.outcome),
+        Csem.eval_expr ge e m a v1 ->
         is_false v1 (typeof a) ->
-        Csem.exec_stmt ge e m1 s2 t2 m2 out ->
-        exec_stmt_prop e m1 s2 t2 m2 out ->
-        exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) (t1 ** t2) m2 out).
+        Csem.exec_stmt ge e m s2 t m' out ->
+        exec_stmt_prop e m s2 t m' out ->
+        exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) t m' out).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]].
-  eapply exec_Sifthenelse_false; eauto. 
+  exploit make_boolean_correct_false.
+    eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto.
+    eauto.
+  intros [vb [EVAL ISFALSE]].
+  eapply exec_Sifthenelse; eauto. apply Val.bool_of_false_val; eauto. simpl; eauto. 
 Qed.
 
 Lemma transl_Sreturn_none_correct:
@@ -907,15 +996,13 @@ Proof.
 Qed.
 
 Lemma transl_Sreturn_some_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
-          (m1 : mem) (v : val),
-        Csem.eval_expr ge e m a t m1 v ->
-        eval_expr_prop e m a t m1 v ->
-        exec_stmt_prop e m (Csyntax.Sreturn (Some a)) t m1
-          (Csem.Out_return (Some v))).
+       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (v : val),
+        Csem.eval_expr ge e m a v ->
+        exec_stmt_prop e m (Csyntax.Sreturn (Some a)) E0 m (Csem.Out_return (Some v))).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  simpl. eapply exec_Sreturn_some; eauto. 
+  intros; red; intros. inv WT. inv H1. monadInv TR.
+  simpl. eapply exec_Sreturn_some; eauto.
+  eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto.
 Qed.
 
 Lemma transl_Sbreak_correct:
@@ -935,47 +1022,51 @@ Proof.
 Qed.
 
 Lemma exit_if_false_true:
-  forall a ts e m1 t m2 v tyenv te,
+  forall a ts e m v tyenv te,
   exit_if_false a = OK ts ->
-  eval_expr_prop e m1 a t m2 v ->
+  Csem.eval_expr ge e m a v ->
+  is_true v (typeof a) ->
   match_env tyenv e te ->
   wt_expr tyenv a ->
-  is_true v (typeof a) ->
-  exec_stmt tprog te m1 ts t m2 Out_normal.
+  exec_stmt tprog te m ts E0 m Out_normal.
 Proof.
-  intros. monadInv H. 
-  exploit make_boolean_correct_true. eapply H0; eauto. eauto.
+  intros. monadInv H.
+  exploit make_boolean_correct_true.
+    eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto.
+    eauto.
   intros [vb [EVAL ISTRUE]].
-  eapply exec_Sifthenelse_true with (v1 := vb); eauto. 
-  constructor. traceEq.
+  eapply exec_Sifthenelse with (v := vb); eauto.
+  apply Val.bool_of_true_val; eauto.  
+  constructor.
 Qed.
  
 Lemma exit_if_false_false:
-  forall a ts e m1 t m2 v tyenv te,
+  forall a ts e m v tyenv te,
   exit_if_false a = OK ts ->
-  eval_expr_prop e m1 a t m2 v ->
+  Csem.eval_expr ge e m a v ->
+  is_false v (typeof a) ->
   match_env tyenv e te ->
   wt_expr tyenv a ->
-  is_false v (typeof a) ->
-  exec_stmt tprog te m1 ts t m2 (Out_exit 0).
+  exec_stmt tprog te m ts E0 m (Out_exit 0).
 Proof.
-  intros. monadInv H. 
-  exploit make_boolean_correct_false. eapply H0; eauto. eauto.
+  intros. monadInv H.
+  exploit make_boolean_correct_false.
+    eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto.
+    eauto.
   intros [vb [EVAL ISFALSE]].
-  eapply exec_Sifthenelse_false with (v1 := vb); eauto. 
-  constructor. traceEq.
+  eapply exec_Sifthenelse with (v := vb); eauto.
+  apply Val.bool_of_false_val; eauto. 
+  simpl. constructor.
 Qed.
 
 Lemma transl_Swhile_false_correct:
-       (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr)
-          (t : trace) (v : val) (m1 : mem),
-        Csem.eval_expr ge e m a t m1 v ->
-        eval_expr_prop e m a t m1 v ->
+       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (s : statement)
+          (v : val),
+        Csem.eval_expr ge e m a v ->
         is_false v (typeof a) ->
-        exec_stmt_prop e m (Swhile a s) t m1 Csem.Out_normal).
+        exec_stmt_prop e m (Swhile a s) E0 m Csem.Out_normal).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  simpl.
+  intros; red; intros; simpl. inv WT. monadInv TR.
   change Out_normal with (outcome_block (Out_exit 0)).
   apply exec_Sblock. apply exec_Sloop_stop. apply exec_Sseq_stop.
   eapply exit_if_false_false; eauto. congruence. congruence.
@@ -999,48 +1090,45 @@ Proof.
 Qed.
 
 Lemma transl_Swhile_stop_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t1 : trace)
-          (m1 : mem) (v : val) (s : statement) (m2 : mem) (t2 : trace)
-          (out2 out : Csem.outcome),
-        Csem.eval_expr ge e m a t1 m1 v ->
-        eval_expr_prop e m a t1 m1 v ->
+       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (v : val)
+          (s : statement) (t : trace) (m' : mem) (out' out : Csem.outcome),
+        Csem.eval_expr ge e m a v ->
         is_true v (typeof a) ->
-        Csem.exec_stmt ge e m1 s t2 m2 out2 ->
-        exec_stmt_prop e m1 s t2 m2 out2 ->
-        out_break_or_return out2 out ->
-        exec_stmt_prop e m (Swhile a s) (t1 ** t2) m2 out).
+        Csem.exec_stmt ge e m s t m' out' ->
+        exec_stmt_prop e m s t m' out' ->
+        out_break_or_return out' out ->
+        exec_stmt_prop e m (Swhile a s) t m' out).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  rewrite (transl_out_break_or_return _ _ nbrk ncnt H4).
+  intros; red; intros. inv WT. monadInv TR.
+  rewrite (transl_out_break_or_return _ _ nbrk ncnt H3).
   apply exec_Sblock. apply exec_Sloop_stop. 
   eapply exec_Sseq_continue. 
   eapply exit_if_false_true; eauto. 
-  apply exec_Sblock. eauto.
-  auto. inversion H4; simpl; congruence.
+  apply exec_Sblock. eauto. traceEq.
+  inversion H3; simpl; congruence.
 Qed.
 
 Lemma transl_Swhile_loop_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t1 : trace)
-          (m1 : mem) (v : val) (s : statement) (out2 out : Csem.outcome)
-          (t2 : trace) (m2 : mem) (t3 : trace) (m3 : mem),
-        Csem.eval_expr ge e m a t1 m1 v ->
-        eval_expr_prop e m a t1 m1 v ->
+       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (s : statement)
+          (v : val) (t1 : trace) (m1 : mem) (out1 : Csem.outcome)
+          (t2 : trace) (m2 : mem) (out : Csem.outcome),
+        Csem.eval_expr ge e m a v ->
         is_true v (typeof a) ->
-        Csem.exec_stmt ge e m1 s t2 m2 out2 ->
-        exec_stmt_prop e m1 s t2 m2 out2 ->
-        out_normal_or_continue out2 ->
-        Csem.exec_stmt ge e m2 (Swhile a s) t3 m3 out ->
-        exec_stmt_prop e m2 (Swhile a s) t3 m3 out ->
-        exec_stmt_prop e m (Swhile a s) (t1 ** t2 ** t3) m3 out).
+        Csem.exec_stmt ge e m s t1 m1 out1 ->
+        exec_stmt_prop e m s t1 m1 out1 ->
+        out_normal_or_continue out1 ->
+        Csem.exec_stmt ge e m1 (Swhile a s) t2 m2 out ->
+        exec_stmt_prop e m1 (Swhile a s) t2 m2 out ->
+        exec_stmt_prop e m (Swhile a s) (t1 ** t2) m2 out).
 Proof.
   intros; red; intros. 
-  exploit H6; eauto. intro NEXTITER.
-  inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  exploit H5; eauto. intro NEXTITER.
+  inv WT. monadInv TR. 
   inversion NEXTITER; subst.
   apply exec_Sblock. 
   eapply exec_Sloop_loop. eapply exec_Sseq_continue.
   eapply exit_if_false_true; eauto. 
-  rewrite (transl_out_normal_or_continue _ H4).
+  rewrite (transl_out_normal_or_continue _ H3).
   apply exec_Sblock. eauto. 
   reflexivity. eassumption.
   traceEq.
@@ -1048,23 +1136,21 @@ Qed.
 
 Lemma transl_Sdowhile_false_correct:
        (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr)
-          (t1 : trace) (m1 : mem) (out1 : Csem.outcome) (v : val)
-          (t2 : trace) (m2 : mem),
-        Csem.exec_stmt ge e m s t1 m1 out1 ->
-        exec_stmt_prop e m s t1 m1 out1 ->
+          (t : trace) (m1 : mem) (out1 : Csem.outcome) (v : val),
+        Csem.exec_stmt ge e m s t m1 out1 ->
+        exec_stmt_prop e m s t m1 out1 ->
         out_normal_or_continue out1 ->
-        Csem.eval_expr ge e m1 a t2 m2 v ->
-        eval_expr_prop e m1 a t2 m2 v ->
+        Csem.eval_expr ge e m1 a v ->
         is_false v (typeof a) ->
-        exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 Csem.Out_normal).
+        exec_stmt_prop e m (Sdowhile a s) t m1 Csem.Out_normal).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  intros; red; intros. inv WT. monadInv TR.
   simpl.
   change Out_normal with (outcome_block (Out_exit 0)).
   apply exec_Sblock. apply exec_Sloop_stop. eapply exec_Sseq_continue.
   rewrite (transl_out_normal_or_continue out1 H1).
   apply exec_Sblock. eauto. 
-  eapply exit_if_false_false; eauto. auto. congruence. 
+  eapply exit_if_false_false; eauto. traceEq. congruence. 
 Qed.
 
 Lemma transl_Sdowhile_stop_correct:
@@ -1075,7 +1161,7 @@ Lemma transl_Sdowhile_stop_correct:
         out_break_or_return out1 out ->
         exec_stmt_prop e m (Sdowhile a s) t m1 out).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  intros; red; intros. inv WT. monadInv TR.
   simpl.
   assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal).
     inversion H1; simpl; congruence.
@@ -1087,22 +1173,19 @@ Qed.
 
 Lemma transl_Sdowhile_loop_correct:
        (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr)
-          (m1 m2 m3 : mem) (t1 t2 t3 : trace) (out out1 : Csem.outcome)
-          (v : val),
+          (m1 m2 : mem) (t1 t2 : trace) (out out1 : Csem.outcome) (v : val),
         Csem.exec_stmt ge e m s t1 m1 out1 ->
         exec_stmt_prop e m s t1 m1 out1 ->
         out_normal_or_continue out1 ->
-        Csem.eval_expr ge e m1 a t2 m2 v ->
-        eval_expr_prop e m1 a t2 m2 v ->
+        Csem.eval_expr ge e m1 a v ->
         is_true v (typeof a) ->
-        Csem.exec_stmt ge e m2 (Sdowhile a s) t3 m3 out ->
-        exec_stmt_prop e m2 (Sdowhile a s) t3 m3 out ->
-        exec_stmt_prop e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out).
+        Csem.exec_stmt ge e m1 (Sdowhile a s) t2 m2 out ->
+        exec_stmt_prop e m1 (Sdowhile a s) t2 m2 out ->
+        exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 out).
 Proof.
   intros; red; intros. 
-  exploit H6; eauto. intro NEXTITER.
-  inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  inversion NEXTITER; subst.
+  exploit H5; eauto. intro NEXTITER.
+  inv WT. monadInv TR. inversion NEXTITER; subst.
   apply exec_Sblock. 
   eapply exec_Sloop_loop. eapply exec_Sseq_continue.
   rewrite (transl_out_normal_or_continue _ H1).
@@ -1115,6 +1198,7 @@ Lemma transl_Sfor_start_correct:
        (forall (e : Csem.env) (m : mem) (s a1 : statement)
           (a2 : Csyntax.expr) (a3 : statement) (out : Csem.outcome)
           (m1 m2 : mem) (t1 t2 : trace),
+        a1 <> Csyntax.Sskip ->
         Csem.exec_stmt ge e m a1 t1 m1 Csem.Out_normal ->
         exec_stmt_prop e m a1 t1 m1 Csem.Out_normal ->
         Csem.exec_stmt ge e m1 (Sfor Csyntax.Sskip a2 a3 s) t2 m2 out ->
@@ -1122,101 +1206,88 @@ Lemma transl_Sfor_start_correct:
         exec_stmt_prop e m (Sfor a1 a2 a3 s) (t1 ** t2) m2 out).
 Proof.
   intros; red; intros.
-  exploit transl_stmt_Sfor_start; eauto. 
-  intros [ts1 [ts2 [A [B C]]]].
-  clear TR; subst ts. 
-  inversion WT; subst.
+  destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H) as [ts1 [ts2 [EQ [TR1 TR2]]]].
+  subst ts.
+  inv WT.
   assert (WT': wt_stmt tyenv (Sfor Csyntax.Sskip a2 a3 s)).
     constructor; auto. constructor.
-  exploit H0; eauto. simpl. intro EXEC1.
-  exploit H2; eauto. intro EXEC2. 
-  assert (EXEC3: exec_stmt tprog te m1 ts2 t2 m2 (transl_outcome nbrk ncnt out)).
-    inversion EXEC2; subst.
-    inversion H5; subst. rewrite E0_left; auto.
-    inversion H11; subst. congruence.
-  eapply exec_Sseq_continue; eauto. 
+  exploit H1; eauto. simpl. intro EXEC1.
+  exploit H3; eauto. intro EXEC2.
+  eapply exec_Sseq_continue; eauto.  
 Qed.
 
 Lemma transl_Sfor_false_correct:
        (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr)
-          (a3 : statement) (t : trace) (v : val) (m1 : mem),
-        Csem.eval_expr ge e m a2 t m1 v ->
-        eval_expr_prop e m a2 t m1 v ->
+          (a3 : statement) (v : val),
+        Csem.eval_expr ge e m a2 v ->
         is_false v (typeof a2) ->
-        exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) t m1 Csem.Out_normal).
+        exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) E0 m Csem.Out_normal).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  intros; red; intros. inv WT.
+  rewrite transl_stmt_Sfor_not_start in TR; monadInv TR.
   simpl.
-  eapply exec_Sseq_continue. apply exec_Sskip.
   change Out_normal with (outcome_block (Out_exit 0)).
   apply exec_Sblock. apply exec_Sloop_stop. 
   apply exec_Sseq_stop. eapply exit_if_false_false; eauto. 
-  congruence. congruence. traceEq. 
+  congruence. congruence.  
 Qed.
 
 Lemma transl_Sfor_stop_correct:
        (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr)
-          (a3 : statement) (v : val) (m1 m2 : mem) (t1 t2 : trace)
-          (out2 out : Csem.outcome),
-        Csem.eval_expr ge e m a2 t1 m1 v ->
-        eval_expr_prop e m a2 t1 m1 v ->
+          (a3 : statement) (v : val) (m1 : mem) (t : trace)
+          (out1 out : Csem.outcome),
+        Csem.eval_expr ge e m a2 v ->
         is_true v (typeof a2) ->
-        Csem.exec_stmt ge e m1 s t2 m2 out2 ->
-        exec_stmt_prop e m1 s t2 m2 out2 ->
-        out_break_or_return out2 out ->
-        exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) (t1 ** t2) m2 out).
+        Csem.exec_stmt ge e m s t m1 out1 ->
+        exec_stmt_prop e m s t m1 out1 ->
+        out_break_or_return out1 out ->
+        exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) t m1 out).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  simpl.
-  assert (outcome_block (transl_outcome 1 0 out2) <> Out_normal).
-    inversion H4; simpl; congruence.
-  rewrite (transl_out_break_or_return _ _ nbrk ncnt H4). 
-  eapply exec_Sseq_continue. apply exec_Sskip.
+  intros; red; intros. inv WT.
+  rewrite transl_stmt_Sfor_not_start in TR; monadInv TR.
+  assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal).
+    inversion H3; simpl; congruence.
+  rewrite (transl_out_break_or_return _ _ nbrk ncnt H3). 
   apply exec_Sblock. apply exec_Sloop_stop. 
   eapply exec_Sseq_continue. eapply exit_if_false_true; eauto.
   apply exec_Sseq_stop. apply exec_Sblock. eauto. 
-  auto. reflexivity. auto. traceEq. 
+  auto. reflexivity. auto. 
 Qed.
 
 Lemma transl_Sfor_loop_correct:
        (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr)
-          (a3 : statement) (v : val) (m1 m2 m3 m4 : mem)
-          (t1 t2 t3 t4 : trace) (out2 out : Csem.outcome),
-        Csem.eval_expr ge e m a2 t1 m1 v ->
-        eval_expr_prop e m a2 t1 m1 v ->
+          (a3 : statement) (v : val) (m1 m2 m3 : mem) (t1 t2 t3 : trace)
+          (out1 out : Csem.outcome),
+        Csem.eval_expr ge e m a2 v ->
         is_true v (typeof a2) ->
-        Csem.exec_stmt ge e m1 s t2 m2 out2 ->
-        exec_stmt_prop e m1 s t2 m2 out2 ->
-        out_normal_or_continue out2 ->
-        Csem.exec_stmt ge e m2 a3 t3 m3 Csem.Out_normal ->
-        exec_stmt_prop e m2 a3 t3 m3 Csem.Out_normal ->
-        Csem.exec_stmt ge e m3 (Sfor Csyntax.Sskip a2 a3 s) t4 m4 out ->
-        exec_stmt_prop e m3 (Sfor Csyntax.Sskip a2 a3 s) t4 m4 out ->
-        exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s)
-          (t1 ** t2 ** t3 ** t4) m4 out).
+        Csem.exec_stmt ge e m s t1 m1 out1 ->
+        exec_stmt_prop e m s t1 m1 out1 ->
+        out_normal_or_continue out1 ->
+        Csem.exec_stmt ge e m1 a3 t2 m2 Csem.Out_normal ->
+        exec_stmt_prop e m1 a3 t2 m2 Csem.Out_normal ->
+        Csem.exec_stmt ge e m2 (Sfor Csyntax.Sskip a2 a3 s) t3 m3 out ->
+        exec_stmt_prop e m2 (Sfor Csyntax.Sskip a2 a3 s) t3 m3 out ->
+        exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) (t1 ** t2 ** t3) m3 out).
 Proof.
   intros; red; intros. 
-  exploit H8; eauto. intro NEXTITER.
-  inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  exploit H7; eauto. intro NEXTITER.
+  inv WT.
+  rewrite transl_stmt_Sfor_not_start in TR; monadInv TR.
   inversion NEXTITER; subst.
-  inversion H11; subst.
-  inversion H18; subst.   
-  eapply exec_Sseq_continue. apply exec_Sskip.
   apply exec_Sblock. 
   eapply exec_Sloop_loop. eapply exec_Sseq_continue.
   eapply exit_if_false_true; eauto.
   eapply exec_Sseq_continue.
-  rewrite (transl_out_normal_or_continue _ H4).
+  rewrite (transl_out_normal_or_continue _ H3).
   apply exec_Sblock. eauto. 
-  red in H6; simpl in H6; eauto.
+  red in H5; simpl in H5; eauto.
   reflexivity. reflexivity. eassumption. 
-  reflexivity. traceEq. 
-  inversion H17. congruence.
+  traceEq. 
 Qed.
 
 Lemma transl_lblstmts_switch:
-  forall e m0 t1 m1 n nbrk ncnt tyenv te t2 m2 out sl body ts,
-  exec_stmt tprog te m0 body t1 m1 
+  forall e m0 m1 n nbrk ncnt tyenv te t0 t m2 out sl body ts,
+  exec_stmt tprog te m0 body t0 m1 
     (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0))) ->
   transl_lblstmts 
     (lblstmts_length sl)
@@ -1224,8 +1295,8 @@ Lemma transl_lblstmts_switch:
     sl (Sblock body) = OK ts ->
   wt_lblstmts tyenv sl ->
   match_env tyenv e te ->
-  exec_lblstmts_prop e m1 (select_switch n sl) t2 m2 out ->
-  Csharpminor.exec_stmt tprog te m0 ts (t1 ** t2) m2 
+  exec_lblstmts_prop e m1 (select_switch n sl) t m2 out ->
+  Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 
     (transl_outcome nbrk ncnt (outcome_switch out)).
 Proof.
   induction sl; intros.
@@ -1251,24 +1322,20 @@ Proof.
 Qed.
 
 Lemma transl_Sswitch_correct:
-       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t1 : trace)
-          (m1 : mem) (n : int) (sl : labeled_statements) (t2 : trace)
-          (m2 : mem) (out : Csem.outcome),
-        Csem.eval_expr ge e m a t1 m1 (Vint n) ->
-        eval_expr_prop e m a t1 m1 (Vint n) ->
-        exec_lblstmts ge e m1 (select_switch n sl) t2 m2 out ->
-        exec_lblstmts_prop e m1 (select_switch n sl) t2 m2 out ->
-        exec_stmt_prop e m (Csyntax.Sswitch a sl) (t1 ** t2) m2
-          (outcome_switch out)).
+       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
+          (n : int) (sl : labeled_statements) (m1 : mem) (out : Csem.outcome),
+        Csem.eval_expr ge e m a (Vint n) ->
+        exec_lblstmts ge e m (select_switch n sl) t m1 out ->
+        exec_lblstmts_prop e m (select_switch n sl) t m1 out ->
+        exec_stmt_prop e m (Csyntax.Sswitch a sl) t m1 (outcome_switch out)).
 Proof.
   intros; red; intros.
-  inversion WT; clear WT; subst.
-  simpl in TR. monadInv TR. 
+  inv WT. monadInv TR.
   rewrite length_switch_table in EQ0. 
   replace (ncnt + lblstmts_length sl + 1)%nat
      with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega.
-  eapply transl_lblstmts_switch; eauto. 
-  constructor. eapply H0; eauto. 
+  change t with (E0 ** t). eapply transl_lblstmts_switch; eauto. 
+  constructor. eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. 
 Qed.
 
 Lemma transl_LSdefault_correct:
@@ -1278,9 +1345,7 @@ Lemma transl_LSdefault_correct:
         exec_stmt_prop e m s t m1 out ->
         exec_lblstmts_prop e m (LSdefault s) t m1 out).
 Proof.
-  intros; red; intros.
-  inversion WT; subst.
-  simpl in TR. monadInv TR.
+  intros; red; intros. inv WT. monadInv TR.
   replace (transl_outcome nbrk ncnt (outcome_switch out))
      with (outcome_block (transl_outcome 0 (S ncnt) out)).
   constructor. 
@@ -1299,11 +1364,9 @@ Lemma transl_LScase_fallthrough_correct:
         exec_lblstmts_prop e m1 ls t2 m2 out ->
         exec_lblstmts_prop e m (LScase n s ls) (t1 ** t2) m2 out).
 Proof.
-  intros; red; intros.
-  inversion WT; subst.
-  monadInv TR.
+  intros; red; intros. inv WT. monadInv TR. 
   assert (exec_stmt tprog te m0 (Sblock (Sseq body x)) 
-                  (t0 ** t1) m1 Out_normal).
+                          (t0 ** t1) m1 Out_normal).
   change Out_normal with
     (outcome_block (transl_outcome (S (lblstmts_length ls))
                                    (S (S (lblstmts_length ls + ncnt)))
@@ -1316,7 +1379,7 @@ Proof.
 Qed.
 
 Lemma transl_LScase_stop_correct:
-       (forall (e : Csem.env) (m : mem) (n : int) (s : statement)
+      (forall (e : Csem.env) (m : mem) (n : int) (s : statement)
           (ls : labeled_statements) (t : trace) (m1 : mem)
           (out : Csem.outcome),
         Csem.exec_stmt ge e m s t m1 out ->
@@ -1324,9 +1387,7 @@ Lemma transl_LScase_stop_correct:
         out <> Csem.Out_normal ->
         exec_lblstmts_prop e m (LScase n s ls) t m1 out).
 Proof.
-  intros; red; intros.
-  inversion WT; subst.
-  monadInv TR.
+  intros; red; intros. inv WT. monadInv TR.
   exploit H0; eauto. intro EXEC.
   destruct out; simpl; simpl in EXEC.
   (* out = Out_break *)
@@ -1378,8 +1439,7 @@ Lemma transl_funcall_internal_correct:
 Proof.
   intros; red; intros.
   (* Exploitation of typing hypothesis *)
-  inversion WT; clear WT; subst. 
-  inversion H6; clear H6; subst.
+  inv WT. inv H6.
   (* Exploitation of translation hypothesis *)
   monadInv TR. 
   monadInv EQ.
@@ -1419,38 +1479,55 @@ Theorem transl_funcall_correct:
   Csem.eval_funcall ge m f l t m0 v ->
   eval_funcall_prop m f l t m0 v.
 Proof
-  (Csem.eval_funcall_ind6 ge
-         eval_expr_prop
-         eval_lvalue_prop
-         eval_exprlist_prop
+  (Csem.eval_funcall_ind3 ge
+         exec_stmt_prop
+         exec_lblstmts_prop
+         eval_funcall_prop
+
+         transl_Sskip_correct
+         transl_Sassign_correct
+         transl_Scall_None_correct
+         transl_Scall_Some_correct
+         transl_Ssequence_1_correct
+         transl_Ssequence_2_correct
+         transl_Sifthenelse_true_correct
+         transl_Sifthenelse_false_correct
+         transl_Sreturn_none_correct
+         transl_Sreturn_some_correct
+         transl_Sbreak_correct
+         transl_Scontinue_correct
+         transl_Swhile_false_correct
+         transl_Swhile_stop_correct
+         transl_Swhile_loop_correct
+         transl_Sdowhile_false_correct
+         transl_Sdowhile_stop_correct
+         transl_Sdowhile_loop_correct
+         transl_Sfor_start_correct
+         transl_Sfor_false_correct
+         transl_Sfor_stop_correct
+         transl_Sfor_loop_correct
+         transl_Sswitch_correct
+         transl_LSdefault_correct
+         transl_LScase_fallthrough_correct
+         transl_LScase_stop_correct
+         transl_funcall_internal_correct
+         transl_funcall_external_correct).
+
+Theorem transl_stmt_correct:
+  forall (e: Csem.env) (m1: mem) (s: Csyntax.statement) (t: trace)
+         (m2: mem) (out: Csem.outcome),
+  Csem.exec_stmt ge e m1 s t m2 out ->
+  exec_stmt_prop e m1 s t m2 out.
+Proof
+  (Csem.exec_stmt_ind3 ge
          exec_stmt_prop
          exec_lblstmts_prop
          eval_funcall_prop
 
-         transl_Econst_int_correct
-         transl_Econst_float_correct
-         transl_Elvalue_correct
-         transl_Eaddrof_correct
-         transl_Esizeof_correct
-         transl_Eunop_correct
-         transl_Ebinop_correct
-         transl_Eorbool_1_correct
-         transl_Eorbool_2_correct
-         transl_Eandbool_1_correct
-         transl_Eandbool_2_correct
-         transl_Ecast_correct
-         transl_Ecall_correct
-         transl_Evar_local_correct
-         transl_Evar_global_correct
-         transl_Ederef_correct
-         transl_Eindex_correct
-         transl_Efield_struct_correct
-         transl_Efield_union_correct
-         transl_Enil_correct
-         transl_Econs_correct
          transl_Sskip_correct
-         transl_Sexpr_correct
          transl_Sassign_correct
+         transl_Scall_None_correct
+         transl_Scall_Some_correct
          transl_Ssequence_1_correct
          transl_Ssequence_2_correct
          transl_Sifthenelse_true_correct
@@ -1476,41 +1553,287 @@ Proof
          transl_funcall_internal_correct
          transl_funcall_external_correct).
 
+(** ** Semantic preservation for divergence *)
+
+Lemma transl_funcall_divergence_correct:
+  forall m1 f params t tf,
+  Csem.evalinf_funcall ge m1 f params t ->
+  wt_fundef (global_typenv prog) f ->
+  transl_fundef f = OK tf ->
+  Csharpminor.evalinf_funcall tprog m1 tf params t.
+Proof.
+  cofix FUNCALL.
+  assert (STMT: 
+    forall e m1 s t,
+    Csem.execinf_stmt ge e m1 s t ->
+    forall tyenv nbrk ncnt ts te
+      (WT: wt_stmt tyenv s)
+      (TR: transl_statement nbrk ncnt s = OK ts)   
+      (MENV: match_env tyenv e te),
+    Csharpminor.execinf_stmt tprog te m1 ts t).
+  cofix STMT.
+  assert(LBLSTMT:
+  forall s ncnt body ts tyenv e te m0 t0 m1 t1 n,
+  transl_lblstmts (lblstmts_length s)
+                  (S (lblstmts_length s + ncnt))
+                  s body = OK ts ->
+  wt_lblstmts tyenv s ->
+  match_env tyenv e te ->
+      (exec_stmt tprog te m0 body t0 m1
+        (outcome_block (Out_exit
+           (switch_target n (lblstmts_length s) (switch_table s 0))))
+       /\ execinf_lblstmts ge e m1 (select_switch n s) t1)
+   \/ (exec_stmt tprog te m0 body t0 m1 Out_normal
+       /\ execinf_lblstmts ge e m1 s t1) ->
+  execinf_stmt_N tprog (lblstmts_length s) te m0 ts (t0 *** t1)).
+
+  cofix LBLSTMT; intros.
+  destruct s; simpl in *; monadInv H; inv H0.
+  (* 1. LSdefault *)
+  assert (exec_stmt tprog te m0 body t0 m1 Out_normal) by tauto.
+  assert (execinf_lblstmts ge e m1 (LSdefault s) t1) by tauto.
+  clear H2. inv H0.  
+  change (Sblock (Sseq body x))
+    with ((fun z => Sblock z) (Sseq body x)).
+  apply execinf_context. 
+  eapply execinf_Sseq_2. eauto. eapply STMT; eauto. auto.
+  constructor.
+  (* 2. LScase *)
+  elim H2; clear H2.
+  (* 2.1 searching for the case *)
+  rewrite (Int.eq_sym i n). 
+  destruct (Int.eq n i).
+  (* 2.1.1 found it! *)
+  intros [A B]. inv B.
+  (* 2.1.1.1 we diverge because of this case *)
+  destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
+  rewrite EQ1. apply execinf_context; auto. 
+  apply execinf_Sblock. eapply execinf_Sseq_2. eauto. 
+  eapply STMT; eauto. auto.
+  (* 2.1.1.2 we diverge later, after falling through *)
+  simpl. apply execinf_sleep.
+  replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). 
+  eapply LBLSTMT with (n := n); eauto. right. split.
+  change Out_normal with (outcome_block Out_normal). 
+  apply exec_Sblock.
+  eapply exec_Sseq_continue. eauto. 
+  change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
+  eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
+  auto. auto. traceEq.
+  (* 2.1.2 still searching *)
+  rewrite switch_target_table_shift. intros [A B].
+  apply execinf_sleep.
+  eapply LBLSTMT with (n := n); eauto. left. split.
+  fold (outcome_block (Out_exit (switch_target n (lblstmts_length s0) (switch_table s0 0)))).
+  apply exec_Sblock. apply exec_Sseq_stop. eauto. congruence.
+  auto.
+  (* 2.2 found the case already, falling through next cases *)
+  intros [A B]. inv B.
+  (* 2.2.1 we diverge because of this case *)
+  destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
+  rewrite EQ1. apply execinf_context; auto. 
+  apply execinf_Sblock. eapply execinf_Sseq_2. eauto. 
+  eapply STMT; eauto. auto.
+  (* 2.2.2 we diverge later *)
+  simpl. apply execinf_sleep.
+  replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). 
+  eapply LBLSTMT with (n := n); eauto. right. split.
+  change Out_normal with (outcome_block Out_normal). 
+  apply exec_Sblock.
+  eapply exec_Sseq_continue. eauto. 
+  change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
+  eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
+  auto. auto. traceEq.
+
+
+  intros. inv H; inv WT; try (generalize TR; intro TR'; monadInv TR').
+  (* Scall *)
+  simpl in TR.
+  caseEq (classify_fun (typeof a)); intros; rewrite H in TR; monadInv TR.
+  destruct (functions_translated _ _ H2) as [tf [TFIND TFD]].
+  eapply execinf_Scall. 
+  eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
+  eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto.
+  eauto. 
+  eapply transl_fundef_sig1; eauto. rewrite H3; auto. 
+  eapply FUNCALL; eauto.
+  eapply functions_well_typed; eauto.
+  (* Sseq 1 *)
+  apply execinf_Sseq_1. eapply STMT; eauto. 
+  (* Sseq 2 *)
+  eapply execinf_Sseq_2. 
+  change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
+  eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto.
+  eapply STMT; eauto. auto.
+  (* Sifthenelse, true *)
+  assert (eval_expr tprog te m1 x v1).
+    eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
+  destruct (make_boolean_correct_true _ _ _ _ _ _ H H1) as [vb [A B]].
+  eapply execinf_Sifthenelse. eauto. apply Val.bool_of_true_val; eauto.
+  auto. eapply STMT; eauto.
+  (* Sifthenelse, false *)
+  assert (eval_expr tprog te m1 x v1).
+    eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
+  destruct (make_boolean_correct_false _ _ _ _ _ _ H H1) as [vb [A B]].
+  eapply execinf_Sifthenelse. eauto. apply Val.bool_of_false_val; eauto.
+  auto. eapply STMT; eauto.
+  (* Swhile, body *)
+  apply execinf_Sblock. apply execinf_Sloop_body.  
+  eapply execinf_Sseq_2. eapply exit_if_false_true; eauto. 
+  apply execinf_Sblock. eapply STMT; eauto. traceEq.
+  (* Swhile, loop *)
+  apply execinf_Sblock. eapply execinf_Sloop_block.
+  eapply exec_Sseq_continue. eapply exit_if_false_true; eauto.
+  rewrite (transl_out_normal_or_continue out1 H3). 
+  apply exec_Sblock. 
+  eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. reflexivity.
+  eapply STMT with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
+  constructor; eauto.
+  traceEq.
+  (* Sdowhile, body *)
+  apply execinf_Sblock. apply execinf_Sloop_body.  
+  apply execinf_Sseq_1. apply execinf_Sblock.
+  eapply STMT; eauto.
+  (* Sdowhile, loop *)
+  apply execinf_Sblock. eapply execinf_Sloop_block.
+  eapply exec_Sseq_continue.
+  rewrite (transl_out_normal_or_continue out1 H1). 
+  apply exec_Sblock. 
+  eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto. 
+  eapply exit_if_false_true; eauto. reflexivity.
+  eapply STMT with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
+  constructor; auto.
+  traceEq.
+  (* Sfor start 1 *)
+  simpl in TR. destruct (is_Sskip a1). 
+  subst a1. inv H0.
+  monadInv TR. 
+  apply execinf_Sseq_1. eapply STMT; eauto.
+  (* Sfor start 2 *)
+  destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H0) as [ts1 [ts2 [EQ [TR1 TR2]]]].
+  subst ts. 
+  eapply execinf_Sseq_2. 
+  change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
+  eapply (transl_stmt_correct _ _ _ _ _ _ H1); eauto.
+  eapply STMT; eauto. 
+    constructor; auto. constructor.
+  auto.
+  (* Sfor_body *)
+  rewrite transl_stmt_Sfor_not_start in TR; monadInv TR.
+  apply execinf_Sblock. apply execinf_Sloop_body.
+  eapply execinf_Sseq_2. 
+  eapply exit_if_false_true; eauto.
+  apply execinf_Sseq_1. apply execinf_Sblock. 
+  eapply STMT; eauto.
+  traceEq.
+  (* Sfor next *)
+  rewrite transl_stmt_Sfor_not_start in TR; monadInv TR.
+  apply execinf_Sblock. apply execinf_Sloop_body.
+  eapply execinf_Sseq_2. 
+  eapply exit_if_false_true; eauto.
+  eapply execinf_Sseq_2.
+  rewrite (transl_out_normal_or_continue out1 H3). 
+  apply exec_Sblock. 
+  eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto.
+  eapply STMT; eauto.
+  reflexivity. traceEq. 
+  (* Sfor loop *)
+  generalize TR. rewrite transl_stmt_Sfor_not_start; intro TR'; monadInv TR'.
+  apply execinf_Sblock. eapply execinf_Sloop_block.
+  eapply exec_Sseq_continue.
+  eapply exit_if_false_true; eauto.
+  eapply exec_Sseq_continue.
+  rewrite (transl_out_normal_or_continue out1 H3). 
+  apply exec_Sblock. 
+  eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto.
+  change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
+  eapply (transl_stmt_correct _ _ _ _ _ _ H4); eauto.
+  reflexivity. reflexivity. 
+  eapply STMT; eauto. 
+    constructor; auto.
+  traceEq.
+  (* Sswitch *)
+  apply execinf_stutter with (lblstmts_length sl).
+  rewrite length_switch_table in EQ0.
+  replace (ncnt + lblstmts_length sl + 1)%nat
+     with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega.
+  change t with (E0 *** t).
+  eapply LBLSTMT; eauto.
+  left. split. apply exec_Sblock. constructor. 
+  eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
+  auto. 
+
+  (* Functions *)
+  intros. inv H. 
+  (* Exploitation of typing hypothesis *)
+  inv H0. inv H6. 
+  (* Exploitation of translation hypothesis *)
+  monadInv H1. monadInv EQ.
+  (* Allocation of variables *)
+  assert (match_env (global_typenv prog) Csem.empty_env Csharpminor.empty_env).
+    apply match_globalenv_match_env_empty. apply match_global_typenv. 
+  generalize (transl_fn_variables _ _ (signature_of_function f0) _ _ x2 EQ0 EQ).
+  intro. 
+  destruct (match_env_alloc_variables _ _ _ _ _ _ H2 _ _ _ H1 H5)
+  as [te [ALLOCVARS MATCHENV]].
+  (* Execution *)
+  econstructor; simpl.
+  eapply transl_names_norepet; eauto. 
+  eexact ALLOCVARS.
+  eapply bind_parameters_match; eauto.
+  eapply STMT; eauto. 
+Qed.
+
 End CORRECTNESS.
 
 (** Semantic preservation for whole programs. *)
 
 Theorem transl_program_correct:
-  forall prog tprog t r,
+  forall prog tprog beh,
   transl_program prog = OK tprog ->
   Ctyping.wt_program prog ->
-  Csem.exec_program prog t r ->
-  Csharpminor.exec_program tprog t r.
+  Csem.exec_program prog beh ->
+  Csharpminor.exec_program tprog beh.
 Proof.
-  intros until r. intros TRANSL WT [b [f [m1 [FINDS [FINDF EVAL]]]]].
-  inversion WT; subst.
-
+  intros. inversion H0; subst. inv H1.
+  (* Termination *)
   assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)).
     apply wt_program_main.
     eapply Genv.find_funct_ptr_symbol_inversion; eauto. 
-  elim H; clear H; intros targs TYP.
+  elim H1; clear H1; intros targs TYP.
   assert (targs = Tnil).
-    inversion EVAL; subst; simpl in TYP.
-    inversion H0; subst. injection TYP. rewrite <- H6. simpl; auto.
-    inversion TYP; subst targs0 tres. inversion H. simpl in H0. 
-    inversion H0. destruct targs; simpl in H8; congruence.
+    inv H4; simpl in TYP.
+    inv H5. injection TYP. rewrite <- H10. simpl. auto.
+    inv TYP. inv H1. 
+    destruct targs; simpl in H4. auto. inv H4. 
   subst targs.
   exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]].
-  exists b; exists tf; exists m1.
-  split. 
-    rewrite (symbols_preserved _ _ TRANSL).
-    rewrite (transform_partial_program2_main transl_fundef transl_globvar prog TRANSL). auto.
-  split. auto.
-  split. 
-    generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto.
-  rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL).
-  generalize (transl_funcall_correct _ _ WT TRANSL _ _ _ _ _ _ EVAL).
-  intro. eapply H. 
+  apply program_terminates with b tf m1.
+  rewrite (symbols_preserved _ _ H).
+  rewrite (transform_partial_program2_main transl_fundef transl_globvar prog H). auto.
+  auto.
+  generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto.
+  rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog H).
+  generalize (transl_funcall_correct _ _ H0 H _ _ _ _ _ _ H4).
+  intro. eapply H1. 
   eapply function_ptr_well_typed; eauto.
   auto.
+  (* Divergence *)
+  assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)).
+    apply wt_program_main.
+    eapply Genv.find_funct_ptr_symbol_inversion; eauto. 
+  elim H1; clear H1; intros targs TYP.
+  assert (targs = Tnil).
+    inv H4; simpl in TYP.
+    inv H5. injection TYP. rewrite <- H9. simpl. auto.
+  subst targs.
+  exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]].
+  apply program_diverges with b tf.
+  rewrite (symbols_preserved _ _ H).
+  rewrite (transform_partial_program2_main transl_fundef transl_globvar prog H). auto.
+  auto.
+  generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto.
+  rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog H).
+  eapply transl_funcall_divergence_correct; eauto. 
+  eapply function_ptr_well_typed; eauto.
 Qed.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 3866669a..31d1d873 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -136,15 +136,10 @@ with expr_descr : Set :=
   | Ebinop: binary_operation -> expr -> expr -> expr_descr (**r binary operation *)
   | Ecast: type -> expr -> expr_descr   (**r type cast ([(ty) e]) *)
   | Eindex: expr -> expr -> expr_descr  (**r array indexing ([e1[e2]]) *)
-  | Ecall: expr -> exprlist -> expr_descr  (**r function call *)
   | Eandbool: expr -> expr -> expr_descr (**r sequential and ([&&]) *)
   | Eorbool: expr -> expr -> expr_descr (**r sequential or ([||]) *)
   | Esizeof: type -> expr_descr         (**r size of a type *)
-  | Efield: expr -> ident -> expr_descr (**r access to a member of a struct or union *)
-
-with exprlist : Set :=
-  | Enil: exprlist
-  | Econs: expr -> exprlist -> exprlist.
+  | Efield: expr -> ident -> expr_descr. (**r access to a member of a struct or union *)
 
 (** Extract the type part of a type-annotated Clight expression. *)
 
@@ -160,8 +155,8 @@ Definition typeof (e: expr) : type :=
 
 Inductive statement : Set :=
   | Sskip : statement                   (**r do nothing *)
-  | Sexpr : expr -> statement           (**r evaluate expression for its side-effects *)
   | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *)
+  | Scall: option expr -> expr -> list expr -> statement (**r function call *)
   | Ssequence : statement -> statement -> statement  (**r sequence *)
   | Sifthenelse : expr  -> statement -> statement -> statement (**r conditional *)
   | Swhile : expr -> statement -> statement   (**r [while] loop *)
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index cb572c09..72c4edf2 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -47,10 +47,6 @@ Inductive wt_expr: expr -> Prop :=
   | wt_Eindex: forall e1 e2 ty,
      wt_expr e1 -> wt_expr e2 ->
      wt_expr (Expr (Eindex e1 e2) ty)
-  | wt_Ecall: forall e1 el ty,
-     wt_expr e1 ->
-     wt_exprlist el ->
-     wt_expr (Expr (Ecall e1 el) ty)
   | wt_Eandbool: forall e1 e2 ty,
      wt_expr e1 -> wt_expr e2 ->
      wt_expr (Expr (Eandbool e1 e2) ty)
@@ -61,23 +57,32 @@ Inductive wt_expr: expr -> Prop :=
      wt_expr (Expr (Esizeof ty') ty)
   | wt_Efield: forall e id ty,
      wt_expr e ->
-     wt_expr (Expr (Efield e id) ty)
+     wt_expr (Expr (Efield e id) ty).
+
+Inductive wt_optexpr: option expr -> Prop :=
+  | wt_Enone:
+      wt_optexpr None
+  | wt_Esome: forall e,
+      wt_expr e ->
+      wt_optexpr (Some e).
 
-with wt_exprlist: exprlist -> Prop :=
+Inductive wt_exprlist: list expr -> Prop :=
   | wt_Enil:
-     wt_exprlist Enil
+     wt_exprlist nil
   | wt_Econs: forall e el,
-     wt_expr e -> wt_exprlist el -> wt_exprlist (Econs e el).
+     wt_expr e -> wt_exprlist el -> wt_exprlist (e :: el).
 
 Inductive wt_stmt: statement -> Prop :=
   | wt_Sskip:
      wt_stmt Sskip
-  | wt_Sexpr: forall e,
-     wt_expr e ->
-     wt_stmt (Sexpr e)
   | wt_Sassign: forall e1 e2,
      wt_expr e1 -> wt_expr e2 ->
      wt_stmt (Sassign e1 e2)
+  | wt_Scall: forall lhs e1 el,
+     wt_optexpr lhs ->
+     wt_expr e1 ->
+     wt_exprlist el ->
+     wt_stmt (Scall lhs e1 el)
   | wt_Ssequence: forall s1 s2,
      wt_stmt s1 -> wt_stmt s2 ->
      wt_stmt (Ssequence s1 s2)
@@ -97,11 +102,9 @@ Inductive wt_stmt: statement -> Prop :=
      wt_stmt Sbreak
   | wt_Scontinue:
      wt_stmt Scontinue
-  | wt_Sreturn_some: forall e,
-     wt_expr e ->
-     wt_stmt (Sreturn (Some e))
-  | wt_Sreturn_none:
-     wt_stmt (Sreturn None)
+  | wt_Sreturn: forall opte,
+     wt_optexpr opte ->
+     wt_stmt (Sreturn opte)
   | wt_Sswitch: forall e sl,
      wt_expr e -> wt_lblstmts sl ->
      wt_stmt (Sswitch e sl)
@@ -282,49 +285,35 @@ with typecheck_exprdescr (a: Csyntax.expr_descr) (ty: type) {struct a} : bool :=
   | Csyntax.Ebinop op b c => typecheck_expr b && typecheck_expr c
   | Csyntax.Ecast ty b => typecheck_expr b
   | Csyntax.Eindex b c => typecheck_expr b && typecheck_expr c
-  | Csyntax.Ecall b cl => typecheck_expr b && typecheck_exprlist cl
   | Csyntax.Eandbool b c => typecheck_expr b && typecheck_expr c
   | Csyntax.Eorbool b c => typecheck_expr b && typecheck_expr c
   | Csyntax.Esizeof ty => true
   | Csyntax.Efield b i => typecheck_expr b
-  end
+  end.
 
-with typecheck_exprlist (al: Csyntax.exprlist): bool :=
+Fixpoint typecheck_exprlist (al: list Csyntax.expr): bool :=
   match al with
-  | Csyntax.Enil => true
-  | Csyntax.Econs a1 a2 => typecheck_expr a1 && typecheck_exprlist a2
+  | nil => true
+  | a1 :: a2 => typecheck_expr a1 && typecheck_exprlist a2
+  end.
+
+Definition typecheck_optexpr (opta: option Csyntax.expr): bool :=
+  match opta with
+  | None => true
+  | Some a => typecheck_expr a
   end.
 
-Scheme expr_ind_3 := Induction for expr Sort Prop
-  with expr_descr_ind_3 := Induction for expr_descr Sort Prop
-  with exprlist_ind_3 := Induction for exprlist Sort Prop.
+Scheme expr_ind_2 := Induction for expr Sort Prop
+  with expr_descr_ind_2 := Induction for expr_descr Sort Prop.
 
 Lemma typecheck_expr_correct:
   forall a, typecheck_expr a = true -> wt_expr env a.
 Proof.
-  apply (expr_ind_3 (fun a => typecheck_expr a = true -> wt_expr env a)
-                    (fun a => forall ty, typecheck_exprdescr a ty = true -> wt_expr env (Expr a ty))
-                    (fun a => typecheck_exprlist a = true -> wt_exprlist env a));
-  simpl; intros; TrueInv.
-  auto.
-  constructor.
-  constructor.
-  constructor. destruct (env!i). decEq; symmetry; apply eq_type_correct; auto.
+  apply (expr_ind_2 (fun a => typecheck_expr a = true -> wt_expr env a)
+                    (fun a => forall ty, typecheck_exprdescr a ty = true -> wt_expr env (Expr a ty)));
+  simpl; intros; TrueInv; try constructor; auto.
+  destruct (env!i). decEq; symmetry; apply eq_type_correct; auto.
   discriminate.
-  constructor; auto.
-  constructor; auto.
-  constructor; auto.
-  constructor; auto.
-  constructor; auto.
-  constructor; auto.
-  constructor; auto.
-  constructor; auto.
-  constructor; auto.
-  auto.
-  constructor; auto.
-  constructor; auto.
-  constructor.
-  constructor; auto.
 Qed.
 
 Lemma typecheck_exprlist_correct:
@@ -335,11 +324,19 @@ Proof.
   TrueInv. constructor; auto. apply typecheck_expr_correct; auto.
 Qed.
 
+Lemma typecheck_optexpr_correct:
+  forall a, typecheck_optexpr a = true -> wt_optexpr env a.
+Proof.
+  destruct a; simpl; intros.
+  constructor. apply typecheck_expr_correct; auto.
+  constructor.
+Qed.
+
 Fixpoint typecheck_stmt (s: Csyntax.statement) {struct s} : bool :=
   match s with
   | Csyntax.Sskip => true
-  | Csyntax.Sexpr e => typecheck_expr e
   | Csyntax.Sassign b c => typecheck_expr b && typecheck_expr c
+  | Csyntax.Scall a b cl => typecheck_optexpr a && typecheck_expr b && typecheck_exprlist cl
   | Csyntax.Ssequence s1 s2 => typecheck_stmt s1 && typecheck_stmt s2
   | Csyntax.Sifthenelse e s1 s2 =>
       typecheck_expr e && typecheck_stmt s1 && typecheck_stmt s2
@@ -368,10 +365,11 @@ Lemma typecheck_stmt_correct:
   forall s, typecheck_stmt s = true -> wt_stmt env s.
 Proof.
   generalize typecheck_expr_correct; intro.
+  generalize typecheck_exprlist_correct; intro.
+  generalize typecheck_optexpr_correct; intro.
   apply (stmt_ind_2 (fun s => typecheck_stmt s = true -> wt_stmt env s)
                     (fun s => typecheck_lblstmts s = true -> wt_lblstmts env s));
-  simpl; intros; TrueInv; try constructor; auto.
-  destruct o; constructor; auto.
+  simpl; intros; TrueInv; constructor; auto.
 Qed.
 
 End TYPECHECKING.