Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


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

7 files changed, 4436 insertions, 0 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
new file mode 100644
index 0000000..b73e83c
--- /dev/null
+++ b/cfrontend/Csem.v
@@ -0,0 +1,752 @@
+(** * Dynamic semantics for the Clight language *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import AST.
+Require Import Mem.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Csyntax.
+
+(** ** Semantics of type-dependent operations *)
+
+Inductive is_false: val -> type -> Prop :=
+  | is_false_int: forall sz sg,
+      is_false (Vint Int.zero) (Tint sz sg)
+  | is_false_pointer: forall t,
+      is_false (Vint Int.zero) (Tpointer t)
+ | is_false_float: forall sz,
+      is_false (Vfloat Float.zero) (Tfloat sz).
+
+Inductive is_true: val -> type -> Prop :=
+  | is_true_int_int: forall n sz sg,
+      n <> Int.zero ->
+      is_true (Vint n) (Tint sz sg)
+  | is_true_pointer_int: forall b ofs sz sg,
+      is_true (Vptr b ofs) (Tint sz sg)
+  | is_true_int_pointer: forall n t,
+      n <> Int.zero ->
+      is_true (Vint n) (Tpointer t)
+  | is_true_pointer_pointer: forall b ofs t,
+      is_true (Vptr b ofs) (Tpointer t)
+ | is_true_float: forall f sz,
+      f <> Float.zero ->
+      is_true (Vfloat f) (Tfloat sz).
+
+Inductive bool_of_val : val -> type -> val -> Prop :=
+  | bool_of_val_true:   forall v ty, 
+         is_true v ty -> 
+         bool_of_val v ty Vtrue
+  | bool_of_val_false:   forall v ty,
+        is_false v ty ->
+        bool_of_val v ty Vfalse.
+
+Function sem_neg (v: val) (ty: type) : option val :=
+  match ty with
+  | Tint _ _ =>
+      match v with
+      | Vint n => Some (Vint (Int.neg n))
+      | _ => None
+      end
+  | Tfloat _ =>
+      match v with
+      | Vfloat f => Some (Vfloat (Float.neg f))
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Function sem_notint (v: val) : option val :=
+  match v with
+  | Vint n => Some (Vint (Int.xor n Int.mone))
+  | _ => None
+  end.
+
+Function sem_notbool (v: val) (ty: type) : option val :=
+  match ty with
+  | Tint _ _ =>
+      match v with
+      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
+      | Vptr _ _ => Some Vfalse
+      | _ => None
+      end
+  | Tpointer _ =>
+      match v with
+      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
+      | Vptr _ _ => Some Vfalse
+      | _ => None
+      end
+  | Tfloat _ =>
+      match v with
+      | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero))
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_add t1 t2 with 
+  | add_case_ii =>  
+      match v1, v2 with
+      | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
+      | _,  _ => None
+      end
+  | add_case_ff =>
+      match v1, v2 with
+      | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2))
+      | _,  _ => None
+      end
+  | add_case_pi ty=>
+      match v1,v2 with
+      | Vptr b1 ofs1, Vint n2 => 
+	Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
+      | _,  _ => None
+      end   
+  | add_default => None
+end.
+
+Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_sub t1 t2 with
+  | sub_case_ii =>               (* integer subtraction *)
+      match v1,v2 with
+      | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
+      | _,  _ => None
+      end 
+  | sub_case_ff =>               (* float subtraction *)
+      match v1,v2 with
+      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2))
+      | _,  _ => None
+      end
+  | sub_case_pi ty =>            (*array| pointer - offset *)
+      match v1,v2 with
+      | Vptr b1 ofs1, Vint n2 => 
+            Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
+      | _,  _ => None
+      end
+  | sub_case_pp ty =>          (* array|pointer - array|pointer *)
+      match v1,v2 with
+      | Vptr b1 ofs1, Vptr b2 ofs2 =>
+          if zeq b1 b2 then
+            if Int.eq (Int.repr (sizeof ty)) Int.zero then None
+            else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty))))
+          else None
+      | _, _ => None
+      end
+  | sub_default => None
+  end.
+ 
+Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+ match classify_mul t1 t2 with
+  | mul_case_ii =>
+      match v1,v2 with
+      | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2))
+      | _,  _ => None
+      end
+  | mul_case_ff =>
+      match v1,v2 with
+      | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
+      | _,  _ => None
+      end
+  | mul_default =>
+      None
+end.
+
+Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+   match classify_div t1 t2 with
+  | div_case_I32unsi =>
+      match v1,v2 with
+      | Vint n1, Vint n2 =>
+          if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
+      | _,_ => None
+      end
+  | div_case_ii =>
+      match v1,v2 with
+       | Vint n1, Vint n2 =>
+          if Int.eq n2 Int.zero then None else Some (Vint(Int.divs n1 n2))
+      | _,_ => None
+      end
+  | div_case_ff =>
+      match v1,v2 with
+      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2))
+      | _,  _ => None
+      end 
+  | div_default =>
+      None
+end.
+
+Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_mod t1 t2 with
+  | mod_case_I32unsi =>
+      match v1, v2 with
+      | Vint n1, Vint n2 =>
+          if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
+      | _, _ => None
+      end
+  | mod_case_ii =>
+      match v1,v2 with
+      | Vint n1, Vint n2 =>
+          if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
+      | _, _ => None
+      end
+  | mod_default =>
+      None
+  end.
+
+Function sem_and (v1 v2: val) : option val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2))
+  | _, _ => None
+  end .
+
+Function sem_or (v1 v2: val) : option val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2))
+  | _, _ => None
+  end. 
+
+Function sem_xor (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2))
+  | _, _ => None
+  end.
+
+Function sem_shl (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 =>
+     if Int.ltu n2 (Int.repr 32) then Some (Vint(Int.shl n1 n2)) else None
+  | _, _ => None
+  end.
+
+Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val :=
+  match classify_shr t1 t2 with 
+  | shr_case_I32unsi => 
+      match v1,v2 with 
+      | Vint n1, Vint n2 =>
+          if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
+      | _,_ => None
+      end
+   | shr_case_ii => 
+      match v1,v2 with
+      | Vint n1,  Vint n2 =>
+          if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
+      | _,  _ => None
+      end
+   | shr_default=>
+      None
+   end.
+
+Function sem_cmp_mismatch (c: comparison): option val :=
+  match c with
+  | Ceq =>  Some Vfalse
+  | Cne =>  Some Vtrue
+  | _   => None
+  end.
+
+Function sem_cmp (c:comparison)
+                  (v1: val) (t1: type) (v2: val) (t2: type)
+                  (m: mem): option val :=
+  match classify_cmp t1 t2 with
+  | cmp_case_I32unsi =>
+      match v1,v2 with
+      | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmpu c n1 n2))
+      | _,  _ => None
+      end
+  | cmp_case_ii =>
+      match v1,v2 with
+      | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmp c n1 n2))
+      | _,  _ => None
+      end
+  | cmp_case_ff =>
+      match v1,v2 with
+      | Vfloat f1, Vfloat f2 =>Some (Val.of_bool (Float.cmp c f1 f2))  
+      | _,  _ => None
+      end
+  | cmp_case_pi =>
+      match v1,v2 with
+      | Vptr b ofs, Vint n2 =>
+          if Int.eq n2 Int.zero then sem_cmp_mismatch c else None
+      | _,  _ => None
+      end
+  | cmp_case_pp =>
+      match v1,v2 with
+      | Vptr b1 ofs1,  Vptr b2 ofs2  =>
+          if valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b2 (Int.signed ofs2) then
+            if zeq b1 b2
+            then Some (Val.of_bool (Int.cmp c ofs1 ofs2))
+            else None
+          else None
+      | _,  _ => None
+      end 
+  | cmp_default => None
+  end.
+
+Definition sem_unary_operation
+            (op: unary_operation) (v: val) (ty: type): option val :=
+  match op with
+  | Onotbool => sem_notbool v ty
+  | Onotint => sem_notint v
+  | Oneg => sem_neg v ty
+  end.
+
+Definition sem_binary_operation
+    (op: binary_operation)
+    (v1: val) (t1: type) (v2: val) (t2:type)
+    (m: mem): option val :=
+  match op with
+  | Oadd => sem_add v1 t1 v2 t2
+  | Osub => sem_sub v1 t1 v2 t2 
+  | Omul => sem_mul v1 t1 v2 t2
+  | Omod => sem_mod v1 t1 v2 t2
+  | Odiv => sem_div v1 t1 v2 t2 
+  | Oand => sem_and v1 v2  
+  | Oor  => sem_or v1 v2 
+  | Oxor  => sem_xor v1 v2 
+  | Oshl => sem_shl v1 v2 
+  | Oshr  => sem_shr v1 t1 v2 t2   
+  | Oeq => sem_cmp Ceq v1 t1 v2 t2 m
+  | One => sem_cmp Cne v1 t1 v2 t2 m
+  | Olt => sem_cmp Clt v1 t1 v2 t2 m
+  | Ogt => sem_cmp Cgt v1 t1 v2 t2 m
+  | Ole => sem_cmp Cle v1 t1 v2 t2 m
+  | Oge => sem_cmp Cge v1 t1 v2 t2 m
+  end.
+
+Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
+  match sz, sg with
+  | I8, Signed => Int.cast8signed i
+  | I8, Unsigned => Int.cast8unsigned i
+  | I16, Signed => Int.cast16signed i
+  | I16, Unsigned => Int.cast16unsigned i 
+  | I32 , _ => i
+  end.
+
+Definition cast_int_float (si : signedness) (i: int) : float :=
+  match si with
+  | Signed => Float.floatofint i
+  | Unsigned => Float.floatofintu i
+  end.
+
+Definition cast_float_float (sz: floatsize) (f: float) : float :=
+  match sz with
+  | F32 => Float.singleoffloat f
+  | F64 => f
+  end.
+
+Inductive cast : val -> type -> type -> val -> Prop :=
+  | cast_ii:   forall i sz2 sz1 si1 si2,
+      cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
+           (Vint (cast_int_int sz2 si2 i))
+  | cast_fi:   forall f sz1 sz2 si2,
+      cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
+           (Vint (cast_int_int sz2 si2 (Float.intoffloat f)))
+  | cast_if:   forall i sz1 sz2 si1,
+      cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
+          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
+  | cast_ff:   forall f sz1 sz2,
+      cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)
+           (Vfloat (cast_float_float sz2 f))
+  | cast_ip_p:   forall b ofs t1 si2,
+      cast (Vptr b ofs) (Tint I32 si2) (Tpointer t1) (Vptr b ofs)
+  | cast_pi_p:   forall b ofs t1 si2,
+      cast (Vptr b ofs) (Tpointer t1) (Tint I32 si2) (Vptr b ofs)
+  | cast_pp_p:    forall b ofs t1 t2,
+      cast (Vptr b ofs) (Tpointer t1) (Tpointer t2) (Vptr b ofs)
+  | cast_ip_i:   forall n t1 si2,
+      cast (Vint n) (Tint I32 si2) (Tpointer t1) (Vint n)
+  | cast_pi_i:   forall n t1 si2,
+      cast (Vint n) (Tpointer t1) (Tint I32 si2) (Vint n)
+  | cast_pp_i:    forall n t1 t2,
+      cast (Vint n) (Tpointer t1) (Tpointer t2) (Vint n).
+
+(** ** Operational semantics *)
+
+(** Global environment *)
+
+Definition genv := Genv.t fundef.
+
+Definition globalenv (p: program) : genv :=
+  Genv.globalenv (program_of_program p).
+
+Definition init_mem (p: program) : mem :=  
+  Genv.init_mem (program_of_program p).
+
+(** Local environment *)
+
+Definition env := PTree.t block. (* map variable -> location *)
+
+Definition empty_env: env := (PTree.empty block).
+
+(** Outcomes for statements *)
+
+Inductive outcome: Set :=
+   | Out_break: outcome
+   | Out_continue: outcome
+   | Out_normal: outcome
+   | Out_return: option val -> outcome.
+
+Inductive out_normal_or_continue : outcome -> Prop :=
+  | Out_normal_or_continue_N: out_normal_or_continue Out_normal
+  | Out_normal_or_continue_C: out_normal_or_continue Out_continue.
+
+Inductive out_break_or_return : outcome -> outcome -> Prop :=
+  | Out_break_or_return_B: out_break_or_return Out_break Out_normal
+  | Out_break_or_return_R: forall ov,
+      out_break_or_return (Out_return ov) (Out_return ov).
+
+Definition outcome_switch (out: outcome) : outcome :=
+  match out with
+  | Out_break => Out_normal
+  | o => o
+  end.
+
+Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
+  match out, t with
+  | Out_normal, Tvoid => v = Vundef
+  | Out_return None, Tvoid => v = Vundef
+  | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v
+  | _, _ => False
+  end. 
+
+(** Selection of the appropriate case of a [switch] *)
+
+Fixpoint select_switch (n: int) (sl: labeled_statements)
+                       {struct sl}: labeled_statements :=
+  match sl with
+  | LSdefault _ => sl
+  | LScase c s sl' => if Int.eq c n then sl else select_switch n sl'
+  end.
+
+(** Loads and stores by type *)
+
+Definition load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val :=
+  match access_mode ty with
+  | By_value chunk => Mem.loadv chunk m (Vptr b ofs)
+  | By_reference => Some (Vptr b ofs)
+  | By_nothing => None
+  end.
+
+Definition store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem :=
+  match access_mode ty_dest with
+  | By_value chunk => Mem.storev chunk m (Vptr loc ofs) v
+  | By_reference => None
+  | By_nothing => None
+  end.
+
+(** Allocation and initialization of function-local variables *)
+
+Inductive alloc_variables: env -> mem ->
+                           list (ident * type) ->
+                           env -> mem -> list block -> Prop :=
+  | alloc_variables_nil:
+      forall e m,
+      alloc_variables e m nil e m nil
+  | alloc_variables_cons:
+      forall e m id ty vars m1 b1 m2 e2 lb,
+      Mem.alloc m 0 (sizeof ty) = (m1, b1) ->
+      alloc_variables (PTree.set id b1 e) m1 vars e2 m2 lb ->
+      alloc_variables e m ((id, ty) :: vars) e2 m2 (b1 :: lb).
+
+Inductive bind_parameters: env ->
+                           mem -> list (ident * type) -> list val ->
+                           mem -> Prop :=
+  | bind_parameters_nil:
+      forall e m,
+      bind_parameters e m nil nil m
+  | bind_parameters_cons:
+      forall e m id ty params v1 vl b m1 m2,
+      PTree.get id e = Some b ->
+      store_value_of_type ty m b Int.zero v1 = Some m1 ->
+      bind_parameters e m1 params vl m2 ->
+      bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
+
+Section RELSEM.
+
+Variable ge: genv.
+
+(** Evaluation of an expression in r-value position *)
+
+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 ->
+      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 ->
+      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 ->
+      is_false v1 (typeof a1) -> 
+      eval_expr e m1 a2 t2 m2 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 ->
+      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 ->
+      is_true v1 (typeof a1) -> 
+      eval_expr e m1 a2 t2 m2 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 ->
+      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 
+
+(** Evaluation of an expression in l-value position *)
+
+with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop :=
+  | eval_Evar_local:   forall e m 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,
+      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 ->
+      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 fList i ty delta,
+      eval_lvalue e m a t m1 l ofs ->
+      typeof a = Tstruct fList ->
+      field_offset i fList = Some 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 fList i ty,
+      eval_lvalue e m a t m1 l ofs ->
+      typeof a = Tunion fList ->
+      eval_lvalue e m (Expr (Efield a i) ty) 
+                  t m1 l ofs
+
+(** Evaluation of a list of expressions *)
+
+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)
+
+(** Execution of a statement *)
+
+with 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_stmt e m (Sassign a1 a2)
+                (t1 ** t2) m3 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 ->
+      exec_stmt e m (Ssequence s1 s2)
+                (t1 ** t2) m2 out
+  | exec_Sseq_2:   forall e m s1 s2 t1 m1 out,
+      exec_stmt e m s1 t1 m1 out ->
+      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 ->
+      is_true v1 (typeof a) ->
+      exec_stmt e m1 s1 t2 m2 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 ->
+      is_false v1 (typeof a) ->
+      exec_stmt e m1 s2 t2 m2 out ->
+      exec_stmt e m (Sifthenelse a s1 s2)
+                (t1 ** t2) m2 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_stmt e m (Sreturn (Some a))
+                t m1 (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 ->
+      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 ->
+      is_true v (typeof a) ->
+      exec_stmt e m1 s t2 m2 out2 ->
+      out_break_or_return out2 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 ->
+      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 ->
+      is_false v (typeof a) ->
+      exec_stmt e m (Sdowhile a s)
+                (t1 ** t2) m2 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_stmt e m s t1 m1 out1 ->
+      out_normal_or_continue out1 ->
+      eval_expr e m1 a t2 m2 v ->
+      is_true v (typeof a) ->
+      exec_stmt e m2 (Sdowhile a s) t3 m3 out ->
+      exec_stmt e m (Sdowhile a s) 
+                (t1 ** t2 ** t3) m3 out
+  | exec_Sfor_start: forall e m s a1 a2 a3 out m1 m2 t1 t2,
+      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 ->
+      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 ->
+      is_true v (typeof a2) ->
+      exec_stmt e m1 s t2 m2 out2 ->
+      out_break_or_return out2 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 ->
+      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 (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 ->
+      exec_stmt e m (Sswitch a sl)
+                (t1 ** t2) m2 (outcome_switch out)
+
+(** Execution of a list of labeled statements *)
+
+with exec_lblstmts: env -> mem -> labeled_statements -> trace -> mem -> outcome -> Prop :=
+  | exec_LSdefault: forall e m s t m1 out,
+     exec_stmt e m s t m1 out ->
+     exec_lblstmts e m (LSdefault s) t m1 out
+  | exec_LScase_fallthrough: forall e m n s ls t1 m1 t2 m2 out,
+     exec_stmt e m s t1 m1 Out_normal ->
+     exec_lblstmts e m1 ls t2 m2 out ->
+     exec_lblstmts e m (LScase n s ls) (t1 ** t2) m2 out
+  | exec_LScase_stop: forall e m n s ls t m1 out,
+     exec_stmt e m s t m1 out -> out <> Out_normal ->
+     exec_lblstmts e m (LScase n s ls) t m1 out
+
+(** Evaluation of a function invocation *)
+
+with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
+  | eval_funcall_internal: forall m f vargs t e m1 lb m2 m3 out vres,
+      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 lb ->
+      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      exec_stmt e m2 f.(fn_body) t m3 out ->
+      outcome_result_value out f.(fn_return) vres ->
+      eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres
+  | eval_funcall_external: forall m id targs tres vargs t vres,
+      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.
+
+End RELSEM.
+
+(** Execution of a whole program *)
+
+Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
+  let ge := globalenv p in 
+  let m0 := 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 /\
+  type_of_fundef f = Tfunction Tnil (Tint I32 Signed) /\
+  eval_funcall ge m0 f nil t m1 r.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
new file mode 100644
index 0000000..58c0bb8
--- /dev/null
+++ b/cfrontend/Cshmgen.v
@@ -0,0 +1,598 @@
+Require Import Coqlib.
+Require Import Integers.
+Require Import Floats.
+Require Import AST.
+Require Import Csyntax.
+Require Import Csharpminor.
+
+(** The error monad *)
+
+Definition bind (A B: Set) (f: option A) (g: A -> option B) :=
+  match f with None => None | Some x => g x end.
+
+Implicit Arguments bind [A B].
+
+Notation "'do' X <- A ; B" := (bind A (fun X => B))
+   (at level 200, X ident, A at level 100, B at level 200).
+
+(** ** Operations on C types *)
+
+Definition signature_of_function (f: Csyntax.function) : signature :=
+  mksignature 
+   (typlist_of_typelist (type_of_params (Csyntax.fn_params f)))
+   (opttyp_of_type (Csyntax.fn_return f)).
+
+Definition chunk_of_type (ty: type): option memory_chunk :=
+  match access_mode ty with
+  | By_value chunk => Some chunk
+  | _ => None
+  end.
+
+Definition var_kind_of_type (ty: type): option var_kind :=
+  match ty with
+  | Tint I8 Signed => Some(Vscalar Mint8signed)
+  | Tint I8 Unsigned => Some(Vscalar Mint8unsigned)
+  | Tint I16 Signed => Some(Vscalar Mint16signed)
+  | Tint I16 Unsigned => Some(Vscalar Mint16unsigned)
+  | Tint I32 _ => Some(Vscalar Mint32)
+  | Tfloat F32 => Some(Vscalar Mfloat32)
+  | Tfloat F64 => Some(Vscalar Mfloat64)
+  | Tvoid => None
+  | Tpointer _ => Some(Vscalar Mint32)
+  | Tarray _ _ => Some(Varray (Csyntax.sizeof ty))
+  | Tfunction _ _ => None
+  | Tstruct fList => Some(Varray (Csyntax.sizeof ty))
+  | Tunion fList => Some(Varray (Csyntax.sizeof ty))
+end.
+  
+(** ** Csharpminor constructors *)
+
+(* The following functions build Csharpminor expressions that compute
+   the value of a C operation.  Most construction functions take
+   as arguments
+   - Csharpminor subexpressions that compute the values of the
+     arguments of the operation;
+   - The C types of the arguments of the operation.  These types
+     are used to insert the necessary numeric conversions and to
+     resolve operation overloading.
+   Most of these functions return an [option expr], with [None] 
+   denoting a case where the operation is not defined at the given types.
+*)
+
+Definition make_intconst (n: int) :=  Eop (Ointconst n) Enil.
+
+Definition make_floatconst (f: float) :=  Eop (Ofloatconst f) Enil.
+
+Definition make_unop (op: operation) (e: expr) :=  Eop op (Econs e Enil).
+
+Definition make_binop (op: operation) (e1 e2: expr) :=
+    Eop op (Econs e1 (Econs e2 Enil)).
+
+Definition make_floatofint (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => make_unop Ofloatofint e
+  | Unsigned => make_unop Ofloatofintu e
+  end.
+
+(* [make_boolean e ty] returns a Csharpminor expression that evaluates
+   to the boolean value of [e].  Recall that:
+     - in Csharpminor, [false] is the integer 0,
+       [true] any non-zero integer or any pointer
+     - in C, [false] is the integer 0, the null pointer, the float 0.0
+       [true] is any non-zero integer, non-null pointer, non-null float.
+*)
+Definition make_boolean (e: expr) (ty: type) :=
+  match ty with
+  | Tfloat _ => make_binop (Ocmpf Cne) e (make_floatconst Float.zero)
+  | _ => e
+  end.
+
+Definition make_neg (e: expr) (ty: type) :=
+  match ty with
+  | Tint _ _ => Some (make_binop Osub (make_intconst Int.zero) e)
+  | Tfloat _ => Some (make_unop Onegf e)
+  | _ => None
+  end.
+
+Definition make_notbool (e: expr) (ty: type) :=
+  make_binop (Ocmp Ceq) (make_boolean e ty) (make_intconst Int.zero).
+
+Definition make_notint (e: expr) (ty: type) :=
+  make_unop Onotint e.
+
+Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_add ty1 ty2 with
+  | add_case_ii => Some (make_binop Oadd e1 e2)
+  | add_case_ff => Some (make_binop Oaddf e1 e2)
+  | add_case_pi ty =>
+      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
+      Some (make_binop Oadd e1 (make_binop Omul n e2))
+  | add_default => None
+  end.
+
+Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_sub ty1 ty2 with
+  | sub_case_ii => Some (make_binop Osub e1 e2)
+  | sub_case_ff => Some (make_binop Osubf e1 e2)
+  | sub_case_pi ty =>
+      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
+      Some (make_binop Osub e1 (make_binop Omul n e2))
+  | sub_case_pp ty =>
+      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
+      Some (make_binop Odivu (make_binop Osub e1 e2) n)
+  | sub_default => None
+  end.
+
+Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_mul ty1 ty2 with
+  | mul_case_ii => Some (make_binop Omul e1 e2)
+  | mul_case_ff => Some (make_binop Omulf e1 e2)
+  | mul_default => None
+  end.
+
+Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_div ty1 ty2 with
+  | div_case_I32unsi => Some (make_binop Odivu e1 e2)
+  | div_case_ii => Some (make_binop Odiv e1 e2)
+  | div_case_ff => Some (make_binop Odivf e1 e2)
+  | div_default => None
+  end.
+
+Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_mod ty1 ty2 with
+  | mod_case_I32unsi => Some (make_binop Omodu e1 e2)
+  | mod_case_ii=> Some (make_binop Omod e1 e2)
+  | mod_default => None
+  end.
+
+Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oand e1 e2).
+
+Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oor e1 e2).
+
+Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oxor e1 e2).
+
+Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oshl e1 e2).
+
+Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_shr ty1 ty2 with
+  | shr_case_I32unsi => Some (make_binop Oshru e1 e2)
+  | shr_case_ii=> Some (make_binop Oshr e1 e2)
+  | shr_default => None
+  end.
+
+Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_cmp ty1 ty2 with
+  | cmp_case_I32unsi => Some (make_binop (Ocmpu c) e1 e2)
+  | cmp_case_ii => Some (make_binop (Ocmp c) e1 e2)
+  | cmp_case_ff => Some (make_binop (Ocmpf c) e1 e2)
+  | cmp_case_pi => Some (make_binop (Ocmp c) e1 e2)
+  | cmp_case_pp => Some (make_binop (Ocmp c) e1 e2)
+  | cmp_default => None
+  end.
+
+Definition make_andbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Econdition
+    (make_boolean e1 ty1)
+    (Econdition
+       (make_boolean e2 ty2)
+       (make_intconst Int.one)
+       (make_intconst Int.zero))
+    (make_intconst Int.zero).
+
+Definition make_orbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Econdition
+    (make_boolean e1 ty1)
+    (make_intconst Int.one)
+    (Econdition
+       (make_boolean e2 ty2)
+       (make_intconst Int.one)
+       (make_intconst Int.zero)).
+
+(* [make_cast from to e] applies to [e] the numeric conversions needed
+   to transform a result of type [from] to a result of type [to].
+   It is decomposed in two functions:
+   - [make_cast1]  converts between int/pointer and float if necessary
+   - [make_cast2]  converts to a "smaller" int or float type if necessary.
+*)
+
+Definition make_cast1 (from to: type) (e: expr) :=
+  match from, to with
+  | Tint _ uns, Tfloat _ => make_floatofint e uns
+  | Tfloat _, Tint _ _ => make_unop Ointoffloat e
+  | _, _ => e
+  end.
+
+Definition make_cast2 (from to: type) (e: expr) :=
+  match to with
+  | Tint I8 Signed => make_unop Ocast8signed e  
+  | Tint I8 Unsigned => make_unop Ocast8unsigned e  
+  | Tint I16 Signed => make_unop Ocast16signed e  
+  | Tint I16 Unsigned => make_unop Ocast16unsigned e  
+  | Tfloat F32 => make_unop Osingleoffloat e
+  | _ => e
+  end.
+
+Definition make_cast (from to: type) (e: expr) :=
+  make_cast2 from to (make_cast1 from to e).
+
+(* [make_load addr ty_res] loads a value of type [ty_res] from
+   the memory location denoted by the Csharpminor expression [addr].
+   If [ty_res] is an array or function type, returns [addr] instead,
+   as consistent with C semantics.
+*)
+
+Definition make_load (addr: expr) (ty_res: type) :=
+  match (access_mode ty_res) with
+  | By_value chunk => Some (Eload chunk addr)
+  | By_reference => Some addr
+  | By_nothing => None
+  end.
+
+(* [make_store addr ty_res rhs ty_rhs] stores the value of the
+   Csharpminor expression [rhs] into the memory location denoted by the
+   Csharpminor expression [addr].  
+   [ty] is the type of the memory location. *)
+
+Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
+  match access_mode ty with
+  | By_value chunk => Some (Sstore chunk addr rhs)
+  | _ => None
+  end.
+
+(** ** Reading and writing variables *)
+
+(* [var_get id ty] builds 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
+   of the corresponding CabsCoq memory block, while variables of other types
+   evaluate to the contents of the corresponding C memory block.
+*)
+
+Definition var_get (id: ident) (ty: type) :=
+  match access_mode ty with
+  | By_value chunk => Some (Evar id)
+  | By_reference => Some (Eaddrof id)
+  | _ => None
+  end.
+
+(* [var_set id ty rhs] stores the value of the Csharpminor
+   expression [rhs] into the CabsCoq variable [id] of type [ty].
+*)
+
+Definition var_set (id: ident) (ty: type) (rhs: expr) :=
+  match access_mode ty with
+  | By_value chunk => Some (Sassign id rhs)
+  | _ => None
+  end.
+
+(** ** Translation of operators *)
+
+Definition transl_unop (op: unary_operation) (a: expr) (ta: type) : option expr :=
+  match op with
+  | Csyntax.Onotbool => Some(make_notbool a ta)
+  | Csyntax.Onotint => Some(make_notint a ta)
+  | Csyntax.Oneg => make_neg a ta
+  end.
+
+Definition transl_binop (op: binary_operation) (a: expr) (ta: type)
+                                  (b: expr) (tb: type) : option expr :=
+  match op with
+  | Csyntax.Oadd => make_add a ta b tb
+  | Csyntax.Osub => make_sub a ta b tb
+  | Csyntax.Omul => make_mul a ta b tb
+  | Csyntax.Odiv => make_div a ta b tb
+  | Csyntax.Omod => make_mod a ta b tb
+  | Csyntax.Oand => make_and a ta b tb
+  | Csyntax.Oor  => make_or a ta b tb
+  | Csyntax.Oxor => make_xor a ta b tb
+  | Csyntax.Oshl => make_shl a ta b tb
+  | Csyntax.Oshr => make_shr a ta b tb
+  | Csyntax.Oeq => make_cmp Ceq a ta b tb
+  | Csyntax.One => make_cmp Cne a ta b tb
+  | Csyntax.Olt => make_cmp Clt a ta b tb
+  | Csyntax.Ogt => make_cmp Cgt a ta b tb
+  | Csyntax.Ole => make_cmp Cle a ta b tb
+  | Csyntax.Oge => make_cmp Cge a ta b tb
+  end.
+
+(** ** Translation of expressions *)
+
+(* [transl_expr a] returns the Csharpminor code that computes the value
+   of expression [a]. The result is an option type to enable error reporting.
+
+   Most cases are self-explanatory.  We outline the non-obvious cases:
+
+   a && b    --->    a ? (b ? 1 : 0) : 0
+
+   a || b    --->    a ? 1 : (b ? 1 : 0)
+*)
+
+Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
+  match a with
+  | Expr (Csyntax.Econst_int n) _ =>
+      Some(make_intconst n)
+  | Expr (Csyntax.Econst_float n) _ =>
+      Some(make_floatconst n)
+  | Expr (Csyntax.Evar id) ty =>
+      var_get id ty
+  | Expr (Csyntax.Ederef b) _ =>
+      do tb <- transl_expr b;
+      make_load tb (typeof a)
+  | Expr (Csyntax.Eaddrof b) _ =>
+      transl_lvalue b
+  | Expr (Csyntax.Eunop op b) _ =>
+      do tb <- transl_expr b;
+      transl_unop op tb (typeof b)
+  | Expr (Csyntax.Ebinop op b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      transl_binop op tb (typeof b) tc (typeof c)
+  | Expr (Csyntax.Ecast ty b) _ =>
+      do tb <- transl_expr b;
+      Some (make_cast (typeof b) ty tb)
+  | Expr (Csyntax.Eindex b c) ty =>
+      do tb <- transl_expr b;
+      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;
+          Some(Ecall (signature_of_type args res) tb tcl)
+      | _ => None
+      end 
+  | Expr (Csyntax.Eandbool b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      Some(make_andbool tb (typeof b) tc (typeof c))
+  | Expr (Csyntax.Eorbool b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      Some(make_orbool tb (typeof b) tc (typeof c))
+  | Expr (Csyntax.Esizeof ty) _ =>
+      Some(make_intconst (Int.repr (Csyntax.sizeof ty)))
+  | Expr (Csyntax.Efield b i) ty => 
+      match typeof b with
+      | Tstruct fld =>
+          do tb <- transl_lvalue b;
+          do ofs <- field_offset i fld;
+          make_load
+            (make_binop Oadd tb (make_intconst (Int.repr ofs)))
+            ty
+      | Tunion fld =>
+          do tb <- transl_lvalue b;
+          make_load tb ty
+      | _ => None
+      end
+  end
+
+(* [transl_lvalue a] returns the Csharpminor code that evaluates
+   [a] as a lvalue, that is, code that returns the memory address
+   where the value of [a] is stored.
+*)
+
+with transl_lvalue (a: Csyntax.expr) {struct a} : option expr :=
+  match a with
+  | Expr (Csyntax.Evar id) _ =>
+      Some (Eaddrof id)
+  | Expr (Csyntax.Ederef b) _ =>
+      transl_expr b
+  | Expr (Csyntax.Eindex b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      make_add tb (typeof b) tc (typeof c)
+  | Expr (Csyntax.Efield b i) ty => 
+      match typeof b with
+      | Tstruct fld =>
+          do tb <- transl_lvalue b;
+          do ofs <- field_offset i fld;
+          Some (make_binop Oadd tb (make_intconst (Int.repr ofs)))
+      | Tunion fld =>
+          transl_lvalue b
+      | _ => None
+      end
+  | _ => None
+  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): option exprlist :=
+  match al with
+  | Csyntax.Enil => Some Enil
+  | Csyntax.Econs a1 a2 =>
+      do ta1 <- transl_expr a1;
+      do ta2 <- transl_exprlist a2;
+      Some (Econs 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 CabsCoq expression [e] and performs an [exit 0] if [e]
+   evaluates to false.
+*)
+Definition exit_if_false (e: Csyntax.expr) : option stmt :=
+  do te <- transl_expr e;
+  Some(Sifthenelse
+        (make_notbool te (typeof e))
+        (Sexit 0%nat)
+        Sskip).
+
+(* [transl_statement nbrk ncnt s] returns a Csharpminor statement
+   that performs the same computations as the CabsCoq statement [s].
+
+   If the statement [s] terminates prematurely on a [break] construct,
+   the generated Csharpminor statement terminates prematurely on an
+   [exit nbrk] construct.
+
+   If the statement [s] terminates prematurely on a [continue]
+   construct, the generated Csharpminor statement terminates
+   prematurely on an [exit ncnt] construct.
+
+   Immediately within a loop, [nbrk = 1] and [ncnt = 0], but this 
+   changes when we're inside a [switch] construct.
+
+   The general translation for loops is as follows:
+
+while (e1) s;       --->     block {
+                               loop {
+                                 if (!e1) exit 0;
+                                 block { s }
+                                 // continue in s branches here
+                               }
+                             }
+                             // break in s branches here
+
+do s; while (e1);   --->     block {
+                               loop {
+                                 block { s }
+                                 // continue in s branches here
+                                 if (!e1) exit 0;
+                               }
+                             }
+                             // break in s branches here
+
+for (e1;e2;e3) s;   --->     e1;
+                             block {
+                               loop {
+                                 if (!e2) exit 0;
+                                 block { s }
+                                 // continue in s branches here
+                                 e3;
+                               }
+                             }
+                             // break in s branches here
+
+switch (e) {        --->    block { block { block { block {
+  case N1: s1;                switch (e) { N1: exit 0; N2: exit 1; default: exit 2; }
+  case N2: s2;                } ; s1  // with break -> exit 2  and continue -> exit 3
+  default: s;                 } ; s2  // with break -> exit 1  and continue -> exit 2
+}                             } ; s   // with break -> exit 0  and continue -> exit 1
+                              }
+*)
+
+Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int * nat) :=
+  match sl with
+  | LSdefault _ => nil
+  | LScase ni _ rem => (ni, k) :: switch_table rem (k+1)
+  end.
+
+Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : option stmt :=
+  match s with
+  | Csyntax.Sskip =>
+      Some Sskip
+  | Csyntax.Sexpr e =>
+      do te <- transl_expr e;
+      Some (Sexpr te)
+  | Csyntax.Sassign b c =>
+      match (is_variable b) with
+      | Some id =>
+          do tc <- transl_expr c;
+          var_set id (typeof b) tc
+      | None =>
+          do tb <- transl_lvalue b;
+          do tc <- transl_expr c;
+          make_store tb (typeof b) tc
+      end 
+  | Csyntax.Ssequence s1 s2 =>
+      do ts1 <- transl_statement nbrk ncnt s1;
+      do ts2 <- transl_statement nbrk ncnt s2;
+      Some (Sseq ts1 ts2)
+  | Csyntax.Sifthenelse e s1 s2 =>
+      do te <- transl_expr e;
+      do ts1 <- transl_statement nbrk ncnt s1;
+      do ts2 <- transl_statement nbrk ncnt s2;
+      Some (Sifthenelse (make_boolean te (typeof e)) ts1 ts2)
+  | Csyntax.Swhile e s1 =>
+      do te <- exit_if_false e;
+      do ts1 <- transl_statement 1%nat 0%nat s1;
+      Some (Sblock (Sloop (Sseq te (Sblock ts1))))
+  | Csyntax.Sdowhile e s1 =>
+      do te <- exit_if_false e;
+      do ts1 <- transl_statement 1%nat 0%nat s1;
+      Some (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;
+      Some (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))
+  | Csyntax.Sbreak =>
+      Some (Sexit nbrk)
+  | Csyntax.Scontinue =>
+      Some (Sexit ncnt)
+  | Csyntax.Sreturn (Some e) =>
+      do te <- transl_expr e;
+      Some (Sreturn (Some te))
+  | Csyntax.Sreturn None =>
+      Some (Sreturn None)
+  | Csyntax.Sswitch e sl =>
+      let cases := switch_table sl 0 in
+      let ncases := List.length cases in
+      do te <- transl_expr e;
+      transl_lblstmts ncases (ncnt + ncases + 1)%nat sl (Sblock (Sswitch te cases ncases))
+  end
+
+with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt)
+                     {struct sl}: option stmt :=
+  match sl with
+  | LSdefault s =>
+      do ts <- transl_statement nbrk ncnt s;
+      Some (Sblock (Sseq body ts))
+  | LScase _ s rem =>
+      do ts <- transl_statement nbrk ncnt s;
+      transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts))
+  end.
+
+(*** Translation of functions *)
+
+Definition transl_params := transf_partial_program chunk_of_type.
+Definition transl_vars := transf_partial_program var_kind_of_type.
+
+Definition transl_function (f: Csyntax.function) : option function :=
+  do tparams <- transl_params (Csyntax.fn_params f);
+  do tvars <- transl_vars (Csyntax.fn_vars f);
+  do tbody <- transl_statement 1%nat 0%nat (Csyntax.fn_body f);
+  Some (mkfunction (signature_of_function f) tparams tvars tbody).
+
+Definition transl_fundef (f: Csyntax.fundef) : option fundef :=
+  match f with
+  | Csyntax.Internal g => 
+      do tg <- transl_function g; Some(AST.Internal tg)
+  | Csyntax.External id args res =>
+      Some(AST.External (external_function id args res))
+  end.
+
+(** ** Translation of programs *)
+
+Fixpoint transl_global_vars
+      (vl: list (ident * type * list init_data)) :
+      option (list (ident * var_kind * list init_data)) :=
+  match vl with
+  | nil => Some nil
+  | (id, ty, init) :: rem =>
+      do vk <- var_kind_of_type ty;
+      do trem <- transl_global_vars rem;
+      Some ((id, vk, init) :: trem)
+  end.
+
+Definition transl_program (p: Csyntax.program) : option program :=
+  do tfun <- transf_partial_program transl_fundef (Csyntax.prog_funct p);
+  do tvars <- transl_global_vars (Csyntax.prog_defs p);
+  Some (mkprogram tfun (Csyntax.prog_main p) tvars).
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
new file mode 100644
index 0000000..17f7aa9
--- /dev/null
+++ b/cfrontend/Cshmgenproof1.v
@@ -0,0 +1,288 @@
+(** * Correctness of the C front end, part 1: syntactic properties *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Integers.
+Require Import Floats.
+Require Import AST.
+Require Import Values.
+Require Import Events.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Csyntax.
+Require Import Csem.
+Require Import Ctyping.
+Require Import Csharpminor.
+Require Import Cshmgen.
+
+(** Monadic simplification *)
+
+Ltac monadSimpl1 :=
+  match goal with
+  | [ |- (bind ?F ?G = Some ?X) -> _ ] =>
+      unfold bind at 1;
+      generalize (refl_equal F);
+      pattern F at -1 in |- *;
+      case F;
+      [ (let EQ := fresh "EQ" in
+           (intro; intro EQ; try monadSimpl1))
+      | intro; intro; discriminate ]
+  | [ |- (None = Some _) -> _ ] =>
+      intro; discriminate
+  | [ |- (Some _ = Some _) -> _ ] =>
+      let h := fresh "H" in
+      (intro h; injection h; intro; clear h)
+  | [ |- (_ = Some _) -> _ ] =>
+      let EQ := fresh "EQ" in intro EQ
+  end.
+
+Ltac monadSimpl :=
+  match goal with
+  | [ |- (bind ?F ?G = Some ?X) -> _ ] => monadSimpl1
+  | [ |- (None = Some _) -> _ ] => monadSimpl1
+  | [ |- (Some _ = Some _) -> _ ] => monadSimpl1
+  | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
+  | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
+  | [ |- (?F _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
+  | [ |- (?F _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
+  | [ |- (?F _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
+  | [ |- (?F _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
+  end.
+
+Ltac monadInv H :=
+  generalize H; monadSimpl.
+
+(** Operations on types *)
+
+Lemma transl_fundef_sig1:
+  forall f tf args res,
+  transl_fundef f = Some tf ->
+  classify_fun (type_of_fundef f) = fun_case_f args res ->
+  funsig tf = signature_of_type args res.
+Proof.
+  intros. destruct f; monadInv H. 
+  monadInv EQ. rewrite <- H2. rewrite <- H3. simpl. 
+  simpl in H0. inversion H0. reflexivity. 
+  rewrite <- H2. simpl. 
+  simpl in H0. congruence.
+Qed.
+
+Lemma transl_fundef_sig2:
+  forall f tf args res,
+  transl_fundef f = Some tf ->
+  type_of_fundef f = Tfunction args res ->
+  funsig tf = signature_of_type args res.
+Proof.
+  intros. eapply transl_fundef_sig1; eauto.
+  rewrite H0; reflexivity.
+Qed.
+
+Lemma var_kind_by_value:
+  forall ty chunk,
+  access_mode ty = By_value chunk ->
+  var_kind_of_type ty = Some(Vscalar chunk).
+Proof.
+  intros ty chunk; destruct ty; simpl; try congruence.
+  destruct i; try congruence; destruct s; congruence.
+  destruct f; congruence.
+Qed.
+
+Lemma sizeof_var_kind_of_type:
+  forall ty vk,
+  var_kind_of_type ty = Some vk ->
+  Csharpminor.sizeof vk = Csyntax.sizeof ty.
+Proof.
+  intros ty vk.
+  assert (sizeof (Varray (Csyntax.sizeof ty)) = Csyntax.sizeof ty).
+    simpl. rewrite Zmax_spec. apply zlt_false. 
+    generalize (Csyntax.sizeof_pos ty). omega.
+  destruct ty; try (destruct i; try destruct s); try (destruct f); 
+  simpl; intro EQ; inversion EQ; subst vk; auto.
+Qed.
+
+(** Transformation of programs and functions *)
+
+Lemma transform_program_of_program:
+  forall prog tprog,
+  transl_program prog = Some tprog ->
+  transform_partial_program transl_fundef (Csyntax.program_of_program prog) =
+  Some (program_of_program tprog).
+Proof.
+  intros prog tprog TRANSL.  
+  monadInv TRANSL. rewrite <- H0. unfold program_of_program; simpl. 
+  unfold transform_partial_program, Csyntax.program_of_program; simpl.
+  rewrite EQ. decEq. decEq. 
+  generalize EQ0. generalize l0. generalize (prog_defs prog).
+  induction l1; simpl; intros. 
+  inversion EQ1; subst l1. reflexivity.
+  destruct a as [[id ty] init]. monadInv EQ1. subst l2. simpl. decEq. apply IHl1. auto. 
+Qed.
+
+(** ** Some properties of the translation functions *)
+
+Lemma transf_partial_program_names:
+  forall (A B: Set) (f: A -> option B)
+         (l: list (ident * A)) (tl: list (ident * B)),
+  transf_partial_program f l = Some tl ->
+  List.map (@fst ident B) tl = List.map (@fst ident A) l.
+Proof.
+  induction l; simpl.
+  intros. inversion H. reflexivity.
+  intro tl. destruct a as [id x]. destruct (f x); try congruence.
+  caseEq (transf_partial_program f l); intros; try congruence.
+  inversion H0; subst tl. simpl. decEq. auto.
+Qed.
+   
+Lemma transf_partial_program_append:
+  forall (A B: Set) (f: A -> option B)
+         (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)),
+  transf_partial_program f l1 = Some tl1 ->
+  transf_partial_program f l2 = Some tl2 ->
+  transf_partial_program f (l1 ++ l2) = Some (tl1 ++ tl2).
+Proof.
+  induction l1; intros until tl2; simpl.
+  intros. inversion H. simpl; auto.
+  destruct a as [id x]. destruct (f x); try congruence.
+  caseEq (transf_partial_program f l1); intros; try congruence.
+  inversion H0. rewrite (IHl1 _ _ _ H H1). auto.
+Qed.
+ 
+Lemma transl_params_names:
+  forall vars tvars,
+  transl_params vars = Some tvars ->
+  List.map (@fst ident memory_chunk) tvars = Ctyping.var_names vars.
+Proof.
+  exact (transf_partial_program_names _ _ chunk_of_type).
+Qed.
+
+Lemma transl_vars_names:
+  forall vars tvars,
+  transl_vars vars = Some tvars ->
+  List.map (@fst ident var_kind) tvars = Ctyping.var_names vars.
+Proof.
+  exact (transf_partial_program_names _ _ var_kind_of_type).
+Qed.
+
+Lemma transl_names_norepet:
+  forall params vars sg tparams tvars body,
+  list_norepet (var_names params ++ var_names vars) ->
+  transl_params params = Some tparams ->
+  transl_vars vars = Some tvars ->
+  let f := Csharpminor.mkfunction sg tparams tvars body in
+  list_norepet (fn_params_names f ++ fn_vars_names f).
+Proof.
+  intros. unfold fn_params_names, fn_vars_names, f. simpl.
+  rewrite (transl_params_names _ _ H0).
+  rewrite (transl_vars_names _ _ H1).
+  auto.
+Qed.
+
+Lemma transl_vars_append:
+  forall l1 l2 tl1 tl2,
+  transl_vars l1 = Some tl1 -> transl_vars l2 = Some tl2 ->
+  transl_vars (l1 ++ l2) = Some (tl1 ++ tl2).
+Proof.
+  exact (transf_partial_program_append _ _ var_kind_of_type).
+Qed.
+
+Lemma transl_params_vars:
+  forall params tparams,
+  transl_params params = Some tparams ->
+  transl_vars params =
+  Some (List.map (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) tparams).
+Proof.
+  induction params; intro tparams; simpl.
+  intros. inversion H. reflexivity.
+  destruct a as [id x]. 
+  unfold chunk_of_type. caseEq (access_mode x); try congruence.
+  intros chunk AM. 
+  caseEq (transl_params params); intros; try congruence.
+  inversion H0. 
+  rewrite (var_kind_by_value _ _ AM). 
+  rewrite (IHparams _ H). reflexivity.
+Qed.
+
+Lemma transl_fn_variables:
+  forall params vars sg tparams tvars body,
+  transl_params params = Some tparams ->
+  transl_vars vars = Some tvars ->
+  let f := Csharpminor.mkfunction sg tparams tvars body in
+  transl_vars (params ++ vars) = Some (fn_variables f).
+Proof.
+  intros. 
+  generalize (transl_params_vars _ _ H); intro.
+  rewrite (transl_vars_append _ _ _ _ H1 H0).
+  reflexivity.
+Qed.
+
+(** Transformation of expressions and statements *)
+
+Lemma is_variable_correct:
+  forall a id,
+  is_variable a = Some id ->
+  a = Csyntax.Expr (Csyntax.Evar id) (typeof a).
+Proof.
+  intros until id. destruct a as [ad aty]; simpl. 
+  destruct ad; intros; try discriminate.
+  congruence.
+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 ->
+  transl_expr (Expr a ty) = Some ta ->
+  (exists id, a = Csyntax.Evar id /\ var_get id ty = Some ta) \/
+  (exists tb, transl_lvalue (Expr a ty) = Some tb /\
+              make_load tb ty = Some ta).
+Proof.
+  intros. inversion H; subst; clear H; simpl in H0.
+  left; exists id; auto.
+  left; exists id; auto.
+  monadInv H0. right. exists e0; split; auto. 
+  simpl. monadInv H0. right. exists e2; split; auto. 
+  simpl. rewrite H6 in H0. rewrite H6. 
+  monadInv H0. right. 
+  exists (make_binop Oadd e0 (make_intconst (Int.repr z))). split; auto.
+  simpl. rewrite H10 in H0. rewrite H10. 
+  monadInv H0. right. 
+  exists e0; auto.
+Qed.
+
+Lemma transl_stmt_Sfor_start:
+  forall nbrk ncnt s1 e2 s3 s4 ts,
+  transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = Some ts ->
+  exists ts1, exists ts2,
+    ts = Sseq ts1 ts2
+  /\ transl_statement nbrk ncnt s1 = Some ts1
+  /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = Some (Sseq Sskip ts2).
+Proof.
+  intros. monadInv H. simpl. 
+  exists s; exists (Sblock (Sloop (Sseq s0 (Sseq (Sblock s5) s2)))).
+  intuition.
+Qed.
+
+(** Properties related to switch constructs *)
+
+Fixpoint lblstmts_length (sl: labeled_statements) : nat :=
+  match sl with
+  | LSdefault _ => 0%nat
+  | LScase _ _ sl' => S (lblstmts_length sl')
+  end.
+
+Lemma switch_target_table_shift:
+  forall n sl base dfl,
+  switch_target n (S dfl) (switch_table sl (S base)) =
+  S(switch_target n dfl (switch_table sl base)).
+Proof.
+  induction sl; intros; simpl.
+  auto.
+  case (Int.eq n i). auto. auto. 
+Qed.
+
+Lemma length_switch_table:
+  forall sl base, List.length (switch_table sl base) = lblstmts_length sl.
+Proof.
+  induction sl; intro; simpl. auto. decEq; auto. 
+Qed.
+
+
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
new file mode 100644
index 0000000..602e33a
--- /dev/null
+++ b/cfrontend/Cshmgenproof2.v
@@ -0,0 +1,419 @@
+(** * Correctness of the C front end, part 2: Csharpminor construction functions *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Integers.
+Require Import Floats.
+Require Import AST.
+Require Import Values.
+Require Import Events.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Csyntax.
+Require Import Csem.
+Require Import Ctyping.
+Require Import Csharpminor.
+Require Import Cshmgen.
+Require Import Cshmgenproof1.
+
+Section CONSTRUCTORS.
+
+Variable tprog: Csharpminor.program.
+
+(** Properties of the translation of [switch] constructs. *)
+
+Lemma transl_lblstmts_exit:
+  forall e m1 t m2 sl body n tsl nbrk ncnt,
+  exec_stmt tprog e m1 body t m2 (Out_exit (lblstmts_length sl + n)) ->
+  transl_lblstmts nbrk ncnt sl body = Some tsl ->
+  exec_stmt tprog e m1 tsl t m2 (outcome_block (Out_exit n)).
+Proof.
+  induction sl; intros.
+  simpl in H; simpl in H0; monadInv H0. 
+  rewrite <- H2. constructor. apply exec_Sseq_stop. auto. congruence.
+  simpl in H; simpl in H0; monadInv H0.
+  eapply IHsl with (body := Sblock (Sseq body s0)); eauto.
+  change (Out_exit (lblstmts_length sl + n))
+    with (outcome_block (Out_exit (S (lblstmts_length sl + n)))).
+  constructor. apply exec_Sseq_stop. auto. congruence.
+Qed.
+
+Lemma transl_lblstmts_return:
+  forall e m1 t m2 sl body optv tsl nbrk ncnt,
+  exec_stmt tprog e m1 body t m2 (Out_return optv) ->
+  transl_lblstmts nbrk ncnt sl body = Some tsl ->
+  exec_stmt tprog e m1 tsl t m2 (Out_return optv).
+Proof.
+  induction sl; intros.
+  simpl in H; simpl in H0; monadInv H0. 
+  rewrite <- H2. change (Out_return optv) with (outcome_block (Out_return optv)).
+  constructor. apply exec_Sseq_stop. auto. congruence.
+  simpl in H; simpl in H0; monadInv H0.
+  eapply IHsl with (body := Sblock (Sseq body s0)); eauto.
+  change (Out_return optv) with (outcome_block (Out_return optv)).
+  constructor. apply exec_Sseq_stop. auto. congruence.
+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).
+Proof.
+  intros. unfold make_intconst. econstructor. constructor. 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).
+Proof.
+  intros. unfold make_floatconst. econstructor. constructor. reflexivity. 
+Qed.
+
+Lemma make_unop_correct:
+  forall op le e m1 a ta m2 va v,
+  Csharpminor.eval_expr tprog le e m1 a ta m2 va ->
+  eval_operation op (va :: nil) m2 = Some v ->
+  Csharpminor.eval_expr tprog le e m1 (make_unop op a) ta m2 v.
+Proof.
+  intros. unfold make_unop. econstructor. econstructor. eauto. constructor.
+  traceEq. auto.
+Qed.
+
+Lemma make_binop_correct:
+  forall op le e m1 a ta m2 va b tb m3 vb t v,
+  Csharpminor.eval_expr tprog le e m1 a ta m2 va ->
+  Csharpminor.eval_expr tprog le e m2 b tb m3 vb ->
+  eval_operation op (va :: vb :: nil) m3 = Some v ->
+  t = ta ** tb ->
+  Csharpminor.eval_expr tprog le e m1 (make_binop op a b) t m3 v.
+Proof.
+  intros. unfold make_binop. 
+  econstructor. econstructor. eauto. econstructor. eauto. constructor.
+  reflexivity. traceEq. auto.
+Qed.
+
+Hint Resolve make_intconst_correct make_floatconst_correct
+             make_unop_correct make_binop_correct: cshm.
+Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
+
+Remark Vtrue_is_true: Val.is_true Vtrue.
+Proof.
+  simpl. apply Int.one_not_zero.
+Qed.
+
+Remark Vfalse_is_false: Val.is_false Vfalse.
+Proof.
+  simpl. auto.
+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 ->
+  is_true v ty ->
+  exists vb,
+    Csharpminor.eval_expr tprog le e m1 (make_boolean a ty) t m2 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.
+  eapply make_binop_correct; 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.
+  rewrite Float.cmp_ne_eq. auto.
+  apply Vtrue_is_true.
+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 ->
+  is_false v ty ->
+  exists vb,
+    Csharpminor.eval_expr tprog le e m1 (make_boolean a ty) t m2 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.
+  eapply make_binop_correct; 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. 
+  rewrite Float.cmp_ne_eq. auto.
+  apply Vfalse_is_false.
+Qed.
+
+Lemma make_neg_correct:
+  forall a tya c ta va v le e m1 m2,
+  sem_neg va tya = Some v ->
+  make_neg a tya = Some c ->  
+  eval_expr tprog le e m1 a ta m2 va ->
+  eval_expr tprog le e m1 c ta m2 v.
+Proof.
+  intros until m2; intro SEM. unfold make_neg. 
+  functional inversion SEM; intros.
+  inversion H4. eapply make_binop_correct; eauto with cshm.
+  inversion H4. eauto with cshm.
+Qed.
+
+Lemma make_notbool_correct:
+  forall a tya c ta va v le e m1 m2,
+  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.
+Proof.
+  intros until m2; intro SEM. unfold make_notbool. 
+  functional inversion SEM; intros; inversion H4; simpl;
+  eauto with cshm.
+  eapply make_binop_correct. 
+  eapply make_binop_correct. eauto. eauto with cshm. 
+  simpl; reflexivity. reflexivity. eauto with cshm. 
+  simpl. rewrite Float.cmp_ne_eq. 
+  destruct (Float.cmp Ceq f Float.zero); reflexivity.
+  traceEq.
+Qed.
+
+Lemma make_notint_correct:
+  forall a tya c ta va v le e m1 m2,
+  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.
+Proof.
+  intros until m2; intro SEM. unfold make_notint. 
+  functional inversion SEM; intros. 
+  inversion H2; eauto with cshm.
+Qed.
+
+Definition binary_constructor_correct
+    (make: expr -> type -> expr -> type -> option 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,
+  sem va tya vb tyb = Some v ->
+  make a tya b tyb = Some 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.
+
+Definition binary_constructor_correct'
+    (make: expr -> type -> expr -> type -> option expr)
+    (sem: val -> val -> option val): Prop :=
+  forall a tya b tyb c ta va tb vb v le e m1 m2 m3,
+  sem va vb = Some v ->
+  make a tya b tyb = Some 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.
+
+Lemma make_add_correct: binary_constructor_correct make_add sem_add.
+Proof.
+  red; intros until m3. intro SEM. unfold make_add. 
+  functional inversion SEM; rewrite H0; intros.
+  inversion H7. eauto with cshm. 
+  inversion H7. eauto with cshm.
+  inversion H7. 
+  eapply make_binop_correct. eauto. 
+  eapply make_binop_correct. 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. 
+  functional inversion SEM; rewrite H0; intros;
+  inversion H7; eauto with cshm. 
+  eapply make_binop_correct. eauto. 
+  eapply make_binop_correct. eauto with cshm. eauto.
+  simpl. reflexivity. reflexivity. 
+  simpl. reflexivity. traceEq.
+  inversion H9. eapply make_binop_correct. 
+  eapply make_binop_correct; eauto. 
+  simpl. unfold eq_block; rewrite H3. reflexivity.
+  eauto with cshm. simpl. rewrite H8. reflexivity. traceEq.
+Qed.
+
+Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul.
+Proof.
+  red; intros until m3. 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. 
+  functional inversion SEM; rewrite H0; intros.
+  inversion H8. eapply make_binop_correct; eauto with cshm. 
+  simpl. rewrite H7; auto.
+  inversion H8. eapply make_binop_correct; 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. 
+  functional inversion SEM; rewrite H0; intros.
+  inversion H8. eapply make_binop_correct; eauto with cshm. 
+  simpl. rewrite H7; auto.
+  inversion H8. eapply make_binop_correct; 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. 
+  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. 
+  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. 
+  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. 
+  functional inversion SEM. intros. inversion H5. 
+  eapply make_binop_correct; 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. 
+  functional inversion SEM; intros; rewrite H0 in H8; inversion H8.
+  eapply make_binop_correct; eauto with cshm.
+  simpl; rewrite H7; auto.
+  eapply make_binop_correct; 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 ->
+  make_cmp cmp a tya b tyb = Some 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.
+Proof.
+  intros until m3. 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. eapply make_binop_correct; eauto with cshm.
+  simpl. functional inversion H; subst; unfold eval_compare_null;
+  rewrite H8; auto.
+  inversion H10. eapply make_binop_correct; 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, 
+  transl_unop op a tya = Some 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.
+Proof.
+  intros. destruct op; simpl in *.
+  eapply make_notbool_correct; eauto. congruence.
+  eapply make_notint_correct with (tya := tya); eauto. congruence.
+  eapply make_neg_correct; eauto.
+Qed.
+
+Lemma transl_binop_correct:
+forall op a tya b tyb c ta va tb vb v le e m1 m2 m3,
+  transl_binop op a tya b tyb = Some 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.
+Proof.
+  intros. destruct op; simpl in *.
+  eapply make_add_correct; eauto.
+  eapply make_sub_correct; eauto.
+  eapply make_mul_correct; eauto.
+  eapply make_div_correct; eauto.
+  eapply make_mod_correct; eauto.
+  eapply make_and_correct; eauto.
+  eapply make_or_correct; eauto.
+  eapply make_xor_correct; eauto.
+  eapply make_shl_correct; eauto.
+  eapply make_shr_correct; eauto.
+  eapply make_cmp_correct; eauto.
+  eapply make_cmp_correct; eauto.
+  eapply make_cmp_correct; eauto.
+  eapply make_cmp_correct; eauto.
+  eapply make_cmp_correct; eauto.
+  eapply make_cmp_correct; eauto.
+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 ->
+   cast v ty1 ty2 v' ->
+   eval_expr tprog le e m1 (make_cast ty1 ty2 a) t m2 v'.
+Proof.
+  unfold make_cast, make_cast1, make_cast2, make_unop.
+  intros until v'; intros EVAL CAST.
+  inversion CAST; clear CAST; subst; auto.
+  (* cast_int_int *)
+    destruct sz2; destruct si2; repeat econstructor; eauto with cshm.
+  (* cast_float_int *)
+    destruct sz2; destruct si2; repeat econstructor; eauto with cshm; simpl; auto.
+  (* cast_int_float *)
+    destruct sz2; destruct si1; unfold make_floatofint, make_unop; repeat econstructor; eauto with cshm; simpl; auto.
+  (* cast_float_float *)
+    destruct sz2; repeat econstructor; eauto with cshm.
+Qed.
+
+Lemma make_load_correct:
+  forall addr ty code b ofs v le e m1 t m2,
+  make_load addr ty = Some 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.
+Proof.
+  unfold make_load, load_value_of_type.
+  intros until m2; intros MKLOAD EVEXP LDVAL.
+  destruct (access_mode ty); inversion MKLOAD.
+  (* access_mode ty = By_value m *)
+  apply eval_Eload with (Vptr b ofs); auto.
+  (* access_mode ty = By_reference *)
+  subst code. inversion LDVAL. auto.
+Qed.
+
+Lemma make_store_correct:
+  forall addr ty rhs code e m1 t1 m2 b ofs t2 m3 v m4,
+  make_store addr ty rhs = Some 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.
+Proof.
+  unfold make_store, store_value_of_type.
+  intros until m4; intros MKSTORE EV1 EV2 STVAL.
+  destruct (access_mode ty); inversion MKSTORE.
+  (* access_mode ty = By_value m *)
+  eapply eval_Sstore; eauto. 
+Qed.
+
+End CONSTRUCTORS.
+
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
new file mode 100644
index 0000000..b33771b
--- /dev/null
+++ b/cfrontend/Cshmgenproof3.v
@@ -0,0 +1,1503 @@
+(** * Correctness of the C front end, part 3: semantic preservation *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Integers.
+Require Import Floats.
+Require Import AST.
+Require Import Values.
+Require Import Events.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Csyntax.
+Require Import Csem.
+Require Import Ctyping.
+Require Import Csharpminor.
+Require Import Cshmgen.
+Require Import Cshmgenproof1.
+Require Import Cshmgenproof2.
+
+Section CORRECTNESS.
+
+Variable prog: Csyntax.program.
+Variable tprog: Csharpminor.program.
+Hypothesis WTPROG: wt_program prog.
+Hypothesis TRANSL: transl_program prog = Some tprog.
+
+Let ge := Csem.globalenv prog.
+Let tge := Genv.globalenv (Csharpminor.program_of_program tprog).
+
+Lemma symbols_preserved:
+  forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  intros. unfold ge, Csem.globalenv, tge. 
+  apply Genv.find_symbol_transf_partial with transl_fundef.
+  apply transform_program_of_program; auto.
+Qed.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = Some tf.
+Proof.
+  intros. 
+  generalize (Genv.find_funct_transf_partial transl_fundef (transform_program_of_program _ _ TRANSL) H).
+  intros [A B]. 
+  destruct (transl_fundef f). exists f0; split. assumption. auto. congruence.
+Qed.
+
+Lemma function_ptr_translated:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some f ->
+  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Some tf.
+Proof.
+  intros. 
+  generalize (Genv.find_funct_ptr_transf_partial transl_fundef (transform_program_of_program _ _ TRANSL) H).
+  intros [A B]. 
+  destruct (transl_fundef f). exists f0; split. assumption. auto. congruence.
+Qed.
+
+Lemma functions_well_typed:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  wt_fundef (global_typenv prog) f.
+Proof.
+  intros. inversion WTPROG. 
+  apply (@Genv.find_funct_prop _ (wt_fundef (global_typenv prog)) 
+                               (Csyntax.program_of_program prog) v f).
+  intros. apply wt_program_funct with id. assumption.
+  assumption.
+Qed.
+
+Lemma function_ptr_well_typed:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some f ->
+  wt_fundef (global_typenv prog) f.
+Proof.
+  intros. inversion WTPROG. 
+  apply (@Genv.find_funct_ptr_prop _ (wt_fundef (global_typenv prog)) 
+                               (Csyntax.program_of_program prog) b f).
+  intros. apply wt_program_funct with id. assumption.
+  assumption.
+Qed.
+
+(** ** Matching between environments *)
+
+Definition match_var_kind (ty: type) (vk: var_kind) : Prop :=
+  match access_mode ty with
+  | By_value chunk => vk = Vscalar chunk
+  | _ => True
+  end.
+
+Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop :=
+  mk_match_env {
+    me_local:
+      forall id b ty,
+      e!id = Some b -> tyenv!id = Some ty ->
+      exists vk, match_var_kind ty vk /\ te!id = Some (b, vk);
+    me_global:
+      forall id ty,
+      e!id = None -> tyenv!id = Some ty ->
+      te!id = None /\ 
+      (forall chunk, access_mode ty = By_value chunk -> (global_var_env tprog)!id = Some (Vscalar chunk))
+  }.
+
+Definition match_globalenv (tyenv: typenv) (gv: gvarenv): Prop :=
+  forall id ty chunk,
+  tyenv!id = Some ty -> access_mode ty = By_value chunk ->
+  gv!id = Some (Vscalar chunk).
+
+Lemma match_globalenv_match_env_empty:
+  forall tyenv,
+  match_globalenv tyenv (global_var_env tprog) ->
+  match_env tyenv Csem.empty_env Csharpminor.empty_env.
+Proof.
+  intros. unfold Csem.empty_env, Csharpminor.empty_env.
+  constructor.
+  intros until ty. repeat rewrite PTree.gempty. congruence.
+  intros. split.
+  apply PTree.gempty. 
+  intros. red in H. eauto.
+Qed.
+
+Lemma match_var_kind_of_type:
+  forall ty vk, var_kind_of_type ty = Some vk -> match_var_kind ty vk.
+Proof.
+  intros; red. 
+  caseEq (access_mode ty); auto.
+  intros chunk AM. generalize (var_kind_by_value _ _ AM). congruence.
+Qed.
+
+Lemma match_env_alloc_variables:
+  forall e1 m1 vars e2 m2 lb,
+  Csem.alloc_variables e1 m1 vars e2 m2 lb ->
+  forall tyenv te1 tvars,
+  match_env tyenv e1 te1 ->
+  transl_vars vars = Some tvars ->
+  exists te2,
+  Csharpminor.alloc_variables te1 m1 tvars te2 m2 lb
+  /\ match_env (Ctyping.add_vars tyenv vars) e2 te2.
+Proof.
+  induction 1; intros.
+  simpl in H0. inversion H0; subst; clear H0. 
+  exists te1; split. constructor. simpl. auto.
+  generalize H2. simpl. 
+  caseEq (var_kind_of_type ty); [intros vk VK | congruence].
+  caseEq (transl_vars vars); [intros tvrs TVARS | congruence].
+  intro EQ; inversion EQ; subst tvars; clear EQ.
+  set (te2 := PTree.set id (b1, vk) te1).
+  assert (match_env (add_var tyenv (id, ty)) (PTree.set id b1 e) te2).
+    inversion H1. unfold te2, add_var. constructor.
+    (* me_local *)
+    intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros.
+    subst id0. exists vk; split. 
+    apply match_var_kind_of_type. congruence. congruence.
+    auto.
+    (* me_global *)
+    intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros.
+    discriminate.
+    auto.
+  destruct (IHalloc_variables _ _ _ H3 TVARS) as [te3 [ALLOC MENV]]. 
+  exists te3; split.
+  econstructor; eauto.
+  rewrite (sizeof_var_kind_of_type _ _ VK). auto. 
+  auto. 
+Qed. 
+
+Lemma bind_parameters_match_rec:
+  forall e m1 vars vals m2,
+  Csem.bind_parameters e m1 vars vals m2 ->
+  forall tyenv te tvars,
+  (forall id ty, In (id, ty) vars -> tyenv!id = Some ty) ->
+  match_env tyenv e te ->
+  transl_params vars = Some tvars ->
+  Csharpminor.bind_parameters te m1 tvars vals m2.
+Proof.
+  induction 1; intros.
+  simpl in H1. inversion H1. constructor.
+  generalize H4; clear H4; simpl. 
+  caseEq (chunk_of_type ty); [intros chunk CHK | congruence].
+  caseEq (transl_params params); [intros tparams TPARAMS | congruence].
+  intro EQ; inversion EQ; clear EQ; subst tvars.
+  generalize CHK. unfold chunk_of_type. 
+  caseEq (access_mode ty); intros; try discriminate.
+  inversion CHK0; clear CHK0; subst m0.
+  unfold store_value_of_type in H0. rewrite H4 in H0.
+  apply bind_parameters_cons with b m1. 
+  assert (tyenv!id = Some ty). apply H2. apply in_eq.
+  destruct (me_local _ _ _ H3 _ _ _ H H5) as [vk [A B]]. 
+  red in A; rewrite H4 in A. congruence.
+  assumption.
+  apply IHbind_parameters with tyenv; auto.
+  intros. apply H2. apply in_cons; auto.
+Qed.
+
+Lemma tyenv_add_vars_norepet:
+  forall vars tyenv,
+  list_norepet (var_names vars) ->
+  (forall id ty,
+   In (id, ty) vars -> (Ctyping.add_vars tyenv vars)!id = Some ty)
+  /\
+  (forall id,
+   ~In id (var_names vars) -> (Ctyping.add_vars tyenv vars)!id = tyenv!id).
+Proof.
+  induction vars; simpl; intros.
+  tauto.
+  destruct a as [id1 ty1]. simpl in *. inversion H; clear H; subst.
+  destruct (IHvars (add_var tyenv (id1, ty1)) H3) as [A B].
+  split; intros.
+  destruct H. inversion H; subst id1 ty1; clear H. 
+  rewrite B. unfold add_var. simpl. apply PTree.gss. auto.
+  auto.
+  rewrite B. unfold add_var; simpl. apply PTree.gso. apply sym_not_equal; tauto. tauto.
+Qed.
+
+Lemma bind_parameters_match:
+  forall e m1 params vals vars m2 tyenv tvars te,
+  Csem.bind_parameters e m1 params vals m2 ->
+  list_norepet (var_names params ++ var_names vars) ->
+  match_env (Ctyping.add_vars tyenv (params ++ vars)) e te ->
+  transl_params params = Some tvars ->
+  Csharpminor.bind_parameters te m1 tvars vals m2.
+Proof.
+  intros. 
+  eapply bind_parameters_match_rec; eauto.
+  assert (list_norepet (var_names (params ++ vars))).
+    unfold var_names. rewrite List.map_app. assumption.
+  destruct (tyenv_add_vars_norepet _ tyenv H3) as [A B].
+  intros. apply A. apply List.in_or_app. auto. 
+Qed.
+
+Definition globvarenv 
+    (gv: gvarenv)
+    (vars: list (ident * var_kind * list init_data)) :=
+  List.fold_left
+    (fun gve x => match x with (id, k, init) => PTree.set id k gve end)
+    vars gv.
+
+Definition type_not_by_value (ty: type) : Prop :=
+  match access_mode ty with
+  | By_value _ => False
+  | _ => True
+  end.
+
+Lemma add_global_funs_charact:
+  forall fns tyenv,
+  (forall id ty, tyenv!id = Some ty -> type_not_by_value ty) ->
+  (forall id ty, (add_global_funs tyenv fns)!id = Some ty -> type_not_by_value ty).
+Proof.
+  induction fns; simpl; intros.
+  eauto.
+  apply IHfns with (add_global_fun tyenv a) id.
+  intros until ty0. destruct a as [id1 fn1]. 
+  unfold add_global_fun; simpl. rewrite PTree.gsspec.
+  destruct (peq id0 id1). 
+  intros. inversion H1. 
+  unfold type_of_fundef. destruct fn1; exact I.
+  eauto.
+  auto.
+Qed.
+
+Definition global_fun_typenv :=
+  add_global_funs (PTree.empty type) (Csyntax.prog_funct prog).
+
+Lemma add_global_funs_match_global_env:
+  match_globalenv global_fun_typenv (PTree.empty var_kind).
+Proof.
+  intros; red; intros.
+  assert (type_not_by_value ty).
+    apply add_global_funs_charact with (Csyntax.prog_funct prog) (PTree.empty type) id.
+    intros until ty0. rewrite PTree.gempty. congruence.
+    assumption.
+  red in H1. rewrite H0 in H1. contradiction.
+Qed.
+
+Lemma add_global_var_match_globalenv:
+  forall vars tenv gv tvars,
+  match_globalenv tenv gv ->
+  transl_global_vars vars = Some tvars ->
+  match_globalenv (add_global_vars tenv vars) (globvarenv gv tvars).
+Proof.
+  induction vars; intros; simpl.
+  simpl in H0. inversion H0. simpl. auto.
+  destruct a as [[id ty] init]. monadInv H0. subst tvars.
+  simpl. apply IHvars; auto.
+  red. intros until chunk. repeat rewrite PTree.gsspec. 
+  destruct (peq id0 id); intros.
+  inversion H1; clear H1; subst id0 ty0. 
+  generalize (var_kind_by_value _ _ H2). congruence.
+  red in H. eauto. 
+Qed.
+
+Lemma match_global_typenv:
+  match_globalenv (global_typenv prog) (global_var_env tprog).
+Proof.
+  change (global_var_env tprog)
+    with (globvarenv (PTree.empty var_kind) (prog_vars tprog)).
+  unfold global_typenv.
+  apply add_global_var_match_globalenv.
+  apply add_global_funs_match_global_env. 
+  monadInv TRANSL. rewrite <- H0. reflexivity.
+Qed.
+
+(** ** Variable accessors *)
+
+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 ->
+  load_value_of_type ty m loc ofs = Some v ->
+  wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
+  var_get id ty = Some code ->
+  match_env tyenv e te ->
+  eval_expr tprog le te m code E0 m v.
+Proof.
+  intros. inversion H1; subst; clear H1. 
+  unfold load_value_of_type in H0.
+  unfold var_get in H2. 
+  caseEq (access_mode ty).
+  (* 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.
+    (* local variable *)
+    exploit me_local; eauto. intros [vk [A B]].
+    red in A; rewrite ACC in A.
+    subst vk.
+    eapply eval_Evar. 
+    eapply eval_var_ref_local. eauto. assumption. 
+    (* global variable *)
+    exploit me_global; eauto. intros [A B].
+    eapply eval_Evar. 
+    eapply eval_var_ref_global. auto. 
+    fold tge. rewrite symbols_preserved. eauto.
+    eauto. assumption. 
+  (* access mode By_reference *)
+  intros ACC. rewrite ACC in H0. rewrite ACC in H2.
+  inversion H0; clear H0; subst.
+  inversion H2; clear H2; subst.
+  inversion H; subst; clear H.
+    (* local variable *)
+    exploit me_local; eauto. intros [vk [A B]].
+    eapply eval_Eaddrof.
+    eapply eval_var_addr_local. eauto. 
+    (* global variable *)
+    exploit me_global; eauto. intros [A B].
+    eapply eval_Eaddrof.
+    eapply eval_var_addr_global. auto. 
+    fold tge. rewrite symbols_preserved. eauto.
+  (* access mode By_nothing *)
+  intros. rewrite H1 in H0; discriminate.
+Qed.
+
+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 ->
+  wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
+  var_set id ty rhs = Some 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.
+Proof.
+  intros. inversion H1; subst; clear H1. 
+  unfold store_value_of_type in H0.
+  unfold var_set in H2. 
+  caseEq (access_mode ty).
+  (* 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.
+    (* 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. 
+    (* global variable *)
+    exploit me_global; eauto. intros [A B].
+    eapply eval_Sassign. eauto.
+    eapply eval_var_ref_global. auto. 
+    fold tge. rewrite symbols_preserved. eauto.
+    eauto. assumption. 
+  (* access mode By_reference *)
+  intros ACC. rewrite ACC in H0. discriminate.
+  (* access mode By_nothing *)
+  intros. rewrite H1 in H0; discriminate.
+Qed.
+
+(** ** Proof of semantic simulation *)
+
+(** Inductive properties *)
+
+Definition eval_expr_prop 
+    (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) (m2: mem) (v: val) : Prop :=
+  forall tyenv ta te tle
+    (WT: wt_expr tyenv a)
+    (TR: transl_expr a = Some ta)
+    (MENV: match_env tyenv e te),
+  Csharpminor.eval_expr tprog tle te m1 ta t m2 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
+    (WT: wt_expr tyenv a)
+    (TR: transl_lvalue a = Some ta)
+    (MENV: match_env tyenv e te),
+  Csharpminor.eval_expr tprog tle te m1 ta t m2 (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
+    (WT: wt_exprlist tyenv al)
+    (TR: transl_exprlist al = Some 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 = Some 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 = Some 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 = Some tf),
+   Csharpminor.eval_funcall tprog m1 tf params t m2 res.
+
+(*
+Set Printing Depth 100.
+Check (Csem.eval_funcall_ind6 ge eval_expr_prop eval_lvalue_prop
+         eval_exprlist_prop exec_stmt_prop exec_lblstmts_prop eval_funcall_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)).
+Proof.
+  intros; red; intros.
+  monadInv TR. subst ta. 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)).
+Proof.
+  intros; red; intros.
+  monadInv TR. subst ta. 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).
+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.
+  (* 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)).
+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')))).
+Proof.
+  intros; red; intros. monadInv TR. subst ta. apply make_intconst_correct. 
+Qed.
+
+Lemma transl_Eunop_correct:
+       (forall (e : Csem.env) (m : mem) (op : 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 (Eunop op a) ty) t m1 v).
+Proof.
+  intros; red; intros.
+  inversion WT; clear WT; subst.
+  monadInv TR. 
+  eapply transl_unop_correct; eauto. 
+Qed.
+
+Lemma transl_Ebinop_correct:
+       (forall (e : Csem.env) (m : mem) (op : 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 (Ebinop op a1 a2) ty) (t1 ** t2) m2 v).
+Proof.
+  intros; red; intros.
+  inversion WT; clear WT; subst.
+  monadInv TR. 
+  eapply transl_binop_correct; eauto. 
+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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
+  rewrite <- H3; 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.
+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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
+  rewrite <- H6; unfold make_orbool.
+  exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]].
+  eapply eval_Econdition_false; eauto.
+  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.
+  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.
+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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
+  rewrite <- H3; 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.
+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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
+  rewrite <- H6; unfold make_andbool.
+  exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]].
+  eapply eval_Econdition_true; eauto.
+  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.
+  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.
+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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta.
+  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. clear TR. subst ta.
+  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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta.
+  exploit (me_local _ _ _ MENV); eauto. intros [vk [A B]].
+  econstructor. eapply eval_var_addr_local. eauto. 
+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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta.
+  exploit (me_global _ _ _ MENV); eauto. intros [A B].
+  econstructor. eapply eval_var_addr_global. eauto. 
+  rewrite symbols_preserved. auto.
+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).
+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).
+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) (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 fList ->
+        field_offset i fList = Some delta ->
+        eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 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.
+  rewrite <- H5. eapply make_binop_correct; eauto.
+  apply make_intconst_correct. 
+  simpl. congruence. traceEq.
+Qed.
+
+Lemma transl_Efield_union_correct:
+       (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace)
+          (m1 : mem) (l : block) (ofs : int) (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 fList ->
+        eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 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. subst tal. constructor.
+Qed.
+
+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)).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. 
+  subst tal. econstructor; eauto. 
+Qed.
+
+Lemma transl_Sskip_correct:
+       (forall (e : Csem.env) (m : mem),
+        exec_stmt_prop e m Csyntax.Sskip E0 m Csem.Out_normal).
+Proof.
+  intros; red; intros. monadInv TR. subst ts. 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. subst ts. 
+  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).
+Proof.
+  intros; red; intros.
+  inversion WT; subst; clear WT.
+  simpl in TR. 
+  caseEq (is_variable a1).
+  (* 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.
+  monadInv TR.
+  eapply var_set_correct; eauto. 
+  (* a is not a variable *)
+  intro ISVAR; rewrite ISVAR in TR. monadInv TR.
+  eapply make_store_correct; eauto.
+Qed.
+
+Lemma transl_Ssequence_1_correct:
+       (forall (e : Csem.env) (m : mem) (s1 s2 : statement) (t1 : trace)
+          (m1 : mem) (t2 : trace) (m2 : mem) (out : Csem.outcome),
+        Csem.exec_stmt ge e m s1 t1 m1 Csem.Out_normal ->
+        exec_stmt_prop e m s1 t1 m1 Csem.Out_normal ->
+        Csem.exec_stmt ge e m1 s2 t2 m2 out ->
+        exec_stmt_prop e m1 s2 t2 m2 out ->
+        exec_stmt_prop e m (Ssequence s1 s2) (t1 ** t2) m2 out).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. red in H0; simpl in H0. eapply exec_Sseq_continue; eauto. 
+Qed.
+
+Lemma transl_Ssequence_2_correct:
+       (forall (e : Csem.env) (m : mem) (s1 s2 : statement) (t1 : trace)
+          (m1 : mem) (out : Csem.outcome),
+        Csem.exec_stmt ge e m s1 t1 m1 out ->
+        exec_stmt_prop e m s1 t1 m1 out ->
+        out <> Csem.Out_normal ->
+        exec_stmt_prop e m (Ssequence s1 s2) t1 m1 out).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. eapply exec_Sseq_stop; eauto. 
+  destruct out; simpl; congruence.
+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 ->
+        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).
+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]].
+  subst ts. eapply exec_Sifthenelse_true; 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 ->
+        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).
+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]].
+  subst ts. eapply exec_Sifthenelse_false; eauto. 
+Qed.
+
+Lemma transl_Sreturn_none_correct:
+       (forall (e : Csem.env) (m : mem),
+        exec_stmt_prop e m (Csyntax.Sreturn None) E0 m (Csem.Out_return None)).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. simpl. apply exec_Sreturn_none. 
+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))).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. simpl. eapply exec_Sreturn_some; eauto. 
+Qed.
+
+Lemma transl_Sbreak_correct:
+       (forall (e : Csem.env) (m : mem),
+        exec_stmt_prop e m Sbreak E0 m Out_break).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. simpl. apply exec_Sexit.  
+Qed.
+
+Lemma transl_Scontinue_correct:
+       (forall (e : Csem.env) (m : mem),
+        exec_stmt_prop e m Scontinue E0 m Out_continue).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. simpl. apply exec_Sexit.  
+Qed.
+
+Lemma exit_if_false_true:
+  forall a ts e m1 t m2 v tyenv te,
+  exit_if_false a = Some ts ->
+  eval_expr_prop e m1 a t m2 v ->
+  match_env tyenv e te ->
+  wt_expr tyenv a ->
+  is_true v (typeof a) ->
+  exec_stmt tprog te m1 ts t m2 Out_normal.
+Proof.
+  intros. monadInv H. rewrite <- H5. 
+  eapply exec_Sifthenelse_false with (v1 := Vfalse).
+  eapply make_notbool_correct with (va := v); eauto.
+  inversion H3; subst; simpl; auto.
+  rewrite Int.eq_false; auto.
+  rewrite Int.eq_false; auto.
+  rewrite Float.eq_zero_false; auto.
+  simpl; auto.
+  constructor. traceEq.
+Qed.
+ 
+Lemma exit_if_false_false:
+  forall a ts e m1 t m2 v tyenv te,
+  exit_if_false a = Some ts ->
+  eval_expr_prop e m1 a t m2 v ->
+  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).
+Proof.
+  intros. monadInv H. rewrite <- H5. 
+  eapply exec_Sifthenelse_true with (v1 := Vtrue).
+  eapply make_notbool_correct with (va := v); eauto.
+  inversion H3; subst; simpl; auto.
+  rewrite Float.eq_zero_true; auto.
+  simpl; apply Int.one_not_zero.
+  constructor. traceEq.
+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 ->
+        is_false v (typeof a) ->
+        exec_stmt_prop e m (Swhile a s) t m1 Csem.Out_normal).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. simpl.
+  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.
+Qed.
+
+Lemma transl_out_break_or_return:
+  forall out1 out2 nbrk ncnt,
+  out_break_or_return out1 out2 ->
+  transl_outcome nbrk ncnt out2 =
+  outcome_block (outcome_block (transl_outcome 1 0 out1)).
+Proof.
+  intros. inversion H; subst; reflexivity.
+Qed.
+
+Lemma transl_out_normal_or_continue:
+  forall out,
+  out_normal_or_continue out ->
+  Out_normal = outcome_block (transl_outcome 1 0 out).
+Proof.
+  intros; inversion H; reflexivity.
+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 ->
+        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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. rewrite (transl_out_break_or_return _ _ nbrk ncnt H4).
+  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.
+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 ->
+        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).
+Proof.
+  intros; red; intros. 
+  exploit H6; eauto. intro NEXTITER.
+  inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. 
+  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).
+  apply exec_Sblock. eauto. 
+  reflexivity. eassumption.
+  traceEq.
+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 ->
+        out_normal_or_continue out1 ->
+        Csem.eval_expr ge e m1 a t2 m2 v ->
+        eval_expr_prop e m1 a t2 m2 v ->
+        is_false v (typeof a) ->
+        exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 Csem.Out_normal).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. 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. 
+Qed.
+
+Lemma transl_Sdowhile_stop_correct:
+       (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr)
+          (t : trace) (m1 : mem) (out1 out : Csem.outcome),
+        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 (Sdowhile a s) t m1 out).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. simpl.
+  assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal).
+    inversion H1; simpl; congruence.
+  rewrite (transl_out_break_or_return _ _ nbrk ncnt H1). 
+  apply exec_Sblock. apply exec_Sloop_stop. 
+  apply exec_Sseq_stop. apply exec_Sblock. eauto. 
+  auto. auto. 
+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),
+        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 ->
+        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).
+Proof.
+  intros; red; intros. 
+  exploit H6; eauto. intro NEXTITER.
+  inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. 
+  inversion NEXTITER; subst.
+  apply exec_Sblock. 
+  eapply exec_Sloop_loop. eapply exec_Sseq_continue.
+  rewrite (transl_out_normal_or_continue _ H1).
+  apply exec_Sblock. eauto. 
+  eapply exit_if_false_true; eauto. 
+  reflexivity. eassumption. traceEq.
+Qed.
+
+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),
+        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 ->
+        exec_stmt_prop e m1 (Sfor Csyntax.Sskip a2 a3 s) t2 m2 out ->
+        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.
+  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. 
+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 ->
+        is_false v (typeof a2) ->
+        exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) t m1 Csem.Out_normal).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. 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. 
+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 ->
+        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).
+Proof.
+  intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. 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.
+  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. 
+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 ->
+        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).
+Proof.
+  intros; red; intros. 
+  exploit H8; eauto. intro NEXTITER.
+  inversion WT; clear WT; subst. simpl in TR; monadInv TR.
+  subst ts. 
+  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).
+  apply exec_Sblock. eauto. 
+  red in H6; simpl in H6; eauto.
+  reflexivity. reflexivity. eassumption. 
+  reflexivity. traceEq. 
+  inversion H17. congruence.
+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 
+    (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0))) ->
+  transl_lblstmts 
+    (lblstmts_length sl)
+    (S (lblstmts_length sl + ncnt))
+    sl (Sblock body) = Some 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 
+    (transl_outcome nbrk ncnt (outcome_switch out)).
+Proof.
+  induction sl; intros.
+  simpl in H. simpl in H3.
+  eapply H3; eauto. 
+  change Out_normal with (outcome_block (Out_exit 0)).
+  apply exec_Sblock. auto.
+  (* Inductive case *)
+  simpl in H. simpl in H3. rewrite Int.eq_sym in H3. destruct (Int.eq n i).
+  (* first case selected *)
+  eapply H3; eauto. 
+  change Out_normal with (outcome_block (Out_exit 0)).
+  apply exec_Sblock. auto.
+  (* next case selected *)
+  inversion H1; clear H1; subst.
+  simpl in H0; monadInv H0.
+  eapply IHsl with (body := Sseq (Sblock body) s0); eauto.
+  apply exec_Sseq_stop. 
+  change (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0)))
+    with (outcome_block (Out_exit (S (switch_target n (lblstmts_length sl) (switch_table sl 0))))).
+  apply exec_Sblock. 
+  rewrite switch_target_table_shift in H. auto. congruence.
+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)).
+Proof.
+  intros; red; intros.
+  inversion WT; clear WT; subst.
+  simpl in TR. monadInv TR; clear 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. 
+Qed.
+
+Lemma transl_LSdefault_correct:
+       (forall (e : Csem.env) (m : mem) (s : statement) (t : trace)
+          (m1 : mem) (out : Csem.outcome),
+        Csem.exec_stmt ge e m s t m1 out ->
+        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.
+  rewrite <- H3. 
+  replace (transl_outcome nbrk ncnt (outcome_switch out))
+     with (outcome_block (transl_outcome 0 (S ncnt) out)).
+  constructor. 
+  eapply exec_Sseq_continue. eauto. 
+  eapply H0; eauto. traceEq.
+  destruct out; simpl; auto.
+Qed.
+
+Lemma transl_LScase_fallthrough_correct:
+       (forall (e : Csem.env) (m : mem) (n : int) (s : statement)
+          (ls : labeled_statements) (t1 : trace) (m1 : mem) (t2 : trace)
+          (m2 : mem) (out : Csem.outcome),
+        Csem.exec_stmt ge e m s t1 m1 Csem.Out_normal ->
+        exec_stmt_prop e m s t1 m1 Csem.Out_normal ->
+        exec_lblstmts ge e m1 ls t2 m2 out ->
+        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.
+  simpl in TR. monadInv TR; clear TR.
+  assert (exec_stmt tprog te m0 (Sblock (Sseq body s0)) 
+                  (t0 ** t1) m1 Out_normal).
+  change Out_normal with
+    (outcome_block (transl_outcome (S (lblstmts_length ls))
+                                   (S (S (lblstmts_length ls + ncnt)))
+                                   Csem.Out_normal)).
+  apply exec_Sblock. eapply exec_Sseq_continue. eexact BODY. 
+  eapply H0; eauto.
+  auto.
+  exploit H2. eauto. simpl; eauto. eauto. eauto. simpl. 
+  rewrite Eapp_assoc. eauto.
+Qed.
+
+Lemma transl_LScase_stop_correct:
+       (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 ->
+        exec_stmt_prop e m s t m1 out ->
+        out <> Csem.Out_normal ->
+        exec_lblstmts_prop e m (LScase n s ls) t m1 out).
+Proof.
+  intros; red; intros.
+  inversion WT; subst.
+  simpl in TR. monadInv TR; clear TR.
+  exploit H0; eauto. intro EXEC.
+  destruct out; simpl; simpl in EXEC.
+  (* out = Out_break *)
+  change Out_normal with (outcome_block (Out_exit 0)).
+  eapply transl_lblstmts_exit with (body := Sblock (Sseq body s0)); eauto.
+  rewrite plus_0_r. 
+  change (Out_exit (lblstmts_length ls))
+    with (outcome_block (Out_exit (S (lblstmts_length ls)))).
+  constructor. eapply exec_Sseq_continue; eauto.
+  (* out = Out_continue *)
+  change (Out_exit ncnt) with (outcome_block (Out_exit (S ncnt))).
+  eapply transl_lblstmts_exit with (body := Sblock (Sseq body s0)); eauto.
+  replace (Out_exit (lblstmts_length ls + S ncnt))
+    with (outcome_block (Out_exit (S (S (lblstmts_length ls + ncnt))))).
+  constructor. eapply exec_Sseq_continue; eauto.
+  simpl. decEq. omega. 
+  (* out = Out_normal *)
+  congruence.
+  (* out = Out_return *)
+  eapply transl_lblstmts_return with (body := Sblock (Sseq body s0)); eauto.
+  change (Out_return o)
+    with (outcome_block (Out_return o)).
+  constructor. eapply exec_Sseq_continue; eauto.
+Qed.
+
+Remark outcome_result_value_match:
+  forall out ty v nbrk ncnt,
+  Csem.outcome_result_value out ty v ->
+  Csharpminor.outcome_result_value (transl_outcome nbrk ncnt out) (opttyp_of_type ty) v.
+Proof.
+  intros until ncnt.
+  destruct out; simpl; try contradiction.
+  destruct ty; simpl; auto.
+  destruct o. intros [A B]. destruct ty; simpl; congruence.
+  destruct ty; simpl; auto.
+Qed.
+
+Lemma transl_funcall_internal_correct:
+       (forall (m : mem) (f : Csyntax.function) (vargs : list val)
+          (t : trace) (e : Csem.env) (m1 : mem) (lb : list block)
+          (m2 m3 : mem) (out : Csem.outcome) (vres : val),
+        Csem.alloc_variables Csem.empty_env m
+          (Csyntax.fn_params f ++ Csyntax.fn_vars f) e m1 lb ->
+        Csem.bind_parameters e m1 (Csyntax.fn_params f) vargs m2 ->
+        Csem.exec_stmt ge e m2 (Csyntax.fn_body f) t m3 out ->
+        exec_stmt_prop e m2 (Csyntax.fn_body f) t m3 out ->
+        Csem.outcome_result_value out (fn_return f) vres ->
+        eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres).
+Proof.
+  intros; red; intros.
+  (* Exploitation of typing hypothesis *)
+  inversion WT; clear WT; subst. 
+  inversion H6; clear H6; subst.
+  (* Exploitation of translation hypothesis *)
+  monadInv TR. subst tf. clear TR. 
+  monadInv EQ. clear EQ. subst f0.
+  (* Allocation of variables *)
+  exploit match_env_alloc_variables; eauto.
+  apply match_globalenv_match_env_empty. 
+  apply match_global_typenv.
+  eexact (transl_fn_variables _ _ (signature_of_function f) _ _ s EQ0 EQ1).
+  intros [te [ALLOCVARS MATCHENV]].
+  (* Execution *)
+  econstructor; simpl.
+    (* Norepet *)
+    eapply transl_names_norepet; eauto. 
+    (* Alloc *)
+    eexact ALLOCVARS.
+    (* Bind *)
+    eapply bind_parameters_match; eauto.
+    (* Execution of body *)
+    eapply H2; eauto.
+    (* Outcome_result_value *)
+    apply outcome_result_value_match; auto.
+Qed.
+
+Lemma transl_funcall_external_correct:
+       (forall (m : mem) (id : ident) (targs : typelist) (tres : type)
+          (vargs : list val) (t : trace) (vres : val),
+        event_match (external_function id targs tres) vargs t vres ->
+        eval_funcall_prop m (External id targs tres) vargs t m vres).
+Proof.
+  intros; red; intros.
+  monadInv TR. subst tf. constructor. auto.
+Qed.
+
+Theorem transl_funcall_correct:
+  forall (m : mem) (f : Csyntax.fundef) (l : list val) (t : trace)
+         (m0 : mem) (v : val),
+  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
+         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_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).
+
+End CORRECTNESS.
+
+(** Semantic preservation for whole programs. *)
+
+Theorem transl_program_correct:
+  forall prog tprog t r,
+  transl_program prog = Some tprog ->
+  Ctyping.wt_program prog ->
+  Csem.exec_program prog t r ->
+  Csharpminor.exec_program tprog t r.
+Proof.
+  intros until r. intros TRANSL WT [b [f [m1 [FINDS [FINDF [TYP EVAL]]]]]].
+  inversion WT; subst.
+  
+  assert (type_of_fundef f = Tfunction Tnil (Tint I32 Signed)).
+    apply wt_program_main.
+    change (Csyntax.prog_funct prog)
+      with (AST.prog_funct (Csyntax.program_of_program prog)).
+    eapply Genv.find_funct_ptr_symbol_inversion; eauto. 
+  exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]].
+  exists b; exists tf; exists m1.
+  split. 
+    rewrite (symbols_preserved _ _ TRANSL).
+    monadInv TRANSL. rewrite <- H1. simpl. auto.
+  split. auto.
+  split. 
+    generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD H). simpl; auto.
+  rewrite (@Genv.init_mem_transf_partial _ _ transl_fundef 
+             (Csyntax.program_of_program prog)
+             (Csharpminor.program_of_program tprog)).
+  generalize (transl_funcall_correct _ _ WT TRANSL _ _ _ _ _ _ EVAL).
+  intro. eapply H0. 
+  eapply function_ptr_well_typed; eauto.
+  auto.
+  apply transform_program_of_program; auto.
+Qed.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
new file mode 100644
index 0000000..d3bd8d6
--- /dev/null
+++ b/cfrontend/Csyntax.v
@@ -0,0 +1,456 @@
+(** * Abstract syntax for the Clight language *)
+
+Require Import Coqlib.
+Require Import Integers.
+Require Import Floats.
+Require Import AST.
+
+(** ** Abstract syntax *)
+
+(** Types *)
+
+Inductive signedness : Set :=
+  | Signed: signedness
+  | Unsigned: signedness.
+
+Inductive intsize : Set :=
+  | I8: intsize
+  | I16: intsize
+  | I32: intsize.
+
+Inductive floatsize : Set :=
+  | F32: floatsize
+  | F64: floatsize.
+
+Inductive type : Set :=
+  | Tvoid: type
+  | Tint: intsize -> signedness -> type
+  | Tfloat: floatsize -> type
+  | Tpointer: type -> type
+  | Tarray: type -> Z -> type
+  | Tfunction: typelist -> type -> type
+  | Tstruct: fieldlist -> type
+  | Tunion: fieldlist -> type
+
+with typelist : Set :=
+  | Tnil: typelist
+  | Tcons: type -> typelist -> typelist
+
+with fieldlist : Set :=
+  | Fnil: fieldlist
+  | Fcons: ident -> type -> fieldlist -> fieldlist.
+
+(** Arithmetic and logical operators *)
+
+Inductive unary_operation : Set :=
+  | Onotbool : unary_operation
+  | Onotint : unary_operation
+  | Oneg : unary_operation.
+
+Inductive binary_operation : Set :=
+  | Oadd : binary_operation
+  | Osub : binary_operation
+  | Omul : binary_operation
+  | Odiv : binary_operation
+  | Omod : binary_operation
+  | Oand : binary_operation
+  | Oor : binary_operation
+  | Oxor : binary_operation
+  | Oshl : binary_operation
+  | Oshr : binary_operation
+  | Oeq: binary_operation
+  | One: binary_operation
+  | Olt: binary_operation
+  | Ogt: binary_operation
+  | Ole: binary_operation
+  | Oge: binary_operation.
+
+(** Expressions *)
+
+Inductive expr : Set :=
+  | Expr: expr_descr -> type -> expr
+
+with expr_descr : Set :=
+  | Econst_int: int -> expr_descr
+  | Econst_float: float -> expr_descr
+  | Evar: ident -> expr_descr
+  | Ederef: expr -> expr_descr
+  | Eaddrof: expr -> expr_descr
+  | Eunop: unary_operation -> expr -> expr_descr
+  | Ebinop: binary_operation -> expr -> expr -> expr_descr
+  | Ecast: type -> expr -> expr_descr
+  | Eindex: expr -> expr -> expr_descr 
+  | Ecall: expr -> exprlist -> expr_descr 
+  | Eandbool: expr -> expr -> expr_descr
+  | Eorbool: expr -> expr -> expr_descr
+  | Esizeof: type -> expr_descr
+  | Efield: expr -> ident -> expr_descr
+
+with exprlist : Set :=
+  | Enil: exprlist
+  | Econs: expr -> exprlist -> exprlist.
+
+(** Extract the type part of a type-annotated Clight expression. *)
+
+Definition typeof (e: expr) : type :=
+  match e with Expr de te => te end.
+
+(** Statements *)
+
+Inductive statement : Set :=
+  | Sskip : statement
+  | Sexpr : expr -> statement
+  | Sassign : expr -> expr -> statement
+  | Ssequence : statement -> statement -> statement
+  | Sifthenelse : expr  -> statement -> statement -> statement
+  | Swhile : expr -> statement -> statement
+  | Sdowhile : expr -> statement -> statement
+  | Sfor: statement -> expr -> statement -> statement -> statement
+  | Sbreak : statement
+  | Scontinue : statement
+  | Sreturn : option expr -> statement
+  | Sswitch : expr -> labeled_statements -> statement
+
+with labeled_statements : Set :=
+  | LSdefault: statement -> labeled_statements
+  | LScase: int -> statement -> labeled_statements -> labeled_statements.
+
+(** Function definition *)
+
+Record function : Set := mkfunction {
+  fn_return: type;
+  fn_params: list (ident * type);
+  fn_vars: list (ident * type);
+  fn_body: statement
+}.
+
+Inductive fundef : Set :=
+  | Internal: function -> fundef
+  | External: ident -> typelist -> type -> fundef.
+
+(** Program *)
+
+Record program : Set := mkprogram {
+    prog_funct: list (ident * fundef);
+    prog_defs: list (ident * type * list init_data);
+    prog_main: ident
+}.
+
+(** ** Operations over types *)
+
+(** The type of a function definition *)
+
+Fixpoint type_of_params (params: list (ident * type)) : typelist :=
+  match params with
+  | nil => Tnil
+  | (id, ty) :: rem => Tcons ty (type_of_params rem)
+  end.
+
+Definition type_of_function (f: function) : type :=
+  Tfunction (type_of_params (fn_params f)) (fn_return f).
+
+Definition type_of_fundef (f: fundef) : type :=
+  match f with
+  | Internal fd => type_of_function fd
+  | External id args res => Tfunction args res
+  end.
+
+(** Natural alignment of a type *)
+
+Fixpoint alignof (t: type) : Z :=
+  match t with
+  | Tvoid => 1
+  | Tint I8 _ => 1
+  | Tint I16 _ => 2
+  | Tint I32 _ => 4
+  | Tfloat F32 => 4
+  | Tfloat F64 => 8
+  | Tpointer _ => 4
+  | Tarray t' n => alignof t'
+  | Tfunction _ _ => 1
+  | Tstruct fld => alignof_fields fld
+  | Tunion fld => alignof_fields fld
+  end
+
+with alignof_fields (f: fieldlist) : Z :=
+  match f with
+  | Fnil => 1
+  | Fcons id t f' => Zmax (alignof t) (alignof_fields f')
+  end.
+
+Scheme type_ind2 := Induction for type Sort Prop
+  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
+
+Lemma alignof_fields_pos:
+  forall f, alignof_fields f > 0.
+Proof.
+  induction f; simpl.
+  omega.
+  generalize (Zmax2 (alignof t) (alignof_fields f)). omega.
+Qed.
+
+Lemma alignof_pos:
+  forall t, alignof t > 0.
+Proof.
+  induction t; simpl; auto; try omega.
+  destruct i; omega.
+  destruct f; omega.
+  apply alignof_fields_pos.
+  apply alignof_fields_pos.
+Qed.
+
+(** Size of a type (in bytes) *)
+
+Fixpoint sizeof (t: type) : Z :=
+  match t with
+  | Tvoid => 1
+  | Tint I8 _ => 1
+  | Tint I16 _ => 2
+  | Tint I32 _ => 4
+  | Tfloat F32 => 4
+  | Tfloat F64 => 8
+  | Tpointer _ => 4
+  | Tarray t' n => sizeof t' * Zmax 1 n
+  | Tfunction _ _ => 1
+  | Tstruct fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
+  | Tunion fld => align (Zmax 1 (sizeof_union fld)) (alignof t)
+  end
+
+with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
+  match fld with
+  | Fnil => pos
+  | Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t)
+  end
+
+with sizeof_union (fld: fieldlist) : Z :=
+  match fld with
+  | Fnil => 0
+  | Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld')
+  end.
+
+Lemma sizeof_pos:
+  forall t, sizeof t > 0.
+Proof.
+  intro t0.
+  apply (type_ind2 (fun t => sizeof t > 0)
+                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
+  intros; simpl; auto; try omega.
+  destruct i; omega.
+  destruct f; omega.
+  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
+  destruct H. 
+  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). 
+  generalize (Zmax1 1 (sizeof_struct f 0)). omega. 
+  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). 
+  generalize (Zmax1 1 (sizeof_union f)). omega. 
+  split. omega. auto.
+  destruct H0. split; intros.
+  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
+  apply H1. 
+  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
+Qed.
+
+(** Byte offset for a field in a struct. *)
+
+Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
+                              {struct fld} : option Z :=
+  match fld with
+  | Fnil => None
+  | Fcons id' t fld' =>
+      if ident_eq id id'
+      then Some (align pos (alignof t))
+      else field_offset_rec id fld' (align pos (alignof t) + sizeof t)
+  end.
+
+Definition field_offset (id: ident) (fld: fieldlist) : option Z :=
+  field_offset_rec id fld 0.
+
+(* Describe how a variable of the given type must be accessed:
+     - by value, i.e. by loading from the address of the variable
+       with the given chunk
+     - by reference, i.e. by just returning the address of the variable
+     - not at all, e.g. the [void] type. *)
+
+Inductive mode: Set :=
+  | By_value: memory_chunk -> mode
+  | By_reference: mode
+  | By_nothing: mode.
+
+Definition access_mode (ty: type) : mode :=
+  match ty with
+  | Tint I8 Signed => By_value Mint8signed
+  | Tint I8 Unsigned => By_value Mint8unsigned
+  | Tint I16 Signed => By_value Mint16signed
+  | Tint I16 Unsigned => By_value Mint16unsigned
+  | Tint I32 _ => By_value Mint32
+  | Tfloat F32 => By_value Mfloat32
+  | Tfloat F64 => By_value Mfloat64
+  | Tvoid => By_nothing
+  | Tpointer _ => By_value Mint32
+  | Tarray _ _ => By_reference
+  | Tfunction _ _ => By_reference
+  | Tstruct fList => By_nothing
+  | Tunion fList => By_nothing
+end.
+
+(** Conversion of a Clight program into an AST program *)
+
+Definition extract_global_var (id_ty_init: ident * type * list init_data) :=
+  match id_ty_init with (id, ty, init) => (id, init) end.
+
+Definition program_of_program (p: program) : AST.program fundef :=
+  AST.mkprogram
+    p.(prog_funct)
+    p.(prog_main)
+    (List.map extract_global_var p.(prog_defs)).
+
+(** Classification of arithmetic operations and comparisons *)
+
+Inductive classify_add_cases : Set :=
+  | add_case_ii: classify_add_cases         (* int , int *)
+  | add_case_ff: classify_add_cases         (* float , float *)
+  | add_case_pi: type -> classify_add_cases (* ptr | array, int *)
+  | add_default: classify_add_cases.        (* other *)
+
+Definition classify_add (ty1: type) (ty2: type) :=
+  match ty1, ty2 with
+  | Tint _ _, Tint _ _ => add_case_ii
+  | Tfloat _, Tfloat _ => add_case_ff
+  | Tpointer ty, Tint _ _ => add_case_pi ty
+  | Tarray ty _, Tint _ _ => add_case_pi ty 
+  | _, _ => add_default
+  end.
+
+Inductive classify_sub_cases : Set :=
+  | sub_case_ii: classify_sub_cases          (* int , int *)
+  | sub_case_ff: classify_sub_cases          (* float , float *)
+  | sub_case_pi: type -> classify_sub_cases  (* ptr | array , int *)
+  | sub_case_pp: type -> classify_sub_cases  (* ptr | array , ptr | array *)
+  | sub_default: classify_sub_cases .        (* other *)
+
+Definition classify_sub (ty1: type) (ty2: type) :=
+  match ty1, ty2 with
+  | Tint _ _ , Tint _ _ => sub_case_ii
+  | Tfloat _ , Tfloat _ => sub_case_ff
+  | Tpointer ty , Tint _ _ => sub_case_pi ty
+  | Tarray ty _ , Tint _ _ => sub_case_pi ty
+  | Tpointer ty , Tpointer _ => sub_case_pp ty
+  | Tpointer ty , Tarray _ _=> sub_case_pp ty
+  | Tarray ty _ , Tpointer _ => sub_case_pp ty
+  | Tarray ty _ , Tarray _ _ => sub_case_pp ty 
+  | _ ,_ => sub_default
+  end.
+
+Inductive classify_mul_cases : Set:=
+  | mul_case_ii: classify_mul_cases (* int , int *)
+  | mul_case_ff: classify_mul_cases (* float , float *)
+  | mul_default: classify_mul_cases . (* other *)
+
+Definition classify_mul (ty1: type) (ty2: type) :=
+  match ty1,ty2 with
+  | Tint _ _, Tint _ _ => mul_case_ii
+  | Tfloat _ , Tfloat _ => mul_case_ff
+  | _,_  => mul_default
+end.
+
+Inductive classify_div_cases : Set:=
+  | div_case_I32unsi: classify_div_cases (* uns int32 , int *)
+  | div_case_ii: classify_div_cases    (* int , int *) 
+  | div_case_ff: classify_div_cases    (* float , float *)
+  | div_default: classify_div_cases. (* other *)
+
+Definition classify_div (ty1: type) (ty2: type) :=
+  match ty1,ty2 with 
+  | Tint I32 Unsigned, Tint _ _ => div_case_I32unsi 
+  | Tint _ _ , Tint I32 Unsigned => div_case_I32unsi 
+  | Tint _ _ , Tint _ _ => div_case_ii 
+  | Tfloat _ , Tfloat _ => div_case_ff 
+  | _ ,_ => div_default 
+end.
+
+Inductive classify_mod_cases : Set:=
+  | mod_case_I32unsi: classify_mod_cases  (* uns I32 , int *)
+  | mod_case_ii: classify_mod_cases  (* int , int *)
+  | mod_default: classify_mod_cases . (* other *)
+
+Definition classify_mod (ty1: type) (ty2: type) :=
+  match ty1,ty2 with
+  | Tint I32 Unsigned , Tint _ _ => mod_case_I32unsi 
+  | Tint _ _ , Tint I32 Unsigned => mod_case_I32unsi 
+  | Tint _ _ , Tint _ _ => mod_case_ii 
+  | _ , _ => mod_default 
+end .
+
+Inductive classify_shr_cases :Set:=
+  | shr_case_I32unsi:  classify_shr_cases (* uns I32 , int *)
+  | shr_case_ii :classify_shr_cases (* int , int *)
+  | shr_default : classify_shr_cases . (* other *)
+
+Definition classify_shr (ty1: type) (ty2: type) :=
+  match ty1,ty2 with
+  | Tint I32 Unsigned , Tint _ _ => shr_case_I32unsi
+  | Tint _ _ , Tint _ _ => shr_case_ii
+  | _ , _ => shr_default 
+  end.
+
+Inductive classify_cmp_cases : Set:=
+  | cmp_case_I32unsi: classify_cmp_cases (* uns I32 , int *)
+  | cmp_case_ii: classify_cmp_cases  (* int , int*)
+  | cmp_case_ff: classify_cmp_cases  (* float , float *)
+  | cmp_case_pi: classify_cmp_cases  (* ptr | array , int *)
+  | cmp_case_pp:classify_cmp_cases   (* ptr | array , ptr | array *)
+  | cmp_default: classify_cmp_cases . (* other *)
+
+Definition classify_cmp (ty1: type) (ty2: type) :=
+  match ty1,ty2 with 
+  | Tint I32 Unsigned , Tint _ _ => cmp_case_I32unsi 
+  | Tint _ _ , Tint I32 Unsigned => cmp_case_I32unsi 
+  | Tint _ _ , Tint _ _ => cmp_case_ii 
+  | Tfloat _ , Tfloat _ => cmp_case_ff
+  | Tpointer _ , Tint _ _ => cmp_case_pi 
+  | Tarray _ _ , Tint _ _ => cmp_case_pi 
+  | Tpointer _ , Tpointer _ => cmp_case_pp
+  | Tpointer _ , Tarray _ _ => cmp_case_pp
+  | Tarray _ _ ,Tpointer _ => cmp_case_pp
+  | Tarray _ _ ,Tarray _ _ => cmp_case_pp
+  | _ , _ => cmp_default
+  end.
+
+Inductive classify_fun_cases : Set:=
+  | fun_case_f: typelist -> type -> classify_fun_cases   (* type fun | ptr fun*)
+  | fun_default: classify_fun_cases . (* other *)
+
+Definition classify_fun (ty: type) :=
+  match ty with 
+  | Tfunction args res => fun_case_f args res
+  | Tpointer (Tfunction args res) => fun_case_f args res
+  | _ => fun_default
+  end.
+
+(** Mapping between Clight types and Cminor types and external functions *)
+
+Definition typ_of_type (t: type) : AST.typ :=
+  match t with
+  | Tfloat _ => AST.Tfloat
+  | _ => AST.Tint
+  end.
+
+Definition opttyp_of_type (t: type) : option AST.typ :=
+  match t with
+  | Tvoid => None
+  | Tfloat _ => Some AST.Tfloat
+  | _ => Some AST.Tint
+  end.
+
+Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
+  match tl with
+  | Tnil => nil
+  | Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl
+  end.
+
+Definition signature_of_type (args: typelist) (res: type) : signature :=
+  mksignature (typlist_of_typelist args) (opttyp_of_type res).
+
+Definition external_function
+    (id: ident) (targs: typelist) (tres: type) : AST.external_function :=
+  mkextfun id (signature_of_type targs tres).
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
new file mode 100644
index 0000000..8b2f90f
--- /dev/null
+++ b/cfrontend/Ctyping.v
@@ -0,0 +1,420 @@
+(** * Type well-formedness of C programs *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Csyntax.
+
+(** ** Typing rules *)
+
+(** This ``type system'' is very coarse: we check only the typing properties
+  that matter for the translation to be correct.  Essentially,
+  we need to check that the types attached to variable references
+  match the declaration types for those variables. *)
+
+Definition typenv := PTree.t type.
+
+Section TYPING.
+
+Variable env: typenv.
+
+Inductive wt_expr: expr -> Prop :=
+  | wt_Econst_int: forall i ty,
+     wt_expr (Expr (Econst_int i) ty)
+  | wt_Econst_float: forall f ty,
+     wt_expr (Expr (Econst_float f) ty)
+  | wt_Evar: forall id ty,
+     env!id = Some ty ->
+     wt_expr (Expr (Evar id) ty)
+  | wt_Ederef: forall e ty,
+     wt_expr e ->
+     wt_expr (Expr (Ederef e) ty)
+  | wt_Eaddrof: forall e ty,
+     wt_expr e ->
+     wt_expr (Expr (Eaddrof e) ty)
+  | wt_Eunop: forall op e ty,
+     wt_expr e ->
+     wt_expr (Expr (Eunop op e) ty)
+  | wt_Ebinop: forall op e1 e2 ty,
+     wt_expr e1 -> wt_expr e2 ->
+     wt_expr (Expr (Ebinop op e1 e2) ty)
+  | wt_Ecast: forall e ty ty',
+     wt_expr e ->
+     wt_expr (Expr (Ecast ty' e) ty)
+  | 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)
+  | wt_Eorbool: forall e1 e2 ty,
+     wt_expr e1 -> wt_expr e2 ->
+     wt_expr (Expr (Eorbool e1 e2) ty)
+  | wt_Esizeof: forall ty' ty,
+     wt_expr (Expr (Esizeof ty') ty)
+  | wt_Efield: forall e id ty,
+     wt_expr e ->
+     wt_expr (Expr (Efield e id) ty)
+
+with wt_exprlist: exprlist -> Prop :=
+  | wt_Enil:
+     wt_exprlist Enil
+  | wt_Econs: forall e el,
+     wt_expr e -> wt_exprlist el -> wt_exprlist (Econs 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_Ssequence: forall s1 s2,
+     wt_stmt s1 -> wt_stmt s2 ->
+     wt_stmt (Ssequence s1 s2)
+  | wt_Sifthenelse: forall e s1 s2,
+     wt_expr e -> wt_stmt s1 -> wt_stmt s2 ->
+     wt_stmt (Sifthenelse e s1 s2)
+  | wt_Swhile: forall e s,
+     wt_expr e -> wt_stmt s ->
+     wt_stmt (Swhile e s)
+  | wt_Sdowhile: forall e s,
+     wt_expr e -> wt_stmt s ->
+     wt_stmt (Sdowhile e s)
+  | wt_Sfor: forall e s1 s2 s3,
+     wt_expr e -> wt_stmt s1 -> wt_stmt s2 -> wt_stmt s3 ->
+     wt_stmt (Sfor s1 e s2 s3)
+  | wt_Sbreak:
+     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_Sswitch: forall e sl,
+     wt_expr e -> wt_lblstmts sl ->
+     wt_stmt (Sswitch e sl)
+
+with wt_lblstmts: labeled_statements -> Prop :=
+  | wt_LSdefault: forall s,
+     wt_stmt s ->
+     wt_lblstmts (LSdefault s)
+  | wt_LScase: forall n s sl,
+     wt_stmt s -> wt_lblstmts sl ->
+     wt_lblstmts (LScase n s sl).
+
+End TYPING.
+
+Definition add_var (env: typenv) (id_ty: ident * type) : typenv :=
+  PTree.set (fst id_ty) (snd id_ty) env.
+
+Definition add_vars (env: typenv) (vars: list(ident * type)) : typenv :=
+  List.fold_left add_var vars env.
+
+Definition var_names (vars: list(ident * type)) : list ident :=
+  List.map (@fst ident type) vars.
+
+Inductive wt_function: typenv -> function -> Prop :=
+  | wt_function_intro: forall env f,
+      list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
+      wt_stmt (add_vars env (f.(fn_params) ++ f.(fn_vars))) f.(fn_body) ->
+      wt_function env f.
+
+Inductive wt_fundef: typenv -> fundef -> Prop :=
+  | wt_fundef_Internal: forall env f,
+      wt_function env f ->
+      wt_fundef env (Internal f)
+  | wt_fundef_External: forall env id args res,
+      wt_fundef env (External id args res).
+
+Definition add_global_var
+     (env: typenv) (id_ty_init: ident * type * list init_data) : typenv :=
+  match id_ty_init with (id, ty, init) => PTree.set id ty env end.
+
+Definition add_global_vars
+     (env: typenv) (vars: list(ident * type * list init_data)) : typenv :=
+  List.fold_left add_global_var vars env.
+
+Definition add_global_fun
+     (env: typenv) (id_fd: ident * fundef) : typenv :=
+  PTree.set (fst id_fd) (type_of_fundef (snd id_fd)) env.
+
+Definition add_global_funs
+     (env: typenv) (funs: list(ident * fundef)) : typenv :=
+  List.fold_left add_global_fun funs env.
+
+Definition global_typenv (p: program) :=
+  add_global_vars (add_global_funs (PTree.empty type) p.(prog_funct)) p.(prog_defs).
+
+Record wt_program (p: program) : Prop :=  mk_wt_program {
+  wt_program_funct:
+    forall id fd,
+    In (id, fd) p.(prog_funct) ->
+    wt_fundef (global_typenv p) fd;
+  wt_program_main:
+    forall fd,
+    In (p.(prog_main), fd) p.(prog_funct) ->
+    type_of_fundef fd = Tfunction Tnil (Tint I32 Signed)
+}.
+
+(** ** Type-checking algorithm *)
+
+Lemma eq_signedness: forall (s1 s2: signedness), {s1=s2} + {s1<>s2}.
+Proof. decide equality. Qed.
+
+Lemma eq_intsize: forall (s1 s2: intsize), {s1=s2} + {s1<>s2}.
+Proof. decide equality. Qed.
+
+Lemma eq_floatsize: forall (s1 s2: floatsize), {s1=s2} + {s1<>s2}.
+Proof. decide equality. Qed.
+
+Fixpoint eq_type (t1 t2: type) {struct t1}: bool :=
+  match t1, t2 with
+  | Tvoid, Tvoid => true
+  | Tint sz1 sg1, Tint sz2 sg2 =>
+      if eq_intsize sz1 sz2
+      then if eq_signedness sg1 sg2 then true else false
+      else false
+  | Tfloat sz1, Tfloat sz2 =>
+      if eq_floatsize sz1 sz2 then true else false
+  | Tpointer u1, Tpointer u2 => eq_type u1 u2
+  | Tarray u1 sz1, Tarray u2 sz2 =>
+      eq_type u1 u2 && if zeq sz1 sz2 then true else false
+  | Tfunction args1 res1, Tfunction args2 res2 =>
+      eq_typelist args1 args2 && eq_type res1 res2
+  | Tstruct f1, Tstruct f2 => eq_fieldlist f1 f2
+  | Tunion f1, Tunion f2 => eq_fieldlist f1 f2
+  | _, _ => false
+  end
+
+with eq_typelist (t1 t2: typelist) {struct t1} : bool :=
+  match t1, t2 with
+  | Tnil, Tnil => true
+  | Tcons u1 r1, Tcons u2 r2 => eq_type u1 u2 && eq_typelist r1 r2
+  | _, _ => false
+  end
+
+with eq_fieldlist (f1 f2: fieldlist) {struct f1} : bool :=
+  match f1, f2 with
+  | Fnil, Fnil => true
+  | Fcons id1 t1 r1, Fcons id2 t2 r2 =>
+      if ident_eq id1 id2
+      then eq_type t1 t2 && eq_fieldlist r1 r2
+      else false
+  | _, _ => false
+  end.
+
+Ltac TrueInv :=
+  match goal with
+  | [ H: ((if ?x then ?y else false) = true) |- _ ] =>
+        destruct x; [TrueInv | discriminate]
+  | [ H: (?x && ?y = true) |- _ ] =>
+        elim (andb_prop _ _ H); clear H; intros; TrueInv
+  | _ =>
+        idtac
+  end.
+
+Scheme type_ind_3 := Induction for type Sort Prop
+  with typelist_ind_3 := Induction for typelist Sort Prop
+  with fieldlist_ind_3 := Induction for fieldlist Sort Prop.
+
+Lemma eq_type_correct:
+  forall t1 t2, eq_type t1 t2 = true -> t1 = t2.
+Proof.
+  apply (type_ind_3 (fun t1 => forall t2, eq_type t1 t2 = true -> t1 = t2)
+                    (fun t1 => forall t2, eq_typelist t1 t2 = true -> t1 = t2)
+                    (fun t1 => forall t2, eq_fieldlist t1 t2 = true -> t1 = t2));
+  intros; destruct t2; simpl in *; try discriminate.
+  auto.
+  TrueInv. congruence.
+  TrueInv. congruence.
+  decEq; auto.
+  TrueInv. decEq; auto.
+  TrueInv. decEq; auto.
+  decEq; auto.
+  decEq; auto.
+  auto.
+  TrueInv. decEq; auto.
+  auto.
+  TrueInv. decEq; auto.
+Qed.
+
+Section TYPECHECKING.
+
+Variable env: typenv.
+
+Fixpoint typecheck_expr (a: Csyntax.expr) {struct a} : bool :=
+  match a with
+  | Expr ad aty => typecheck_exprdescr ad aty
+  end
+
+with typecheck_exprdescr (a: Csyntax.expr_descr) (ty: type) {struct a} : bool :=
+  match a with
+  | Csyntax.Econst_int n => true
+  | Csyntax.Econst_float n => true
+  | Csyntax.Evar id =>
+      match env!id with
+      | None => false
+      | Some ty' => eq_type ty ty'
+      end
+  | Csyntax.Ederef b => typecheck_expr b
+  | Csyntax.Eaddrof b => typecheck_expr b
+  | Csyntax.Eunop op b => typecheck_expr b
+  | 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
+
+with typecheck_exprlist (al: Csyntax.exprlist): bool :=
+  match al with
+  | Csyntax.Enil => true
+  | Csyntax.Econs a1 a2 => typecheck_expr a1 && typecheck_exprlist a2
+  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.
+
+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.
+  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:
+  forall a, typecheck_exprlist a = true -> wt_exprlist env a.
+Proof.
+  induction a; simpl; intros.
+  constructor.
+  TrueInv. constructor; auto. apply typecheck_expr_correct; auto.
+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.Ssequence s1 s2 => typecheck_stmt s1 && typecheck_stmt s2
+  | Csyntax.Sifthenelse e s1 s2 =>
+      typecheck_expr e && typecheck_stmt s1 && typecheck_stmt s2
+  | Csyntax.Swhile e s1 => typecheck_expr e && typecheck_stmt s1
+  | Csyntax.Sdowhile e s1 => typecheck_expr e && typecheck_stmt s1
+  | Csyntax.Sfor e1 e2 e3 s1 =>
+      typecheck_stmt e1 && typecheck_expr e2 &&
+      typecheck_stmt e3 && typecheck_stmt s1
+  | Csyntax.Sbreak => true
+  | Csyntax.Scontinue => true
+  | Csyntax.Sreturn (Some e) => typecheck_expr e
+  | Csyntax.Sreturn None => true
+  | Csyntax.Sswitch e sl => typecheck_expr e && typecheck_lblstmts sl
+  end    
+
+with typecheck_lblstmts (sl: labeled_statements) {struct sl}: bool :=
+  match sl with
+  | LSdefault s => typecheck_stmt s
+  | LScase _ s rem => typecheck_stmt s && typecheck_lblstmts rem
+  end.
+
+Scheme stmt_ind_2 := Induction for statement Sort Prop
+  with lblstmts_ind_2 := Induction for labeled_statements Sort Prop.
+
+Lemma typecheck_stmt_correct:
+  forall s, typecheck_stmt s = true -> wt_stmt env s.
+Proof.
+  generalize typecheck_expr_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.
+Qed.
+
+End TYPECHECKING.
+
+Definition typecheck_function (env: typenv) (f: function) : bool :=
+  if list_norepet_dec ident_eq
+                      (var_names f.(fn_params) ++ var_names f.(fn_vars))
+  then typecheck_stmt (add_vars env (f.(fn_params) ++ f.(fn_vars)))
+                      f.(fn_body)
+  else false.
+
+Lemma typecheck_function_correct:
+  forall env f, typecheck_function env f = true -> wt_function env f.
+Proof.
+  unfold typecheck_function; intros; TrueInv.
+  constructor. auto. apply typecheck_stmt_correct; auto.
+Qed.
+
+Definition typecheck_fundef (main: ident) (env: typenv) (id_fd: ident * fundef) : bool :=
+  let (id, fd) := id_fd in
+  match fd with
+  | Internal f => typecheck_function env f
+  | External _ _ _ => true
+  end &&
+  if ident_eq id main
+  then eq_type (type_of_fundef fd) (Tfunction Tnil (Tint I32 Signed))
+  else true.
+
+Lemma typecheck_fundef_correct:
+  forall main env id fd,
+  typecheck_fundef main env (id, fd) = true ->
+  wt_fundef env fd /\
+  (id = main -> type_of_fundef fd = Tfunction Tnil (Tint I32 Signed)).
+Proof.
+  intros. unfold typecheck_fundef in H; TrueInv.
+  split. 
+    destruct fd.
+    constructor. apply typecheck_function_correct; auto. 
+    constructor.
+  intro. destruct (ident_eq id main). 
+  apply eq_type_correct; auto.
+  congruence.
+Qed.
+
+Definition typecheck_program (p: program) : bool :=
+  List.forallb (typecheck_fundef p.(prog_main) (global_typenv p))
+               p.(prog_funct).
+
+Lemma typecheck_program_correct:
+  forall p, typecheck_program p = true -> wt_program p.
+Proof.
+  unfold typecheck_program; intros. 
+  rewrite List.forallb_forall in H. 
+  constructor; intros.
+  exploit typecheck_fundef_correct; eauto. tauto. 
+  exploit typecheck_fundef_correct; eauto. tauto. 
+Qed.