Merge branch 'master' into cleanup

23 files changed, 1493 insertions, 989 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 6eabfbf4..16e8a80d 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -1078,7 +1078,7 @@ let convertFundef loc env fd =
       a_access = Sections.Access_default;
       a_inline = fd.fd_inline && not fd.fd_vararg;  (* PR#15 *)
       a_loc = loc };
-  (id', Gfun(Csyntax.Internal
+  (id', Gfun(Ctypes.Internal
           {fn_return = ret;
            fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib;
            fn_params = params;
@@ -1088,6 +1088,7 @@ let convertFundef loc env fd =
 (** External function declaration *)
 
 let re_builtin = Str.regexp "__builtin_"
+let re_runtime = Str.regexp "__i64_"
 
 let convertFundecl env (sto, id, ty, optinit) =
   let (args, res, cconv) =
@@ -1100,11 +1101,12 @@ let convertFundecl env (sto, id, ty, optinit) =
   let ef =
     if id.name = "malloc" then EF_malloc else
     if id.name = "free" then EF_free else
+    if Str.string_match re_runtime id.name 0 then EF_runtime(id'', sg) else
     if Str.string_match re_builtin id.name 0
     && List.mem_assoc id.name builtins.functions
     then EF_builtin(id'', sg)
     else EF_external(id'', sg) in
-  (id', Gfun(Csyntax.External(ef, args, res, cconv)))
+  (id', Gfun(Ctypes.External(ef, args, res, cconv)))
 
 (** Initializers *)
 
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7e966ffe..bf88e033 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -536,6 +536,7 @@ Definition do_external (ef: external_function):
   match ef with
   | EF_external name sg => do_external_function name sg ge
   | EF_builtin name sg => do_external_function name sg ge
+  | EF_runtime name sg => do_external_function name sg ge
   | EF_vload chunk => do_ef_volatile_load chunk
   | EF_vstore chunk => do_ef_volatile_store chunk
   | EF_malloc => do_ef_malloc
@@ -558,6 +559,8 @@ Proof with try congruence.
   eapply do_external_function_sound; eauto.
 (* EF_builtin *)
   eapply do_external_function_sound; eauto.
+(* EF_runtime *)
+  eapply do_external_function_sound; eauto.
 (* EF_vload *)
   unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
   mydestr. destruct p as [[w'' t''] v]; mydestr.
@@ -604,6 +607,8 @@ Proof.
   eapply do_external_function_complete; eauto.
 (* EF_builtin *)
   eapply do_external_function_complete; eauto.
+(* EF_runtime *)
+  eapply do_external_function_complete; eauto.
 (* EF_vload *)
   inv H; unfold do_ef_volatile_load.
   exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
@@ -645,11 +650,11 @@ Section EXPRS.
 Variable e: env.
 Variable w: world.
 
-Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) :=
+Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) (m: mem) : option (list val) :=
   match vtl, tl with
   | nil, Tnil => Some nil
   | (v1,t1)::vtl, Tcons t1' tl =>
-      do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl)
+      do v <- sem_cast v1 t1 t1' m; do vl <- sem_cast_arguments vtl tl m; Some(v::vl)
   | _, _ => None
   end.
 
@@ -772,7 +777,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   | RV, Ecast r1 ty =>
       match is_val r1 with
       | Some(v1, ty1) =>
-          do v <- sem_cast v1 ty1 ty;
+          do v <- sem_cast v1 ty1 ty m;
           topred (Rred "red_cast" (Eval v ty) m E0)
       | None =>
           incontext (fun x => Ecast x ty) (step_expr RV r1 m)
@@ -811,7 +816,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
           check type_eq ty1 ty;
-          do v <- sem_cast v2 ty2 ty1;
+          do v <- sem_cast v2 ty2 ty1 m;
           do w',t,m' <- do_assign_loc w ty1 m b ofs v;
           topred (Rred "red_assign" (Eval v ty) m' t)
       | _, _ =>
@@ -856,7 +861,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   | RV, Eparen r1 tycast ty =>
       match is_val r1 with
       | Some (v1, ty1) =>
-          do v <- sem_cast v1 ty1 tycast;
+          do v <- sem_cast v1 ty1 tycast m;
           topred (Rred "red_paren" (Eval v ty) m E0)
       | None =>
           incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m)
@@ -867,7 +872,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           match classify_fun tyf with
           | fun_case_f tyargs tyres cconv =>
               do fd <- Genv.find_funct ge vf;
-              do vargs <- sem_cast_arguments vtl tyargs;
+              do vargs <- sem_cast_arguments vtl tyargs m;
               check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv);
               topred (Callred "red_call" fd vargs ty m)
           | _ => stuck
@@ -879,7 +884,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   | RV, Ebuiltin ef tyargs rargs ty =>
       match is_val_list rargs with
       | Some vtl =>
-          do vargs <- sem_cast_arguments vtl tyargs;
+          do vargs <- sem_cast_arguments vtl tyargs m;
           match do_external ef w vargs m with
           | None => stuck
           | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t)
@@ -915,7 +920,7 @@ Inductive imm_safe_t: kind -> expr -> mem -> Prop :=
       context RV to C ->
       imm_safe_t to (C r) m
   | imm_safe_t_callred: forall to C r m fd args ty,
-      callred ge r fd args ty ->
+      callred ge r m fd args ty ->
       context RV to C ->
       imm_safe_t to (C r) m.
 
@@ -961,7 +966,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
       exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v
   | Ecast (Eval v1 ty1) ty =>
-      exists v, sem_cast v1 ty1 ty = Some v
+      exists v, sem_cast v1 ty1 ty m = Some v
   | Eseqand (Eval v1 ty1) r2 ty =>
       exists b, bool_val v1 ty1 m = Some b
   | Eseqor (Eval v1 ty1) r2 ty =>
@@ -970,7 +975,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists b, bool_val v1 ty1 m = Some b
   | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
       exists v, exists m', exists t, exists w',
-      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w'
+      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w'
   | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
       exists t, exists v1, exists w',
       ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w'
@@ -980,18 +985,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
   | Eparen (Eval v1 ty1) tycast ty =>
-      exists v, sem_cast v1 ty1 tycast = Some v
+      exists v, sem_cast v1 ty1 tycast m = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs tyres cconv fd vl,
          classify_fun tyf = fun_case_f tyargs tyres cconv
       /\ Genv.find_funct ge vf = Some fd
-      /\ cast_arguments rargs tyargs vl
+      /\ cast_arguments m rargs tyargs vl
       /\ type_of_fundef fd = Tfunction tyargs tyres cconv
   | Ebuiltin ef tyargs rargs ty =>
       exprlist_all_values rargs ->
       exists vargs t vres m' w',
-         cast_arguments rargs tyargs vargs
+         cast_arguments m rargs tyargs vargs
       /\ external_call ef ge vargs m t vres m'
       /\ possible_trace w t w'
   | _ => True
@@ -1028,7 +1033,7 @@ Qed.
 
 Lemma callred_invert:
   forall r fd args ty m,
-  callred ge r fd args ty ->
+  callred ge r m fd args ty ->
   invert_expr_prop r m.
 Proof.
   intros. inv H. simpl.
@@ -1124,7 +1129,7 @@ Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop :=
   match k, rd with
   | LV, Lred _ l' m' => lred ge e a m l' m'
   | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w'
-  | RV, Callred _ fd args tyres m' => callred ge a fd args tyres /\ m' = m
+  | RV, Callred _ fd args tyres m' => callred ge a m fd args tyres /\ m' = m
   | LV, Stuckred => ~imm_safe_t k a m
   | RV, Stuckred => ~imm_safe_t k a m
   | _, _ => False
@@ -1152,10 +1157,10 @@ Ltac monadInv :=
   end.
 
 Lemma sem_cast_arguments_sound:
-  forall rargs vtl tyargs vargs,
+  forall m rargs vtl tyargs vargs,
   is_val_list rargs = Some vtl ->
-  sem_cast_arguments vtl tyargs = Some vargs ->
-  cast_arguments rargs tyargs vargs.
+  sem_cast_arguments vtl tyargs m = Some vargs ->
+  cast_arguments m rargs tyargs vargs.
 Proof.
   induction rargs; simpl; intros.
   inv H. destruct tyargs; simpl in H0; inv H0. constructor.
@@ -1164,9 +1169,9 @@ Proof.
 Qed.
 
 Lemma sem_cast_arguments_complete:
-  forall al tyl vl,
-  cast_arguments al tyl vl ->
-  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl.
+  forall m al tyl vl,
+  cast_arguments m al tyl vl ->
+  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl m = Some vl.
 Proof.
   induction 1.
   exists (@nil (val * type)); auto.
@@ -1396,7 +1401,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* cast *)
   destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
-  destruct (sem_cast v ty' ty) as [v'|] eqn:?...
+  destruct (sem_cast v ty' ty m) as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
@@ -1433,7 +1438,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
   (* top *)
   destruct (type_eq ty1 ty)... subst ty1.
-  destruct (sem_cast v2 ty2 ty) as [v|] eqn:?...
+  destruct (sem_cast v2 ty2 ty m) as [v|] eqn:?...
   destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|] eqn:?.
   exploit do_assign_loc_sound; eauto. intros [P Q].
   apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto.
@@ -1478,7 +1483,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   (* top *)
   destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?...
   destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?...
+  destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?...
   destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))...
   apply topred_ok; auto. red. split; auto. eapply red_call; eauto.
   eapply sem_cast_arguments_sound; eauto.
@@ -1494,7 +1499,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (is_val_list rargs) as [vtl | ] eqn:?.
   exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?...
+  destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?...
   destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?...
   exploit do_ef_external_sound; eauto. intros [EC PT].
   apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto.
@@ -1514,7 +1519,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* paren *)
   destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
-  destruct (sem_cast v ty' tycast) as [v'|] eqn:?...
+  destruct (sem_cast v ty' tycast m) as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
@@ -1607,7 +1612,7 @@ Qed.
 
 Lemma callred_topred:
   forall a fd args ty m,
-  callred ge a fd args ty ->
+  callred ge a m fd args ty ->
   exists rule, step_expr RV a m = topred (Callred rule fd args ty m).
 Proof.
   induction 1; simpl.
@@ -1961,7 +1966,7 @@ Definition do_step (w: world) (s: state) : list transition :=
             then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m)
             else ret "step_for_false" (State f Sskip k e m)
         | Kreturn k =>
-            do v' <- sem_cast v ty f.(fn_return);
+            do v' <- sem_cast v ty f.(fn_return) m;
             do m' <- Mem.free_list m (blocks_of_env ge e);
             ret "step_return_2" (Returnstate v' (call_cont k) m')
         | Kswitch1 sl k =>
@@ -2165,7 +2170,7 @@ Proof with (unfold ret; eauto with coqlib).
   apply extensionality; auto.
 (* callred *)
   unfold do_step; rewrite NOTVAL.
-  exploit callred_topred; eauto. instantiate (1 := m). instantiate (1 := w). instantiate (1 := e).
+  exploit callred_topred; eauto. instantiate (1 := w). instantiate (1 := e).
   intros (rule & STEP). exists rule.
   change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)).
   apply in_map.
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 8722da69..e6426fb8 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -146,9 +146,7 @@ Definition var_names (vars: list(ident * type)) : list ident :=
 (** Functions can either be defined ([Internal]) or declared as
   external functions ([External]). *)
 
-Inductive fundef : Type :=
-  | Internal: function -> fundef
-  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+Definition fundef := Ctypes.fundef function.
 
 (** The type of a function definition. *)
 
@@ -163,45 +161,16 @@ Definition type_of_fundef (f: fundef) : type :=
 
 (** ** Programs *)
 
-(** A program is composed of:
+(** As defined in module [Ctypes], a program, or compilation unit, is
+  composed of:
 - a list of definitions of functions and global variables;
 - the names of functions and global variables that are public (not static);
 - the name of the function that acts as entry point ("main" function).
-- a list of definitions for structure and union names;
-- the corresponding composite environment;
-*)
-
-Record program : Type := {
-  prog_defs: list (ident * globdef fundef type);
-  prog_public: list ident;
-  prog_main: ident;
-  prog_types: list composite_definition;
-  prog_comp_env: composite_env;
-  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
-}.
+- a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
 
-Definition program_of_program (p: program) : AST.program fundef type :=
-  {| AST.prog_defs := p.(prog_defs);
-     AST.prog_public := p.(prog_public);
-     AST.prog_main := p.(prog_main) |}.
-
-Coercion program_of_program: program >-> AST.program.
-
-Program Definition make_program (types: list composite_definition)
-                                (defs: list (ident * globdef fundef type))
-                                (public: list ident)
-                                (main: ident): res program :=
-  match build_composite_env types with
-  | OK env =>
-      OK {| prog_defs := defs;
-            prog_public := public;
-            prog_main := main;
-            prog_types := types;
-            prog_comp_env := env;
-            prog_comp_env_eq := _ |}
-  | Error msg =>
-      Error msg
-  end.
+Definition program := Ctypes.program function.
 
 (** * Operational semantics *)
 
@@ -412,7 +381,7 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr (Ebinop op a1 a2 ty) v
   | eval_Ecast:   forall a ty v1 v,
       eval_expr a v1 ->
-      sem_cast v1 (typeof a) ty = Some v ->
+      sem_cast v1 (typeof a) ty m = Some v ->
       eval_expr (Ecast a ty) v
   | eval_Esizeof: forall ty1 ty,
       eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
@@ -464,7 +433,7 @@ Inductive eval_exprlist: list expr -> typelist -> list val -> Prop :=
       eval_exprlist nil Tnil nil
   | eval_Econs:   forall a bl ty tyl v1 v2 vl,
       eval_expr a v1 ->
-      sem_cast v1 (typeof a) ty = Some v2 ->
+      sem_cast v1 (typeof a) ty m = Some v2 ->
       eval_exprlist bl tyl vl ->
       eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl).
 
@@ -580,7 +549,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_assign:   forall f a1 a2 k e le m loc ofs v2 v m',
       eval_lvalue e le m a1 loc ofs ->
       eval_expr e le m a2 v2 ->
-      sem_cast v2 (typeof a2) (typeof a1) = Some v ->
+      sem_cast v2 (typeof a2) (typeof a1) m = Some v ->
       assign_loc ge (typeof a1) m loc ofs v m' ->
       step (State f (Sassign a1 a2) k e le m)
         E0 (State f Sskip k e le m')
@@ -647,7 +616,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (Returnstate Vundef (call_cont k) m')
   | step_return_1: forall f a k e le m v v' m',
       eval_expr e le m a v ->
-      sem_cast v (typeof a) f.(fn_return) = Some v' ->
+      sem_cast v (typeof a) f.(fn_return) m = Some v' ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f (Sreturn (Some a)) k e le m)
         E0 (Returnstate v' (call_cont k) m')
@@ -774,4 +743,3 @@ Proof.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
-
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index ee653d50..92457586 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -60,11 +60,11 @@ Definition outcome_switch (out: outcome) : outcome :=
   | o => o
   end.
 
-Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
+Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop :=
   match out, t with
   | Out_normal, Tvoid => v = Vundef
   | Out_return None, Tvoid => v = Vundef
-  | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t = Some v
+  | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t m = Some v
   | _, _ => False
   end.
 
@@ -81,7 +81,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
   | exec_Sassign:   forall e le m a1 a2 loc ofs v2 v m',
       eval_lvalue ge e le m a1 loc ofs ->
       eval_expr ge e le m a2 v2 ->
-      sem_cast v2 (typeof a2) (typeof a1) = Some v ->
+      sem_cast v2 (typeof a2) (typeof a1) m = Some v ->
       assign_loc ge (typeof a1) m loc ofs v m' ->
       exec_stmt e le m (Sassign a1 a2)
                E0 le m' Out_normal
@@ -168,7 +168,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
       bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out ->
-      outcome_result_value out f.(fn_return) vres ->
+      outcome_result_value out f.(fn_return) vres m3 ->
       Mem.free_list m3 (blocks_of_env ge e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
   | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index c2b59fbe..b9a28ee1 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -12,19 +12,10 @@
 
 (** Translation from Csharpminor to Cminor. *)
 
-Require Import FSets.
-Require FSetAVL.
-Require Import Orders.
-Require Mergesort.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Ordered.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Csharpminor.
-Require Import Cminor.
+Require Import FSets FSetAVL Orders Mergesort.
+Require Import Coqlib Maps Ordered Errors Integers Floats.
+Require Import AST Linking.
+Require Import Csharpminor Cminor.
 
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 7a5d882e..2f551d68 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -12,61 +12,54 @@
 
 (** Correctness proof for Cminor generation. *)
 
-Require Import Coq.Program.Equality.
-Require Import FSets.
-Require Import Permutation.
-Require Import Coqlib.
+Require Import Coq.Program.Equality FSets Permutation.
+Require Import FSets FSetAVL Orders Mergesort.
+Require Import Coqlib Maps Ordered Errors Integers Floats.
 Require Intv.
-Require Import Errors.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Switch.
-Require Import Csharpminor.
-Require Import Cminor.
-Require Import Cminorgen.
+Require Import AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Csharpminor Switch Cminor Cminorgen.
 
 Open Local Scope error_monad_scope.
 
+Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) :=
+  match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transl_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. apply match_transform_partial_program; auto.
+Qed.
+
 Section TRANSLATION.
 
 Variable prog: Csharpminor.program.
 Variable tprog: program.
-Hypothesis TRANSL: transl_program prog = OK tprog.
+Hypothesis TRANSL: match_prog prog tprog.
 Let ge : Csharpminor.genv := Genv.globalenv prog.
 Let tge: genv := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_transf_partial transl_fundef _ TRANSL).
+Proof (Genv.find_symbol_transf_partial TRANSL).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof (Genv.public_symbol_transf_partial transl_fundef _ TRANSL).
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf_partial TRANSL).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Csharpminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).
+Proof (Genv.find_funct_ptr_transf_partial TRANSL).
 
 Lemma functions_translated:
   forall (v: val) (f: Csharpminor.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial transl_fundef _ TRANSL).
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof (Genv.find_var_info_transf_partial transl_fundef _ TRANSL).
+Proof (Genv.find_funct_transf_partial TRANSL).
 
 Lemma sig_preserved_body:
   forall f tf cenv size,
@@ -2029,8 +2022,7 @@ Proof.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor. eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. eexact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   assert (MCS': match_callstack f' m' tm'
                  (Frame cenv tfn e le te sp lo hi :: cs)
                  (Mem.nextblock m') (Mem.nextblock tm')).
@@ -2184,8 +2176,7 @@ Opaque PTree.set.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. eexact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
   apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
@@ -2224,11 +2215,11 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor.
-  apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto.
+  apply (Genv.init_mem_transf_partial TRANSL). eauto.
   simpl. fold tge. rewrite symbols_preserved.
   replace (prog_main tprog) with (prog_main prog). eexact H0.
   symmetry. unfold transl_program in TRANSL.
-  eapply transform_partial_program_main; eauto.
+  eapply match_program_main; eauto. 
   eexact FIND.
   rewrite <- H2. apply sig_preserved; auto.
   eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z).
@@ -2250,7 +2241,7 @@ Theorem transl_program_correct:
   forward_simulation (Csharpminor.semantics prog) (Cminor.semantics tprog).
 Proof.
   eapply forward_simulation_star; eauto.
-  eexact public_preserved.
+  apply senv_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
   eexact transl_step_correct.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index b4784028..4ac56b04 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -130,7 +130,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   | _, _ => cast_case_default
   end.
 
-(** Semantics of casts.  [sem_cast v1 t1 t2 = Some v2] if value [v1],
+(** Semantics of casts.  [sem_cast v1 t1 t2 m = Some v2] if value [v1],
   viewed with static type [t1], can be converted  to type [t2],
   resulting in value [v2].  *)
 
@@ -198,7 +198,7 @@ Definition cast_single_long (si : signedness) (f: float32) : option int64 :=
   | Unsigned => Float32.to_longu f
   end.
 
-Definition sem_cast (v: val) (t1 t2: type) : option val :=
+Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
   match classify_cast t1 t2 with
   | cast_case_neutral =>
       match v with
@@ -273,6 +273,7 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
   | cast_case_p2bool =>
       match v with
       | Vint i => Some (Vint (cast_int_int IBool Signed i))
+      | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vone else None
       | _ => None
       end
   | cast_case_l2l =>
@@ -586,13 +587,13 @@ Definition sem_binarith
     (sem_long: signedness -> int64 -> int64 -> option val)
     (sem_float: float -> float -> option val)
     (sem_single: float32 -> float32 -> option val)
-    (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
+    (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val :=
   let c := classify_binarith t1 t2 in
   let t := binarith_type c in
-  match sem_cast v1 t1 t with
+  match sem_cast v1 t1 t m with
   | None => None
   | Some v1' =>
-  match sem_cast v2 t2 t with
+  match sem_cast v2 t2 t m with
   | None => None
   | Some v2' =>
   match c with
@@ -637,18 +638,22 @@ Definition classify_add (ty1: type) (ty2: type) :=
   | _, _ => add_default
   end.
 
-Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val :=
   match classify_add t1 t2 with
   | add_case_pi ty =>                 (**r pointer plus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 =>
         Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+      | Vint n1, Vint n2 =>
+        Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
       | _,  _ => None
       end
   | add_case_ip ty =>                 (**r integer plus pointer *)
       match v1,v2 with
       | Vint n1, Vptr b2 ofs2 =>
         Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
+      | Vint n1, Vint n2 =>
+        Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
       | _,  _ => None
       end
   | add_case_pl ty =>                 (**r pointer plus long *)
@@ -656,6 +661,9 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
       | Vptr b1 ofs1, Vlong n2 =>
         let n2 := Int.repr (Int64.unsigned n2) in
         Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+      | Vint n1, Vlong n2 =>
+        let n2 := Int.repr (Int64.unsigned n2) in
+        Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
       | _,  _ => None
       end
   | add_case_lp ty =>                 (**r long plus pointer *)
@@ -663,6 +671,9 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
       | Vlong n1, Vptr b2 ofs2 =>
         let n1 := Int.repr (Int64.unsigned n1) in
         Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
+      | Vlong n1, Vint n2 =>
+        let n1 := Int.repr (Int64.unsigned n1) in
+        Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
       | _,  _ => None
       end
   | add_default =>
@@ -671,7 +682,7 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
         (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2)))
         (fun n1 n2 => Some(Vfloat(Float.add n1 n2)))
         (fun n1 n2 => Some(Vsingle(Float32.add n1 n2)))
-        v1 t1 v2 t2
+        v1 t1 v2 t2 m
   end.
 
 (** *** Subtraction *)
@@ -690,12 +701,14 @@ Definition classify_sub (ty1: type) (ty2: type) :=
   | _, _ => sub_default
   end.
 
-Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m:mem): option val :=
   match classify_sub t1 t2 with
   | sub_case_pi ty =>            (**r pointer minus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 =>
           Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+      | Vint n1, Vint n2 =>
+          Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
       | _,  _ => None
       end
   | sub_case_pl ty =>            (**r pointer minus long *)
@@ -703,6 +716,9 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
       | Vptr b1 ofs1, Vlong n2 =>
           let n2 := Int.repr (Int64.unsigned n2) in
           Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+      | Vint n1, Vlong n2 =>
+          let n2 := Int.repr (Int64.unsigned n2) in
+          Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
       | _,  _ => None
       end
   | sub_case_pp ty =>          (**r pointer minus pointer *)
@@ -722,20 +738,20 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
         (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2)))
         (fun n1 n2 => Some(Vfloat(Float.sub n1 n2)))
         (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2)))
-        v1 t1 v2 t2
+        v1 t1 v2 t2 m
   end.
 
 (** *** Multiplication, division, modulus *)
 
-Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.mul n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2)))
     (fun n1 n2 => Some(Vfloat(Float.mul n1 n2)))
     (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2)))
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 =>
       match sg with
@@ -759,9 +775,9 @@ Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       end)
     (fun n1 n2 => Some(Vfloat(Float.div n1 n2)))
     (fun n1 n2 => Some(Vsingle(Float32.div n1 n2)))
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 =>
       match sg with
@@ -785,31 +801,31 @@ Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       end)
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.and n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2)))
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.or n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2)))
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
-Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 => Some(Vint(Int.xor n1 n2)))
     (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2)))
     (fun n1 n2 => None)
     (fun n1 n2 => None)
-    v1 t1 v2 t2.
+    v1 t1 v2 t2 m.
 
 (** *** Shifts *)
 
@@ -931,7 +947,7 @@ Definition sem_cmp (c:comparison)
             Some(Val.of_bool(Float.cmp c n1 n2)))
         (fun n1 n2 =>
             Some(Val.of_bool(Float32.cmp c n1 n2)))
-        v1 t1 v2 t2
+        v1 t1 v2 t2 m
   end.
 
 (** ** Function applications *)
@@ -988,14 +1004,14 @@ Definition sem_binary_operation
     (v1: val) (t1: type) (v2: val) (t2:type)
     (m: mem): option val :=
   match op with
-  | Oadd => sem_add cenv v1 t1 v2 t2
-  | Osub => sem_sub cenv 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 t1 v2 t2
-  | Oor  => sem_or v1 t1 v2 t2
-  | Oxor  => sem_xor v1 t1 v2 t2
+  | Oadd => sem_add cenv v1 t1 v2 t2 m
+  | Osub => sem_sub cenv v1 t1 v2 t2 m
+  | Omul => sem_mul v1 t1 v2 t2 m
+  | Omod => sem_mod v1 t1 v2 t2 m
+  | Odiv => sem_div v1 t1 v2 t2 m
+  | Oand => sem_and v1 t1 v2 t2 m
+  | Oor  => sem_or v1 t1 v2 t2 m
+  | Oxor  => sem_xor v1 t1 v2 t2 m
   | Oshl => sem_shl v1 t1 v2 t2
   | Oshr  => sem_shr v1 t1 v2 t2
   | Oeq => sem_cmp Ceq v1 t1 v2 t2 m
@@ -1006,10 +1022,10 @@ Definition sem_binary_operation
   | Oge => sem_cmp Cge v1 t1 v2 t2 m
   end.
 
-Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) :=
+Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) (m: mem) :=
   match id with
-  | Incr => sem_add cenv v ty (Vint Int.one) type_int32s
-  | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s
+  | Incr => sem_add cenv v ty (Vint Int.one) type_int32s m
+  | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s m
   end.
 
 Definition incrdecr_type (ty: type) :=
@@ -1074,11 +1090,11 @@ Ltac TrivialInject :=
   | _ => idtac
   end.
 
-Lemma sem_cast_inject:
+Lemma sem_cast_inj:
   forall v1 ty1 ty v tv1,
-  sem_cast v1 ty1 ty = Some v ->
+  sem_cast v1 ty1 ty m = Some v ->
   Val.inject f v1 tv1 ->
-  exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv.
+  exists tv, sem_cast tv1 ty1 ty m'= Some tv /\ Val.inject f v tv.
 Proof.
   unfold sem_cast; intros; destruct (classify_cast ty1 ty);
   inv H0; inv H; TrivialInject.
@@ -1087,6 +1103,8 @@ Proof.
 - destruct (cast_single_int si2 f0); inv H1; TrivialInject.
 - destruct (cast_float_long si2 f0); inv H1; TrivialInject.
 - destruct (cast_single_long si2 f0); inv H1; TrivialInject.
+- destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VALID; inv H2.
+  erewrite weak_valid_pointer_inj by eauto. TrivialInject. 
 - destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto.
 - destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto.
 - econstructor; eauto.
@@ -1119,13 +1137,13 @@ Definition optval_self_injects (ov: option val) : Prop :=
 
 Remark sem_binarith_inject:
   forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2',
-  sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v ->
+  sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 m = Some v ->
   Val.inject f v1 v1' -> Val.inject f v2 v2' ->
   (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) ->
   (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) ->
   (forall n1 n2, optval_self_injects (sem_float n1 n2)) ->
   (forall n1 n2, optval_self_injects (sem_single n1 n2)) ->
-  exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'.
+  exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 m' = Some v' /\ Val.inject f v v'.
 Proof.
   intros.
   assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v).
@@ -1135,10 +1153,10 @@ Proof.
   unfold sem_binarith in *.
   set (c := classify_binarith t1 t2) in *.
   set (t := binarith_type c) in *.
-  destruct (sem_cast v1 t1 t) as [w1|] eqn:C1; try discriminate.
-  destruct (sem_cast v2 t2 t) as [w2|] eqn:C2; try discriminate.
-  exploit (sem_cast_inject v1); eauto. intros (w1' & C1' & INJ1).
-  exploit (sem_cast_inject v2); eauto. intros (w2' & C2' & INJ2).
+  destruct (sem_cast v1 t1 t m) as [w1|] eqn:C1; try discriminate.
+  destruct (sem_cast v2 t2 t m) as [w2|] eqn:C2; try discriminate.
+  exploit (sem_cast_inj v1); eauto. intros (w1' & C1' & INJ1).
+  exploit (sem_cast_inj v2); eauto. intros (w2' & C2' & INJ2).
   rewrite C1'; rewrite C2'.
   destruct c; inv INJ1; inv INJ2; discriminate || eauto.
 Qed.
@@ -1202,25 +1220,25 @@ Proof.
   unfold sem_binary_operation; intros; destruct op.
 - (* add *)
   unfold sem_add in *; destruct (classify_add ty1 ty2).
-  + inv H0; inv H1; inv H. TrivialInject.
+  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
     econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  + inv H0; inv H1; inv H. TrivialInject.
+  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
     econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  + inv H0; inv H1; inv H. TrivialInject.
+  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
     econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  + inv H0; inv H1; inv H. TrivialInject.
+  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
     econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
   + eapply sem_binarith_inject; eauto; intros; exact I.
 - (* sub *)
   unfold sem_sub in *; destruct (classify_sub ty1 ty2).
-  + inv H0; inv H1; inv H. TrivialInject.
+  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
     econstructor. eauto. rewrite Int.sub_add_l. auto.
   + inv H0; inv H1; inv H. TrivialInject.
     destruct (eq_block b1 b0); try discriminate. subst b1.
     rewrite H0 in H2; inv H2. rewrite dec_eq_true.
     destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3.
     rewrite Int.sub_shifted. TrivialInject.
-  + inv H0; inv H1; inv H. TrivialInject.
+  + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
     econstructor. eauto. rewrite Int.sub_add_l. auto.
   + eapply sem_binarith_inject; eauto; intros; exact I.
 - (* mul *)
@@ -1282,6 +1300,17 @@ Qed.
 
 End GENERIC_INJECTION.
 
+Lemma sem_cast_inject:
+  forall f v1 ty1 ty m v tv1 tm,
+  sem_cast v1 ty1 ty m = Some v ->
+  Val.inject f v1 tv1 ->
+  Mem.inject f m tm ->
+  exists tv, sem_cast tv1 ty1 ty tm = Some tv /\ Val.inject f v tv.
+Proof.
+  intros. eapply sem_cast_inj; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+Qed.
+
 Lemma sem_unary_operation_inject:
   forall f m m' op v1 ty1 v tv1,
   sem_unary_operation op v1 ty1 m = Some v ->
@@ -1321,20 +1350,16 @@ Qed.
 (** * Some properties of operator semantics *)
 
 (** This section collects some common-sense properties about the type
-  classification and semantic functions above.  These properties are
-  not used in the CompCert semantics preservation proofs, but increase
+  classification and semantic functions above.  Some properties are used
+  in the CompCert semantics preservation proofs.  Others are not, but increase
   confidence in the specification and its relation with the ISO C99 standard. *)
 
 (** Relation between Boolean value and casting to [_Bool] type. *)
 
 Lemma cast_bool_bool_val:
   forall v t m,
-  match sem_cast v t (Tint IBool Signed noattr), bool_val v t m with
-  | Some v', Some b => v' = Val.of_bool b
-  | Some v', None => False
-  | None, _ => True
-  end.
-Proof.
+  sem_cast v t (Tint IBool Signed noattr) m =
+  match bool_val v t m with None => None | Some b => Some(Val.of_bool b) end.
   intros.
   assert (A: classify_bool t =
     match t with
@@ -1360,8 +1385,11 @@ Proof.
   destruct (Float32.cmp Ceq f0 Float32.zero); auto.
   destruct f; auto.
   destruct (Int.eq i Int.zero); auto.
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
   destruct (Int.eq i Int.zero); auto.
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
   destruct (Int.eq i Int.zero); auto.
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
 Qed.
 
 (** Relation between Boolean value and Boolean negation. *)
@@ -1376,6 +1404,119 @@ Proof.
   destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto.
 Qed.
 
+(** Properties of values obtained by casting to a given type. *)
+
+Inductive val_casted: val -> type -> Prop :=
+  | val_casted_int: forall sz si attr n,
+      cast_int_int sz si n = n ->
+      val_casted (Vint n) (Tint sz si attr)
+  | val_casted_float: forall attr n,
+       val_casted (Vfloat n) (Tfloat F64 attr)
+  | val_casted_single: forall attr n,
+       val_casted (Vsingle n) (Tfloat F32 attr)
+  | val_casted_long: forall si attr n,
+      val_casted (Vlong n) (Tlong si attr)
+  | val_casted_ptr_ptr: forall b ofs ty attr,
+      val_casted (Vptr b ofs) (Tpointer ty attr)
+  | val_casted_int_ptr: forall n ty attr,
+      val_casted (Vint n) (Tpointer ty attr)
+  | val_casted_ptr_int: forall b ofs si attr,
+      val_casted (Vptr b ofs) (Tint I32 si attr)
+  | val_casted_struct: forall id attr b ofs,
+      val_casted (Vptr b ofs) (Tstruct id attr)
+  | val_casted_union: forall id attr b ofs,
+      val_casted (Vptr b ofs) (Tunion id attr)
+  | val_casted_void: forall v,
+      val_casted v Tvoid.
+
+Remark cast_int_int_idem:
+  forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i.
+Proof.
+  intros. destruct sz; simpl; auto.
+  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
+  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
+  destruct (Int.eq i Int.zero); auto.
+Qed.
+
+Lemma cast_val_is_casted:
+  forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> val_casted v' ty'.
+Proof.
+  unfold sem_cast; intros. destruct ty'; simpl in *.
+- (* void *)
+  constructor.
+- (* int *)
+  destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H.
+  constructor. apply (cast_int_int_idem I8 s).
+  constructor. apply (cast_int_int_idem I8 s).
+  destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s).
+  destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s).
+  constructor. apply (cast_int_int_idem I16 s).
+  constructor. apply (cast_int_int_idem I16 s).
+  destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s).
+  destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s).
+  constructor. auto.
+  constructor.
+  constructor. auto.
+  destruct (cast_single_int s f); inv H1. constructor. auto.
+  destruct (cast_float_int s f); inv H1. constructor; auto.
+  constructor; auto.
+  constructor.
+  constructor; auto.
+  constructor.
+  constructor; auto.
+  constructor.
+  constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
+  constructor. simpl. destruct (Int64.eq i Int64.zero); auto.
+  constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto.
+  constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto.
+  constructor. simpl. destruct (Int.eq i Int.zero); auto.
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto.
+  constructor. simpl. destruct (Int.eq i Int.zero); auto.
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto.
+  constructor. simpl. destruct (Int.eq i Int.zero); auto.
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto.
+- (* long *)
+  destruct ty; try (destruct f); try discriminate.
+  destruct v; inv H. constructor.
+  destruct v; inv H. constructor.
+  destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor.
+  destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor.
+  destruct v; inv H. constructor.
+  destruct v; inv H. constructor.
+  destruct v; inv H. constructor.
+- (* float *)
+  destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor.
+- (* pointer *)
+  destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor.
+- (* array (impossible case) *)
+  discriminate.
+- (* function (impossible case) *)
+  discriminate.
+- (* structs *)
+  destruct ty; try discriminate; destruct v; try discriminate.
+  destruct (ident_eq i0 i); inv H; constructor.
+- (* unions *)
+  destruct ty; try discriminate; destruct v; try discriminate.
+  destruct (ident_eq i0 i); inv H; constructor.
+Qed.
+
+(** As a consequence, casting twice is equivalent to casting once. *)
+
+Lemma cast_val_casted:
+  forall v ty m, val_casted v ty -> sem_cast v ty ty m = Some v.
+Proof.
+  intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto.
+  destruct sz; congruence.
+  unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
+  unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
+Qed.
+
+Lemma cast_idempotent:
+  forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> sem_cast v' ty' ty' m = Some v'.
+Proof.
+  intros. apply cast_val_casted. eapply cast_val_is_casted; eauto.
+Qed.
+
 (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *)
 
 Module ArithConv.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 539b6826..30e6200d 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -187,12 +187,12 @@ Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement :=
 
 (** Extract the values from a list of function arguments *)
 
-Inductive cast_arguments: exprlist -> typelist -> list val -> Prop :=
+Inductive cast_arguments (m: mem): exprlist -> typelist -> list val -> Prop :=
   | cast_args_nil:
-      cast_arguments Enil Tnil nil
+      cast_arguments m Enil Tnil nil
   | cast_args_cons: forall v ty el targ1 targs v1 vl,
-      sem_cast v ty targ1 = Some v1 -> cast_arguments el targs vl ->
-      cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
+      sem_cast v ty targ1 m = Some v1 -> cast_arguments m el targs vl ->
+      cast_arguments m (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
 
 (** ** Reduction semantics for expressions *)
 
@@ -249,7 +249,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m
         E0 (Eval v ty) m
   | red_cast: forall ty v1 ty1 m v,
-      sem_cast v1 ty1 ty = Some v ->
+      sem_cast v1 ty1 ty m = Some v ->
       rred (Ecast (Eval v1 ty1) ty) m
         E0 (Eval v ty) m
   | red_seqand_true: forall v1 ty1 r2 ty m,
@@ -279,7 +279,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       rred (Ealignof ty1 ty) m
         E0 (Eval (Vint (Int.repr (alignof ge ty1))) ty) m
   | red_assign: forall b ofs ty1 v2 ty2 m v t m',
-      sem_cast v2 ty2 ty1 = Some v ->
+      sem_cast v2 ty2 ty1 m = Some v ->
       assign_loc ty1 m b ofs v t m' ->
       rred (Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty1) m
          t (Eval v ty1) m'
@@ -303,11 +303,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       rred (Ecomma (Eval v ty1) r2 ty) m
         E0 r2 m
   | red_paren: forall v1 ty1 ty2 ty m v,
-      sem_cast v1 ty1 ty2 = Some v ->
+      sem_cast v1 ty1 ty2 m = Some v ->
       rred (Eparen (Eval v1 ty1) ty2 ty) m
         E0 (Eval v ty) m
   | red_builtin: forall ef tyargs el ty m vargs t vres m',
-      cast_arguments el tyargs vargs ->
+      cast_arguments m el tyargs vargs ->
       external_call ef ge vargs m t vres m' ->
       rred (Ebuiltin ef tyargs el ty) m
          t (Eval vres ty) m'.
@@ -316,13 +316,13 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
 (** Head reduction for function calls.
     (More exactly, identification of function calls that can reduce.) *)
 
-Inductive callred: expr -> fundef -> list val -> type -> Prop :=
-  | red_call: forall vf tyf tyargs tyres cconv el ty fd vargs,
+Inductive callred: expr -> mem -> fundef -> list val -> type -> Prop :=
+  | red_call: forall vf tyf m tyargs tyres cconv el ty fd vargs,
       Genv.find_funct ge vf = Some fd ->
-      cast_arguments el tyargs vargs ->
+      cast_arguments m el tyargs vargs ->
       type_of_fundef fd = Tfunction tyargs tyres cconv ->
       classify_fun tyf = fun_case_f tyargs tyres cconv ->
-      callred (Ecall (Eval vf tyf) el ty)
+      callred (Ecall (Eval vf tyf) el ty) m
               fd vargs ty.
 
 (** Reduction contexts.  In accordance with C's nondeterministic semantics,
@@ -429,17 +429,14 @@ Inductive imm_safe: kind -> expr -> mem -> Prop :=
       context RV to C ->
       imm_safe to (C e) m
   | imm_safe_callred: forall to C e m fd args ty,
-      callred e fd args ty ->
+      callred e m fd args ty ->
       context RV to C ->
       imm_safe to (C e) m.
 
-(* An expression is not stuck if none of the potential redexes contained within
-   is immediately stuck. *)
-(*
 Definition not_stuck (e: expr) (m: mem) : Prop :=
   forall k C e' ,
-  context k RV C -> e = C e' -> not_imm_stuck k e' m.
-*)
+  context k RV C -> e = C e' -> imm_safe k e' m.
+
 End EXPR.
 
 (** ** Transition semantics. *)
@@ -597,7 +594,7 @@ Inductive estep: state -> trace -> state -> Prop :=
           t (ExprState f (C a') k e m')
 
   | step_call: forall C f a k e m fd vargs ty,
-      callred a fd vargs ty ->
+      callred a m fd vargs ty ->
       context RV RV C ->
       estep (ExprState f (C a) k e m)
          E0 (Callstate fd vargs (Kcall f e C ty k) m)
@@ -709,7 +706,7 @@ Inductive sstep: state -> trace -> state -> Prop :=
       sstep (State f (Sreturn (Some x)) k e m)
          E0 (ExprState f x (Kreturn k) e  m)
   | step_return_2:  forall f v1 ty k e m v2 m',
-      sem_cast v1 ty f.(fn_return) = Some v2 ->
+      sem_cast v1 ty f.(fn_return) m = Some v2 ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
       sstep (ExprState f (Eval v1 ty) (Kreturn k) e m)
          E0 (Returnstate v2 (call_cont k) m')
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 825a563c..40b51bd3 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -20,17 +20,9 @@
    Csharpminor's simpler control structures.
 *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
-Require Import Cminor.
-Require Import Csharpminor.
+Require Import Coqlib Maps Errors Integers Floats.
+Require Import AST Linking.
+Require Import Ctypes Cop Clight Cminor Csharpminor.
 
 Open Local Scope string_scope.
 Open Local Scope error_monad_scope.
@@ -125,6 +117,18 @@ Definition make_cmp_ne_zero (e: expr) :=
   | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero)
   end.
 
+(** Variants of [sizeof] and [alignof] that check that the given type is complete. *)
+
+Definition sizeof (ce: composite_env) (t: type) : res Z :=
+  if complete_type ce t
+  then OK (Ctypes.sizeof ce t)
+  else Error (msg "incomplete type").
+
+Definition alignof (ce: composite_env) (t: type) : res Z :=
+  if complete_type ce t
+  then OK (Ctypes.alignof ce t)
+  else Error (msg "incomplete type").
+
 (** [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]. *)
 
@@ -238,16 +242,20 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation)
 Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
   | add_case_pi ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e1 (Ebinop Omul n e2))
   | add_case_ip ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e2 (Ebinop Omul n e1))
   | add_case_pl ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | add_case_lp ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1)))
   | add_default =>
       make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2
@@ -256,13 +264,16 @@ Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2:
 Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_sub ty1 ty2 with
   | sub_case_pi ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
   | sub_case_pl ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | sub_default =>
       make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2
@@ -351,8 +362,9 @@ Definition make_load (addr: expr) (ty_res: type) :=
   by-copy assignment of a value of Clight type [ty]. *)
 
 Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) :=
-  Sbuiltin None (EF_memcpy (Ctypes.sizeof ce ty) (Ctypes.alignof_blockcopy ce ty))
-                (dst :: src :: nil).
+  do sz <- sizeof ce ty;
+  OK (Sbuiltin None (EF_memcpy sz (Ctypes.alignof_blockcopy ce ty))
+                    (dst :: src :: nil)).
 
 (** [make_store addr ty rhs] stores the value of the
    Csharpminor expression [rhs] into the memory location denoted by the
@@ -362,7 +374,7 @@ Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) :=
 Definition make_store (ce: composite_env) (addr: expr) (ty: type) (rhs: expr) :=
   match access_mode ty with
   | By_value chunk => OK (Sstore chunk addr rhs)
-  | By_copy => OK (make_memcpy ce addr rhs ty)
+  | By_copy => make_memcpy ce addr rhs ty
   | _ => Error (msg "Cshmgen.make_store")
   end.
 
@@ -457,9 +469,9 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr
       do addr <- make_field_access ce (typeof b) i tb;
       make_load addr ty
   | Clight.Esizeof ty' ty =>
-      OK(make_intconst (Int.repr (sizeof ce ty')))
+      do sz <- sizeof ce ty'; OK(make_intconst (Int.repr sz))
   | Clight.Ealignof ty' ty =>
-      OK(make_intconst (Int.repr (alignof ce ty')))
+      do al <- alignof ce ty'; OK(make_intconst (Int.repr al))
   end
 
 (** [transl_lvalue a] returns the Csharpminor code that evaluates
@@ -621,7 +633,8 @@ with transl_lbl_stmt (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
 
 (*** Translation of functions *)
 
-Definition transl_var (ce: composite_env) (v: ident * type) := (fst v, sizeof ce (snd v)).
+Definition transl_var (ce: composite_env) (v: ident * type) :=
+  do sz <- sizeof ce (snd v); OK (fst v, sz).
 
 Definition signature_of_function (f: Clight.function) :=
   {| sig_args := map typ_of_type (map snd (Clight.fn_params f));
@@ -630,18 +643,19 @@ Definition signature_of_function (f: Clight.function) :=
 
 Definition transl_function (ce: composite_env) (f: Clight.function) : res function :=
   do tbody <- transl_statement ce f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f);
+  do tvars <- mmap (transl_var ce) (Clight.fn_vars f);
   OK (mkfunction
        (signature_of_function f)
        (map fst (Clight.fn_params f))
-       (map (transl_var ce) (Clight.fn_vars f))
+       tvars
        (map fst (Clight.fn_temps f))
        tbody).
 
-Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef :=
+Definition transl_fundef (ce: composite_env) (id: ident) (f: Clight.fundef) : res fundef :=
   match f with
-  | Clight.Internal g =>
+  | Internal g =>
       do tg <- transl_function ce g; OK(AST.Internal tg)
-  | Clight.External ef args res cconv =>
+  | External ef args res cconv =>
       if signature_eq (ef_sig ef) (signature_of_type args res cconv)
       then OK(AST.External ef)
       else Error(msg "Cshmgen.transl_fundef: wrong external signature")
@@ -649,7 +663,7 @@ Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef :=
 
 (** ** Translation of programs *)
 
-Definition transl_globvar (ty: type) := OK tt.
+Definition transl_globvar (id: ident) (ty: type) := OK tt.
 
 Definition transl_program (p: Clight.program) : res program :=
   transform_partial_program2 (transl_fundef p.(prog_comp_env)) transl_globvar p.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index e25e21c9..8bc97b99 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -12,24 +12,40 @@
 
 (** * Correctness of the translation from Clight to C#minor. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import AST.
-Require Import Values.
-Require Import Events.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
-Require Import Cminor.
-Require Import Csharpminor.
+Require Import Coqlib Errors Maps Integers Floats.
+Require Import AST Linking.
+Require Import Values Events Memory Globalenvs Smallstep.
+Require Import Ctypes Cop Clight Cminor Csharpminor.
 Require Import Cshmgen.
 
+(** * Relational specification of the transformation *)
+
+Inductive match_fundef (p: Clight.program) : Clight.fundef -> Csharpminor.fundef -> Prop :=
+  | match_fundef_internal: forall f tf,
+      transl_function p.(prog_comp_env) f = OK tf ->
+      match_fundef p (Ctypes.Internal f) (AST.Internal tf)
+  | match_fundef_external: forall ef args res cc,
+      ef_sig ef = signature_of_type args res cc ->
+      match_fundef p (Ctypes.External ef args res cc) (AST.External ef).
+
+Definition match_varinfo (v: type) (tv: unit) := True.
+
+Definition match_prog (p: Clight.program) (tp: Csharpminor.program) : Prop :=
+  match_program_gen match_fundef match_varinfo p p tp.
+
+Lemma transf_program_match:
+  forall p tp, transl_program p = OK tp -> match_prog p tp.
+Proof.
+  unfold transl_program; intros.
+  eapply match_transform_partial_program2. 
+  eexact H.
+- intros. destruct f; simpl in H0.
++ monadInv H0. constructor; auto.
++ destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H0.
+  constructor; auto.
+- intros; red; auto.
+Qed.
+
 (** * Properties of operations over types *)
 
 Remark transl_params_types:
@@ -41,21 +57,20 @@ Qed.
 
 Lemma transl_fundef_sig1:
   forall ce f tf args res cc,
-  transl_fundef ce f = OK tf ->
+  match_fundef ce f tf ->
   classify_fun (type_of_fundef f) = fun_case_f args res cc ->
   funsig tf = signature_of_type args res cc.
 Proof.
-  intros. destruct f; simpl in *.
-  monadInv H. monadInv EQ. simpl. inversion H0.
+  intros. inv H.
+- monadInv H1. simpl. inversion H0.
   unfold signature_of_function, signature_of_type.
   f_equal. apply transl_params_types.
-  destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H.
-  simpl. congruence.
+- simpl in H0. unfold funsig. congruence.
 Qed.
 
 Lemma transl_fundef_sig2:
   forall ce f tf args res cc,
-  transl_fundef ce f = OK tf ->
+  match_fundef ce f tf ->
   type_of_fundef f = Tfunction args res cc ->
   funsig tf = signature_of_type args res cc.
 Proof.
@@ -63,15 +78,73 @@ Proof.
   rewrite H0; reflexivity.
 Qed.
 
+Lemma transl_sizeof:
+  forall (cunit prog: Clight.program) t sz,
+  linkorder cunit prog ->
+  sizeof cunit.(prog_comp_env) t = OK sz ->
+  sz = Ctypes.sizeof prog.(prog_comp_env) t.
+Proof.
+  intros. destruct H.
+  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
+  symmetry. apply Ctypes.sizeof_stable; auto.
+Qed.
+
+Lemma transl_alignof:
+  forall (cunit prog: Clight.program) t al,
+  linkorder cunit prog ->
+  alignof cunit.(prog_comp_env) t = OK al ->
+  al = Ctypes.alignof prog.(prog_comp_env) t.
+Proof.
+  intros. destruct H.
+  unfold alignof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
+  symmetry. apply Ctypes.alignof_stable; auto.
+Qed.
+
+Lemma transl_alignof_blockcopy:
+  forall (cunit prog: Clight.program) t sz,
+  linkorder cunit prog ->
+  sizeof cunit.(prog_comp_env) t = OK sz ->
+  sz = Ctypes.sizeof prog.(prog_comp_env) t /\
+  alignof_blockcopy cunit.(prog_comp_env) t = alignof_blockcopy prog.(prog_comp_env) t.
+Proof.
+  intros. destruct H.
+  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
+  split. 
+- symmetry. apply Ctypes.sizeof_stable; auto.
+- revert C. induction t; simpl; auto;
+  destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto.
+Qed.
+
+Lemma field_offset_stable:
+  forall (cunit prog: Clight.program) id co f,
+  linkorder cunit prog ->
+  cunit.(prog_comp_env)!id = Some co ->
+  prog.(prog_comp_env)!id = Some co /\ 
+  field_offset prog.(prog_comp_env) f (co_members co) = field_offset cunit.(prog_comp_env) f (co_members co).
+Proof.
+  intros. 
+  assert (C: composite_consistent cunit.(prog_comp_env) co).
+  { apply build_composite_env_consistent with cunit.(prog_types) id; auto.
+    apply prog_comp_env_eq. }
+  destruct H as [_ A].
+  split. auto. generalize (co_consistent_complete _ _ C).
+  unfold field_offset. generalize 0. induction (co_members co) as [ | [f1 t1] m]; simpl; intros.
+- auto.
+- InvBooleans.
+  rewrite ! (alignof_stable _ _ A) by auto.
+  rewrite ! (sizeof_stable _ _ A) by auto.
+  destruct (ident_eq f f1); eauto.
+Qed. 
+
 (** * Properties of the translation functions *)
 
 (** Transformation of expressions and statements. *)
 
 Lemma transl_expr_lvalue:
-  forall ge e le m a loc ofs ta,
+  forall ge e le m a loc ofs ce ta,
   Clight.eval_lvalue ge e le m a loc ofs ->
-  transl_expr ge a = OK ta ->
-  (exists tb, transl_lvalue ge a = OK tb /\ make_load tb (typeof a) = OK ta).
+  transl_expr ce a = OK ta ->
+  (exists tb, transl_lvalue ce a = OK tb /\ make_load tb (typeof a) = OK ta).
 Proof.
   intros until ta; intros EVAL TR. inv EVAL; simpl in TR.
   (* var local *)
@@ -140,7 +213,8 @@ Qed.
 
 Section CONSTRUCTORS.
 
-Variable ce: composite_env.
+Variables cunit prog: Clight.program.
+Hypothesis LINK: linkorder cunit prog.
 Variable ge: genv.
 
 Lemma make_intconst_correct:
@@ -255,7 +329,7 @@ Lemma make_cast_correct:
   forall e le m a b v ty1 ty2 v',
   make_cast ty1 ty2 a = OK b ->
   eval_expr ge e le m a v ->
-  sem_cast v ty1 ty2 = Some v' ->
+  sem_cast v ty1 ty2 m = Some v' ->
   eval_expr ge e le m b v'.
 Proof.
   intros. unfold make_cast, sem_cast in *;
@@ -302,6 +376,12 @@ Proof.
   econstructor; eauto with cshm.
   simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
   destruct (Int.eq i Int.zero); auto.
+  (* pointer -> bool *)
+  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:VALID; inv H2.
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmpu. simpl. rewrite Int.eq_true.
+  unfold Mem.weak_valid_pointer in VALID; rewrite VALID. 
+  auto.
   (* struct *)
   destruct (ident_eq id1 id2); inv H2; auto.
   (* union *)
@@ -394,6 +474,16 @@ Qed.
 
 Definition binary_constructor_correct
     (make: expr -> type -> expr -> type -> res expr)
+    (sem: val -> type -> val -> type -> mem -> option val): Prop :=
+  forall a tya b tyb c va vb v e le m,
+  sem va tya vb tyb m = Some v ->
+  make a tya b tyb = OK c ->
+  eval_expr ge e le m a va ->
+  eval_expr ge e le m b vb ->
+  eval_expr ge e le m c v.
+
+Definition shift_constructor_correct
+    (make: expr -> type -> expr -> type -> res expr)
     (sem: val -> type -> val -> type -> option val): Prop :=
   forall a tya b tyb c va vb v e le m,
   sem va tya vb tyb = Some v ->
@@ -433,8 +523,8 @@ Proof.
   set (cls := classify_binarith tya tyb) in *.
   set (ty := binarith_type cls) in *.
   monadInv MAKE.
-  destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate.
-  destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate.
+  destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate.
+  destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate.
   exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
   exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
   destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
@@ -456,8 +546,8 @@ Proof.
   set (cls := classify_binarith tya tyb) in *.
   set (ty := binarith_type cls) in *.
   monadInv MAKE.
-  destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate.
-  destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate.
+  destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate.
+  destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate.
   exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
   exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
   destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
@@ -471,27 +561,33 @@ End MAKE_BIN.
 
 Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
 
-Lemma make_add_correct: binary_constructor_correct (make_add ce) (sem_add ce).
+Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
 Proof.
   red; unfold make_add, sem_add;
   intros until m; intros SEM MAKE EV1 EV2;
-  destruct (classify_add tya tyb); inv MAKE.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+  destruct (classify_add tya tyb); try (monadInv MAKE).
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
-Lemma make_sub_correct: binary_constructor_correct (make_sub ce) (sem_sub ce).
+Lemma make_sub_correct: binary_constructor_correct (make_sub cunit.(prog_comp_env)) (sem_sub prog.(prog_comp_env)).
 Proof.
   red; unfold make_sub, sem_sub;
   intros until m; intros SEM MAKE EV1 EV2;
-  destruct (classify_sub tya tyb); inv MAKE.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM.
+  destruct (classify_sub tya tyb); try (monadInv MAKE).
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM.
   destruct (eq_block b0 b1); try discriminate.
-  set (sz := sizeof ce ty) in *.
+  set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *.
   destruct (zlt 0 sz); try discriminate.
   destruct (zle sz Int.max_signed); simpl in H0; inv H0.
   econstructor; eauto with cshm.
@@ -503,7 +599,8 @@ Proof.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
   rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction.
   rewrite andb_false_r; auto.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -578,7 +675,7 @@ Proof.
   apply Int64.unsigned_repr. comput Int64.max_unsigned; omega.
 Qed.
 
-Lemma make_shl_correct: binary_constructor_correct make_shl sem_shl.
+Lemma make_shl_correct: shift_constructor_correct make_shl sem_shl.
 Proof.
   red; unfold make_shl, sem_shl, sem_shift;
   intros until m; intros SEM MAKE EV1 EV2;
@@ -597,7 +694,7 @@ Proof.
   unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto.
 Qed.
 
-Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr.
+Lemma make_shr_correct: shift_constructor_correct make_shr sem_shr.
 Proof.
   red; unfold make_shr, sem_shr, sem_shift;
   intros until m; intros SEM MAKE EV1 EV2;
@@ -619,15 +716,9 @@ Proof.
   unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto.
 Qed.
 
-Lemma make_cmp_correct:
-  forall cmp a tya b tyb c va vb v e le m,
-  sem_cmp cmp va tya vb tyb m = Some v ->
-  make_cmp cmp a tya b tyb = OK c ->
-  eval_expr ge e le m a va ->
-  eval_expr ge e le m b vb ->
-  eval_expr ge e le m c v.
+Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp).
 Proof.
-  unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2;
+  red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2;
   destruct (classify_cmp tya tyb).
 - inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
   simpl in SEM; inv SEM.
@@ -663,8 +754,8 @@ Qed.
 
 Lemma transl_binop_correct:
   forall op a tya b tyb c va vb v e le m,
-  transl_binop ce op a tya b tyb = OK c ->
-  sem_binary_operation ce op va tya vb tyb m = Some v ->
+  transl_binop cunit.(prog_comp_env) op a tya b tyb = OK c ->
+  sem_binary_operation prog.(prog_comp_env) op va tya vb tyb m = Some v ->
   eval_expr ge e le m a va ->
   eval_expr ge e le m b vb ->
   eval_expr ge e le m c v.
@@ -706,15 +797,18 @@ Proof.
 Qed.
 
 Lemma make_memcpy_correct:
-  forall ce f dst src ty k e le m b ofs v m',
+  forall f dst src ty k e le m b ofs v m' s,
   eval_expr ge e le m dst (Vptr b ofs) ->
   eval_expr ge e le m src v ->
-  assign_loc ce ty m b ofs v m' ->
+  assign_loc prog.(prog_comp_env) ty m b ofs v m' ->
   access_mode ty = By_copy ->
-  step ge (State f (make_memcpy ce dst src ty) k e le m) E0 (State f Sskip k e le m').
+  make_memcpy cunit.(prog_comp_env) dst src ty = OK s ->
+  step ge (State f s k e le m) E0 (State f Sskip k e le m').
 Proof.
   intros. inv H1; try congruence.
-  unfold make_memcpy. change le with (set_optvar None Vundef le) at 2.
+  monadInv H3. 
+  exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B.
+  change le with (set_optvar None Vundef le) at 2.
   econstructor.
   econstructor. eauto. econstructor. eauto. constructor.
   econstructor; eauto.
@@ -725,10 +819,10 @@ Qed.
 
 Lemma make_store_correct:
   forall addr ty rhs code e le m b ofs v m' f k,
-  make_store ce addr ty rhs = OK code ->
+  make_store cunit.(prog_comp_env) addr ty rhs = OK code ->
   eval_expr ge e le m addr (Vptr b ofs) ->
   eval_expr ge e le m rhs v ->
-  assign_loc ce ty m b ofs v m' ->
+  assign_loc prog.(prog_comp_env) ty m b ofs v m' ->
   step ge (State f code k e le m) E0 (State f Sskip k e le m').
 Proof.
   unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN.
@@ -737,8 +831,8 @@ Proof.
   rewrite H in MKSTORE; inv MKSTORE.
   econstructor; eauto.
   (* by copy *)
-  rewrite H in MKSTORE; inv MKSTORE.
-  eapply make_memcpy_correct; eauto.
+  rewrite H in MKSTORE.
+  eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto.
 Qed.
 
 End CONSTRUCTORS.
@@ -749,34 +843,30 @@ Section CORRECTNESS.
 
 Variable prog: Clight.program.
 Variable tprog: Csharpminor.program.
-Hypothesis TRANSL: transl_program prog = OK tprog.
+Hypothesis TRANSL: match_prog prog tprog.
 
 Let ge := globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
+Proof (Genv.find_symbol_match TRANSL).
 
-Lemma public_preserved:
-  forall s, Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof (Genv.public_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  exists cu tf, Genv.find_funct_ptr tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
+Proof (Genv.find_funct_ptr_match TRANSL).
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
-  exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef ge f = OK tf.
-Proof (Genv.find_funct_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
-
-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 ge f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
-
-Lemma block_is_volatile_preserved:
-  forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b.
-Proof (Genv.block_is_volatile_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
+  exists cu tf, Genv.find_funct tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
+Proof (Genv.find_funct_match TRANSL).
 
 (** * Matching between environments *)
 
@@ -787,7 +877,7 @@ Record match_env (e: Clight.env) (te: Csharpminor.env) : Prop :=
   mk_match_env {
     me_local:
       forall id b ty,
-      e!id = Some (b, ty) -> te!id = Some(b, sizeof ge ty);
+      e!id = Some (b, ty) -> te!id = Some(b, Ctypes.sizeof ge ty);
     me_local_inv:
       forall id b sz,
       te!id = Some (b, sz) -> exists ty, e!id = Some(b, ty)
@@ -811,13 +901,13 @@ Proof.
   intros.
   set (R := fun (x: (block * type)) (y: (block * Z)) =>
          match x, y with
-         | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ge ty
+         | (b1, ty), (b2, sz) => b2 = b1 /\ sz = Ctypes.sizeof ge ty
          end).
   assert (list_forall2
             (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
             (PTree.elements e) (PTree.elements te)).
   apply PTree.elements_canonical_order.
-  intros id [b ty] GET. exists (b, sizeof ge ty); split. eapply me_local; eauto. red; auto.
+  intros id [b ty] GET. exists (b, Ctypes.sizeof ge ty); split. eapply me_local; eauto. red; auto.
   intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ].
   exploit me_local; eauto. intros EQ1.
   exists (b, ty); split. auto. red; split; congruence.
@@ -853,17 +943,21 @@ Qed.
   local variables and initialization of the parameters. *)
 
 Lemma match_env_alloc_variables:
-  forall e1 m1 vars e2 m2,
-  Clight.alloc_variables ge e1 m1 vars e2 m2 ->
-  forall te1,
+  forall cunit, linkorder cunit prog ->
+  forall e1 m1 vars e2 m2, Clight.alloc_variables ge e1 m1 vars e2 m2 ->
+  forall tvars te1,
+  mmap (transl_var cunit.(prog_comp_env)) vars = OK tvars ->
   match_env e1 te1 ->
   exists te2,
-  Csharpminor.alloc_variables te1 m1 (map (transl_var ge) vars) te2 m2
+  Csharpminor.alloc_variables te1 m1 tvars te2 m2
   /\ match_env e2 te2.
 Proof.
-  induction 1; intros; simpl.
-  exists te1; split. constructor. auto.
-  exploit (IHalloc_variables (PTree.set id (b1, sizeof ge ty) te1)).
+  induction 2; simpl; intros.
+- inv H0. exists te1; split. constructor. auto.
+- monadInv H2. monadInv EQ. simpl in *. 
+  exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ. 
+  exploit (IHalloc_variables x0 (PTree.set id (b1, Ctypes.sizeof ge ty) te1)).
+  auto.
   constructor.
     (* me_local *)
     intros until ty0. repeat rewrite PTree.gsspec.
@@ -893,6 +987,16 @@ Proof.
   destruct a as [id ty]. destruct vals; try discriminate. auto.
 Qed.
 
+Lemma transl_vars_names:
+  forall ce vars tvars,
+  mmap (transl_var ce) vars = OK tvars ->
+  map fst tvars = var_names vars.
+Proof.
+  intros. exploit mmap_inversion; eauto. generalize vars tvars. induction 1; simpl.
+- auto.
+- monadInv H0. simpl; congruence.
+Qed.
+
 (** * Proof of semantic preservation *)
 
 (** ** Semantic preservation for expressions *)
@@ -919,6 +1023,8 @@ Qed.
 
 Section EXPR.
 
+Variable cunit: Clight.program.
+Hypothesis LINK: linkorder cunit prog.
 Variable e: Clight.env.
 Variable le: temp_env.
 Variable m: mem.
@@ -928,11 +1034,11 @@ Hypothesis MENV: match_env e te.
 Lemma transl_expr_lvalue_correct:
   (forall a v,
    Clight.eval_expr ge e le m a v ->
-   forall ta (TR: transl_expr ge a = OK ta) ,
+   forall ta (TR: transl_expr cunit.(prog_comp_env) a = OK ta) ,
    Csharpminor.eval_expr tge te le m ta v)
 /\(forall a b ofs,
    Clight.eval_lvalue ge e le m a b ofs ->
-   forall ta (TR: transl_lvalue ge a = OK ta),
+   forall ta (TR: transl_lvalue cunit.(prog_comp_env) a = OK ta),
    Csharpminor.eval_expr tge te le m ta (Vptr b ofs)).
 Proof.
   apply eval_expr_lvalue_ind; intros; try (monadInv TR).
@@ -955,9 +1061,9 @@ Proof.
 (* cast *)
   eapply make_cast_correct; eauto.
 (* sizeof *)
-  apply make_intconst_correct.
+  rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_intconst_correct.
 (* alignof *)
-  apply make_intconst_correct.
+  rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_intconst_correct.
 (* rvalue out of lvalue *)
   exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]].
   eapply make_load_correct; eauto.
@@ -971,11 +1077,13 @@ Proof.
 (* deref *)
   simpl in TR. eauto.
 (* field struct *)
-  change (prog_comp_env prog) with (genv_cenv ge) in EQ0.
-  unfold make_field_access in EQ0; rewrite H1, H2 in EQ0; monadInv EQ0.
+  unfold make_field_access in EQ0. rewrite H1 in EQ0. 
+  destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0.
+  exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
+  rewrite <- B in EQ1. 
   eapply eval_Ebinop; eauto.
   apply make_intconst_correct.
-  simpl. congruence.
+  simpl. unfold ge in *; simpl in *. congruence.
 (* field union *)
   unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0.
   auto.
@@ -984,21 +1092,21 @@ Qed.
 Lemma transl_expr_correct:
    forall a v,
    Clight.eval_expr ge e le m a v ->
-   forall ta, transl_expr ge a = OK ta ->
+   forall ta, transl_expr cunit.(prog_comp_env) a = OK ta ->
    Csharpminor.eval_expr tge te le m ta v.
 Proof (proj1 transl_expr_lvalue_correct).
 
 Lemma transl_lvalue_correct:
    forall a b ofs,
    Clight.eval_lvalue ge e le m a b ofs ->
-   forall ta, transl_lvalue ge a = OK ta ->
+   forall ta, transl_lvalue cunit.(prog_comp_env) a = OK ta ->
    Csharpminor.eval_expr tge te le m ta (Vptr b ofs).
 Proof (proj2 transl_expr_lvalue_correct).
 
 Lemma transl_arglist_correct:
   forall al tyl vl,
   Clight.eval_exprlist ge e le m al tyl vl ->
-  forall tal, transl_arglist ge al tyl = OK tal ->
+  forall tal, transl_arglist cunit.(prog_comp_env) al tyl = OK tal ->
   Csharpminor.eval_exprlist tge te le m tal vl.
 Proof.
   induction 1; intros.
@@ -1052,71 +1160,75 @@ Proof.
   apply star_refl.
 Qed.
 
-Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> Prop :=
-  | match_Kstop: forall tyret nbrk ncnt,
-      match_cont tyret nbrk ncnt Clight.Kstop Kstop
-  | match_Kseq: forall tyret nbrk ncnt s k ts tk,
-      transl_statement ge tyret nbrk ncnt s = OK ts ->
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret nbrk ncnt
+Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> Prop :=
+  | match_Kstop: forall ce tyret nbrk ncnt,
+      match_cont tyret ce nbrk ncnt Clight.Kstop Kstop
+  | match_Kseq: forall ce tyret nbrk ncnt s k ts tk,
+      transl_statement ce tyret nbrk ncnt s = OK ts ->
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret nbrk ncnt
                  (Clight.Kseq s k)
                  (Kseq ts tk)
-  | match_Kloop1: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
-      transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 ->
-      transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 ->
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret 1%nat 0%nat
+  | match_Kloop1: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
+      transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 ->
+      transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 ->
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret 1%nat 0%nat
                  (Clight.Kloop1 s1 s2 k)
                  (Kblock (Kseq ts2 (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk))))
-  | match_Kloop2: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
-      transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 ->
-      transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 ->
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret 0%nat (S ncnt)
+  | match_Kloop2: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
+      transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 ->
+      transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 ->
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret 0%nat (S ncnt)
                  (Clight.Kloop2 s1 s2 k)
                  (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk))
-  | match_Kswitch: forall tyret nbrk ncnt k tk,
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret 0%nat (S ncnt)
+  | match_Kswitch: forall ce tyret nbrk ncnt k tk,
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret 0%nat (S ncnt)
                  (Clight.Kswitch k)
                  (Kblock tk)
-  | match_Kcall_some: forall tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk,
-      transl_function ge f = OK tf ->
+  | match_Kcall: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk cu,
+      linkorder cu prog ->
+      transl_function cu.(prog_comp_env) f = OK tf ->
       match_env e te ->
-      match_cont (Clight.fn_return f) nbrk' ncnt' k tk ->
-      match_cont tyret nbrk ncnt
+      match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk ->
+      match_cont ce tyret nbrk ncnt
                  (Clight.Kcall id f e le k)
                  (Kcall id tf te le tk).
 
 Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
   | match_state:
-      forall f nbrk ncnt s k e le m tf ts tk te ts' tk'
-          (TRF: transl_function ge f = OK tf)
-          (TR: transl_statement ge (Clight.fn_return f) nbrk ncnt s = OK ts)
+      forall f nbrk ncnt s k e le m tf ts tk te ts' tk' cu
+          (LINK: linkorder cu prog)
+          (TRF: transl_function cu.(prog_comp_env) f = OK tf)
+          (TR: transl_statement cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt s = OK ts)
           (MTR: match_transl ts tk ts' tk')
           (MENV: match_env e te)
-          (MK: match_cont (Clight.fn_return f) nbrk ncnt k tk),
+          (MK: match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk),
       match_states (Clight.State f s k e le m)
                    (State tf ts' tk' te le m)
   | match_callstate:
-      forall fd args k m tfd tk targs tres cconv
-          (TR: transl_fundef ge fd = OK tfd)
-          (MK: match_cont Tvoid 0%nat 0%nat k tk)
+      forall fd args k m tfd tk targs tres cconv cu ce
+          (LINK: linkorder cu prog)
+          (TR: match_fundef cu fd tfd)
+          (MK: match_cont ce Tvoid 0%nat 0%nat k tk)
           (ISCC: Clight.is_call_cont k)
           (TY: type_of_fundef fd = Tfunction targs tres cconv),
       match_states (Clight.Callstate fd args k m)
                    (Callstate tfd args tk m)
   | match_returnstate:
-      forall res k m tk
-          (MK: match_cont Tvoid 0%nat 0%nat k tk),
+      forall res k m tk ce
+          (MK: match_cont ce Tvoid 0%nat 0%nat k tk),
       match_states (Clight.Returnstate res k m)
                    (Returnstate res tk m).
 
 Remark match_states_skip:
-  forall f e le te nbrk ncnt k tf tk m,
-  transl_function ge f = OK tf ->
+  forall f e le te nbrk ncnt k tf tk m cu,
+  linkorder cu prog ->
+  transl_function cu.(prog_comp_env) f = OK tf ->
   match_env e te ->
-  match_cont (Clight.fn_return f) nbrk ncnt k tk ->
+  match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk ->
   match_states (Clight.State f Clight.Sskip k e le m) (State tf Sskip tk te le m).
 Proof.
   intros. econstructor; eauto. simpl; reflexivity. constructor.
@@ -1125,89 +1237,90 @@ Qed.
 (** Commutation between label resolution and compilation *)
 
 Section FIND_LABEL.
+Variable ce: composite_env.
 Variable lbl: label.
 Variable tyret: type.
 
 Lemma transl_find_label:
   forall s nbrk ncnt k ts tk
-  (TR: transl_statement ge tyret nbrk ncnt s = OK ts)
-  (MC: match_cont tyret nbrk ncnt k tk),
+  (TR: transl_statement ce tyret nbrk ncnt s = OK ts)
+  (MC: match_cont ce tyret nbrk ncnt k tk),
   match Clight.find_label lbl s k with
   | None => find_label lbl ts tk = None
   | Some (s', k') =>
       exists ts', exists tk', exists nbrk', exists ncnt',
       find_label lbl ts tk = Some (ts', tk')
-      /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts'
-      /\ match_cont tyret nbrk' ncnt' k' tk'
+      /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts'
+      /\ match_cont ce tyret nbrk' ncnt' k' tk'
   end
 
 with transl_find_label_ls:
   forall ls nbrk ncnt k tls tk
-  (TR: transl_lbl_stmt ge tyret nbrk ncnt ls = OK tls)
-  (MC: match_cont tyret nbrk ncnt k tk),
+  (TR: transl_lbl_stmt ce tyret nbrk ncnt ls = OK tls)
+  (MC: match_cont ce tyret nbrk ncnt k tk),
   match Clight.find_label_ls lbl ls k with
   | None => find_label_ls lbl tls tk = None
   | Some (s', k') =>
       exists ts', exists tk', exists nbrk', exists ncnt',
       find_label_ls lbl tls tk = Some (ts', tk')
-      /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts'
-      /\ match_cont tyret nbrk' ncnt' k' tk'
+      /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts'
+      /\ match_cont ce tyret nbrk' ncnt' k' tk'
   end.
 
 Proof.
-  intro s; case s; intros; try (monadInv TR); simpl.
-(* skip *)
+* intro s; case s; intros; try (monadInv TR); simpl.
+- (* skip *)
   auto.
-(* assign *)
+- (* assign *)
   unfold make_store, make_memcpy in EQ3.
-  destruct (access_mode (typeof e)); inv EQ3; auto.
-(* set *)
+  destruct (access_mode (typeof e)); monadInv EQ3; auto.
+- (* set *)
   auto.
-(* call *)
+- (* call *)
   simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto.
-(* builtin *)
+- (* builtin *)
   auto.
-(* seq *)
+- (* seq *)
   exploit (transl_find_label s0 nbrk ncnt (Clight.Kseq s1 k)); eauto. constructor; eauto.
   destruct (Clight.find_label lbl s0 (Clight.Kseq s1 k)) as [[s' k'] | ].
   intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
   rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
   intro. rewrite H. eapply transl_find_label; eauto.
-(* ifthenelse *)
+- (* ifthenelse *)
   exploit (transl_find_label s0); eauto.
   destruct (Clight.find_label lbl s0 k) as [[s' k'] | ].
   intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
   rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
   intro. rewrite H. eapply transl_find_label; eauto.
-(* loop *)
+- (* loop *)
   exploit (transl_find_label s0 1%nat 0%nat (Kloop1 s0 s1 k)); eauto. econstructor; eauto.
   destruct (Clight.find_label lbl s0 (Kloop1 s0 s1 k)) as [[s' k'] | ].
   intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
   rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
   intro. rewrite H.
   eapply transl_find_label; eauto. econstructor; eauto.
-(* break *)
+- (* break *)
   auto.
-(* continue *)
+- (* continue *)
   auto.
-(* return *)
+- (* return *)
   simpl in TR. destruct o; monadInv TR. auto. auto.
-(* switch *)
+- (* switch *)
   assert (exists b, ts = Sblock (Sswitch b x x0)).
   { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. }
   destruct H as [b EQ3]; rewrite EQ3; simpl.
   eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto.
-(* label *)
+- (* label *)
   destruct (ident_eq lbl l).
   exists x; exists tk; exists nbrk; exists ncnt; auto.
   eapply transl_find_label; eauto.
-(* goto *)
+- (* goto *)
   auto.
 
-  intro ls; case ls; intros; monadInv TR; simpl.
-(* nil *)
+* intro ls; case ls; intros; monadInv TR; simpl.
+- (* nil *)
   auto.
-(* cons *)
+- (* cons *)
   exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto.
   econstructor; eauto. apply transl_lbl_stmt_2; eauto.
   destruct (Clight.find_label lbl s (Clight.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ].
@@ -1222,9 +1335,9 @@ End FIND_LABEL.
 (** Properties of call continuations *)
 
 Lemma match_cont_call_cont:
-  forall tyret' nbrk' ncnt' tyret nbrk ncnt k tk,
-  match_cont tyret nbrk ncnt k tk ->
-  match_cont tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
+  forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk,
+  match_cont ce tyret nbrk ncnt k tk ->
+  match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
 Proof.
   induction 1; simpl; auto.
   constructor.
@@ -1232,10 +1345,10 @@ Proof.
 Qed.
 
 Lemma match_cont_is_call_cont:
-  forall tyret nbrk ncnt k tk tyret' nbrk' ncnt',
-  match_cont tyret nbrk ncnt k tk ->
+  forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt',
+  match_cont ce tyret nbrk ncnt k tk ->
   Clight.is_call_cont k ->
-  match_cont tyret' nbrk' ncnt' k tk /\ is_call_cont tk.
+  match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk.
 Proof.
   intros. inv H; simpl in H0; try contradiction; simpl.
   split; auto; constructor.
@@ -1251,11 +1364,12 @@ Lemma transl_step:
 Proof.
   induction 1; intros T1 MST; inv MST.
 
-(* assign *)
+- (* assign *)
   monadInv TR.
   assert (SAME: ts' = ts /\ tk' = tk).
-    inversion MTR. auto.
-    subst ts. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof a1)); congruence.
+  { inversion MTR. auto.
+    subst ts. unfold make_store, make_memcpy in EQ3.
+    destruct (access_mode (typeof a1)); monadInv EQ3; auto. }
   destruct SAME; subst ts' tk'.
   econstructor; split.
   apply plus_one. eapply make_store_correct; eauto.
@@ -1263,62 +1377,61 @@ Proof.
   eapply transl_expr_correct; eauto.
   eapply match_states_skip; eauto.
 
-(* set *)
+- (* set *)
   monadInv TR. inv MTR. econstructor; split.
   apply plus_one. econstructor. eapply transl_expr_correct; eauto.
   eapply match_states_skip; eauto.
 
-(* call *)
+- (* call *)
   revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
   intros targs tres cc CF TR. monadInv TR. inv MTR.
-  exploit functions_translated; eauto. intros [tfd [FIND TFD]].
+  exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
   rewrite H in CF. simpl in CF. inv CF.
   econstructor; split.
   apply plus_one. econstructor; eauto.
-  exploit transl_expr_correct; eauto.
-  exploit transl_arglist_correct; eauto.
+  eapply transl_expr_correct with (cunit := cu); eauto. 
+  eapply transl_arglist_correct with (cunit := cu); eauto.
   erewrite typlist_of_arglist_eq by eauto.
   eapply transl_fundef_sig1; eauto.
   rewrite H3. auto.
   econstructor; eauto.
-  econstructor; eauto.
+  eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
   simpl. auto.
 
-(* builtin *)
+- (* builtin *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. econstructor.
   eapply transl_arglist_correct; eauto.
-  eapply external_call_symbols_preserved_gen with (ge1 := ge).
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto.
+  eapply external_call_symbols_preserved with (ge1 := ge). apply senv_preserved. eauto.
   eapply match_states_skip; eauto.
 
-(* seq *)
+- (* seq *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. constructor.
   econstructor; eauto.
 
-(* skip seq *)
+- (* skip seq *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. apply step_skip_seq.
   econstructor; eauto. constructor.
 
-(* continue seq *)
+- (* continue seq *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. simpl. reflexivity. constructor.
 
-(* break seq *)
+- (* break seq *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. simpl. reflexivity. constructor.
 
-(* ifthenelse *)
+- (* ifthenelse *)
   monadInv TR. inv MTR.
   exploit make_boolean_correct; eauto.
   exploit transl_expr_correct; eauto.
@@ -1327,7 +1440,7 @@ Proof.
   apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto.
   destruct b; econstructor; eauto; constructor.
 
-(* loop *)
+- (* loop *)
   monadInv TR.
   econstructor; split.
   eapply star_plus_trans. eapply match_transl_step; eauto.
@@ -1337,9 +1450,9 @@ Proof.
   reflexivity. reflexivity. traceEq.
   econstructor; eauto. constructor. econstructor; eauto.
 
-(* skip-or-continue loop *)
+- (* skip-or-continue loop *)
   assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk).
-    destruct H; subst x; monadInv TR; inv MTR; auto.
+  { destruct H; subst x; monadInv TR; inv MTR; auto. }
   destruct H0. inv MK.
   econstructor; split.
   eapply plus_left.
@@ -1347,7 +1460,7 @@ Proof.
   apply star_one. constructor. traceEq.
   econstructor; eauto. constructor. econstructor; eauto.
 
-(* break loop1 *)
+- (* break loop1 *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   eapply plus_left. constructor.
@@ -1357,16 +1470,15 @@ Proof.
   reflexivity. reflexivity. traceEq.
   eapply match_states_skip; eauto.
 
-(* skip loop2 *)
+- (* skip loop2 *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
-Local Opaque ge.
-  simpl. rewrite H5; simpl. rewrite H7; simpl. eauto.
+  simpl. rewrite H6; simpl. rewrite H8; simpl. eauto.
   constructor.
 
-(* break loop2 *)
+- (* break loop2 *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   eapply plus_left. constructor.
@@ -1374,32 +1486,32 @@ Local Opaque ge.
   traceEq.
   eapply match_states_skip; eauto.
 
-(* return none *)
+- (* return none *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   eapply match_env_free_blocks; eauto.
-  econstructor; eauto.
+  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
 
-(* return some *)
+- (* return some *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto.
   eapply match_env_free_blocks; eauto.
-  econstructor; eauto.
+  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
 
-(* skip call *)
+- (* skip call *)
   monadInv TR. inv MTR.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
   apply plus_one. apply step_skip_call. auto.
   eapply match_env_free_blocks; eauto.
-  constructor. eauto.
+  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
 
-(* switch *)
+- (* switch *)
   monadInv TR.
   assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n).
   { unfold sem_switch_arg in H0.
@@ -1415,7 +1527,7 @@ Local Opaque ge.
   constructor.
   econstructor. eauto.
 
-(* skip or break switch *)
+- (* skip or break switch *)
   assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk).
     destruct H; subst x; monadInv TR; inv MTR; auto.
   destruct H0. inv MK.
@@ -1423,57 +1535,54 @@ Local Opaque ge.
   apply plus_one. destruct H0; subst ts'. 2:constructor. constructor.
   eapply match_states_skip; eauto.
 
-
-(* continue switch *)
+- (* continue switch *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. simpl. reflexivity. constructor.
 
-(* label *)
+- (* label *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. constructor.
 
-(* goto *)
+- (* goto *)
   monadInv TR. inv MTR.
   generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'.
-  exploit (transl_find_label lbl). eexact EQ. eapply match_cont_call_cont. eauto.
+  exploit (transl_find_label (prog_comp_env cu) lbl). eexact EQ. eapply match_cont_call_cont. eauto.
   rewrite H.
   intros [ts' [tk'' [nbrk' [ncnt' [A [B C]]]]]].
   econstructor; split.
   apply plus_one. constructor. simpl. eexact A.
   econstructor; eauto. constructor.
 
-(* internal function *)
-  inv H. monadInv TR. monadInv EQ.
+- (* internal function *)
+  inv H. inv TR. monadInv H5. 
   exploit match_cont_is_call_cont; eauto. intros [A B].
   exploit match_env_alloc_variables; eauto.
   apply match_env_empty.
   intros [te1 [C D]].
   econstructor; split.
   apply plus_one. eapply step_internal_function.
-  simpl. rewrite list_map_compose. simpl. assumption.
-  simpl. auto.
-  simpl. auto.
-  simpl. eauto.
+  simpl. erewrite transl_vars_names by eauto. assumption.
+  simpl. assumption.
+  simpl. assumption.
+  simpl; eauto. 
   simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto.
   simpl. econstructor; eauto.
-  unfold transl_function. rewrite EQ0; simpl. auto.
+  unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
   constructor.
 
-(* external function *)
-  simpl in TR.
-  destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR.
+- (* external function *)
+  inv TR.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
   apply plus_one. constructor. eauto.
-  eapply external_call_symbols_preserved_gen with (ge1 := ge).
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto.
-  econstructor; eauto.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  eapply match_returnstate with (ce := ce); eauto.
 
-(* returnstate *)
+- (* returnstate *)
   inv MK.
   econstructor; split.
   apply plus_one. constructor.
@@ -1485,17 +1594,14 @@ Lemma transl_initial_states:
   exists R, initial_state tprog R /\ match_states S R.
 Proof.
   intros. inv H.
-  exploit function_ptr_translated; eauto. intros [tf [A B]].
-  assert (C: Genv.find_symbol tge (AST.prog_main tprog) = Some b).
-    rewrite symbols_preserved. replace (AST.prog_main tprog) with (prog_main prog).
-    auto. symmetry. unfold transl_program in TRANSL.
-    change (prog_main prog) with (AST.prog_main (program_of_program prog)).
-    eapply transform_partial_program2_main; eauto.
-  assert (funsig tf = signature_of_type Tnil type_int32s cc_default).
-    eapply transl_fundef_sig2; eauto.
+  exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C).
+  assert (D: Genv.find_symbol tge (AST.prog_main tprog) = Some b).
+  { destruct TRANSL as (P & Q & R). rewrite Q. rewrite symbols_preserved. auto. }
+  assert (E: funsig tf = signature_of_type Tnil type_int32s cc_default).
+  { eapply transl_fundef_sig2; eauto. }
   econstructor; split.
-  econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto.
-  econstructor; eauto. constructor; auto. exact I.
+  econstructor; eauto. apply (Genv.init_mem_match TRANSL). eauto.
+  econstructor; eauto. instantiate (1 := prog_comp_env cu). constructor; auto. exact I.
 Qed.
 
 Lemma transl_final_states:
@@ -1509,10 +1615,40 @@ Theorem transl_program_correct:
   forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog).
 Proof.
   eapply forward_simulation_plus.
-  eexact public_preserved.
+  apply senv_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
   eexact transl_step.
 Qed.
 
 End CORRECTNESS.
+
+(** ** Commutation with linking *)
+
+Instance TransfCshmgenLink : TransfLink match_prog.
+Proof.
+  red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2).
+  generalize H. 
+Local Transparent Ctypes.Linker_program.
+  simpl; unfold link_program.
+  destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
+  destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|P]; try discriminate.
+  destruct (link_build_composite_env (prog_types p1) (prog_types p2) typs
+           (prog_comp_env p1) (prog_comp_env p2) (prog_comp_env_eq p1)
+           (prog_comp_env_eq p2) EQ) as (env & P & Q).
+  intros E.
+  eapply Linking.link_match_program; eauto.
+- intros. 
+Local Transparent Linker_fundef Linking.Linker_fundef.
+  inv H3; inv H4; simpl in H2. 
++ discriminate.
++ destruct ef; inv H2. econstructor; split. simpl; eauto. left; constructor; auto.
++ destruct ef; inv H2. econstructor; split. simpl; eauto. right; constructor; auto.
++ destruct (external_function_eq ef ef0 && typelist_eq args args0 &&
+         type_eq res res0 && calling_convention_eq cc cc0) eqn:E'; inv H2.
+  InvBooleans. subst ef0. econstructor; split. 
+  simpl; rewrite dec_eq_true; eauto.
+  left; constructor. congruence.
+- intros. exists tt. auto.
+- replace (program_of_program p) with pp. auto. inv E; destruct pp; auto.
+Qed.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index b3cbacca..2650e0a8 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -130,7 +130,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Ebinop op r1 r2 ty) v
   | esr_cast: forall ty r1 v1 v,
       eval_simple_rvalue r1 v1 ->
-      sem_cast v1 (typeof r1) ty = Some v ->
+      sem_cast v1 (typeof r1) ty m = Some v ->
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
       eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
@@ -141,7 +141,7 @@ Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
   | esrl_nil:
       eval_simple_list Enil Tnil nil
   | esrl_cons: forall r rl ty tyl v vl v',
-      eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty = Some v ->
+      eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty m = Some v ->
       eval_simple_list rl tyl vl ->
       eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl).
 
@@ -283,7 +283,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       eval_simple_rvalue e m r v ->
-      sem_cast v (typeof r) (typeof l) = Some v' ->
+      sem_cast v (typeof r) (typeof l) m = Some v' ->
       assign_loc ge (typeof l) m b ofs v' t m' ->
       ty = typeof l ->
       estep (ExprState f (C (Eassign l r ty)) k e m)
@@ -295,7 +295,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       deref_loc ge (typeof l) m b ofs t1 v1 ->
       eval_simple_rvalue e m r v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 ->
-      sem_cast v3 tyres (typeof l) = Some v4 ->
+      sem_cast v3 tyres (typeof l) m = Some v4 ->
       assign_loc ge (typeof l) m b ofs v4 t2 m' ->
       ty = typeof l ->
       t = t1 ** t2 ->
@@ -310,7 +310,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       match sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m with
       | None => True
       | Some v3 =>
-          match sem_cast v3 tyres (typeof l) with
+          match sem_cast v3 tyres (typeof l) m with
           | None => True
           | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m')
           end
@@ -323,8 +323,8 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge ty m b ofs t1 v1 ->
-      sem_incrdecr ge id v1 ty = Some v2 ->
-      sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
+      sem_incrdecr ge id v1 ty m = Some v2 ->
+      sem_cast v2 (incrdecr_type ty) ty m = Some v3 ->
       assign_loc ge ty m b ofs v3 t2 m' ->
       ty = typeof l ->
       t = t1 ** t2 ->
@@ -335,10 +335,10 @@ Inductive estep: state -> trace -> state -> Prop :=
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge ty m b ofs t v1 ->
-      match sem_incrdecr ge id v1 ty with
+      match sem_incrdecr ge id v1 ty m with
       | None => True
       | Some v2 =>
-          match sem_cast v2 (incrdecr_type ty) ty with
+          match sem_cast v2 (incrdecr_type ty) ty m with
           | None => True
           | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m')
           end
@@ -357,7 +357,7 @@ Inductive estep: state -> trace -> state -> Prop :=
   | step_paren: forall f C r tycast ty k e m v1 v,
       leftcontext RV RV C ->
       eval_simple_rvalue e m r v1 ->
-      sem_cast v1 (typeof r) tycast = Some v ->
+      sem_cast v1 (typeof r) tycast m = Some v ->
       estep (ExprState f (C (Eparen r tycast ty)) k e m)
          E0 (ExprState f (C (Eval v ty)) k e m)
 
@@ -472,7 +472,7 @@ Proof.
 Qed.
 
 Lemma callred_kind:
-  forall a fd args ty, callred ge a fd args ty -> expr_kind a = RV.
+  forall a m fd args ty, callred ge a m fd args ty -> expr_kind a = RV.
 Proof.
   induction 1; auto.
 Qed.
@@ -540,7 +540,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
       exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v
   | Ecast (Eval v1 ty1) ty =>
-      exists v, sem_cast v1 ty1 ty = Some v
+      exists v, sem_cast v1 ty1 ty m = Some v
   | Eseqand (Eval v1 ty1) r2 ty =>
       exists b, bool_val v1 ty1 m = Some b
   | Eseqor (Eval v1 ty1) r2 ty =>
@@ -549,7 +549,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists b, bool_val v1 ty1 m = Some b
   | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
       exists v, exists m', exists t,
-      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m'
+      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m'
   | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
       exists t, exists v1,
       ty = ty1
@@ -561,18 +561,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
   | Eparen (Eval v1 ty1) ty2 ty =>
-      exists v, sem_cast v1 ty1 ty2 = Some v
+      exists v, sem_cast v1 ty1 ty2 m = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs tyres cconv fd vl,
          classify_fun tyf = fun_case_f tyargs tyres cconv
       /\ Genv.find_funct ge vf = Some fd
-      /\ cast_arguments rargs tyargs vl
+      /\ cast_arguments m rargs tyargs vl
       /\ type_of_fundef fd = Tfunction tyargs tyres cconv
   | Ebuiltin ef tyargs rargs ty =>
       exprlist_all_values rargs ->
       exists vargs, exists t, exists vres, exists m',
-         cast_arguments rargs tyargs vargs
+         cast_arguments m rargs tyargs vargs
       /\ external_call ef ge vargs m t vres m'
   | _ => True
   end.
@@ -608,7 +608,7 @@ Qed.
 
 Lemma callred_invert:
   forall r fd args ty m,
-  callred ge r fd args ty ->
+  callred ge r m fd args ty ->
   invert_expr_prop r m.
 Proof.
   intros. inv H. simpl.
@@ -893,7 +893,7 @@ Inductive eval_simple_list': exprlist -> list val -> Prop :=
 Lemma eval_simple_list_implies:
   forall rl tyl vl,
   eval_simple_list e m rl tyl vl ->
-  exists vl', cast_arguments (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'.
+  exists vl', cast_arguments m (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'.
 Proof.
   induction 1.
   exists (@nil val); split. constructor. constructor.
@@ -905,7 +905,7 @@ Lemma can_eval_simple_list:
   forall rl vl,
   eval_simple_list' rl vl ->
   forall tyl vl',
-  cast_arguments (rval_list vl rl) tyl vl' ->
+  cast_arguments m (rval_list vl rl) tyl vl' ->
   eval_simple_list e m rl tyl vl'.
 Proof.
   induction 1; simpl; intros.
@@ -1234,9 +1234,9 @@ Proof.
   left; apply step_rred; auto. econstructor; eauto.
   set (op := match id with Incr => Oadd | Decr => Osub end).
   assert (SEM: sem_binary_operation ge op v1 (typeof l) (Vint Int.one) type_int32s m =
-              sem_incrdecr ge id v1 (typeof l)).
+              sem_incrdecr ge id v1 (typeof l) m).
     destruct id; auto.
-  destruct (sem_incrdecr ge id v1 (typeof l)) as [v2|].
+  destruct (sem_incrdecr ge id v1 (typeof l) m) as [v2|].
   eapply star_left.
   left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
   econstructor; eauto.
@@ -1329,7 +1329,7 @@ Proof.
   intros [v [E2 S2]].
   exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]].
   destruct (sem_binary_operation ge op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?.
-  destruct (sem_cast v3 tyres (typeof b1)) as [v4|] eqn:?.
+  destruct (sem_cast v3 tyres (typeof b1) m) as [v4|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')).
   destruct H2 as [t2 [m' D]].
   econstructor; econstructor; eapply step_assignop; eauto.
@@ -1343,8 +1343,8 @@ Proof.
   exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto.
   intros [b1 [ofs [E1 S1]]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]].
-  destruct (sem_incrdecr ge id v1 ty) as [v2|] eqn:?.
-  destruct (sem_cast v2 (incrdecr_type ty) ty) as [v3|] eqn:?.
+  destruct (sem_incrdecr ge id v1 ty m) as [v2|] eqn:?.
+  destruct (sem_cast v2 (incrdecr_type ty) ty m) as [v3|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')).
   destruct H0 as [t2 [m' D]].
   econstructor; econstructor; eapply step_postincr; eauto.
@@ -1498,7 +1498,7 @@ Proof.
   econstructor; econstructor; eauto.
   inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1511,7 +1511,7 @@ Proof.
   (* assignop stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1526,8 +1526,8 @@ Proof.
   subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
   econstructor; econstructor; eauto.
   inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
-  destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?.
-  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?.
+  destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1539,8 +1539,8 @@ Proof.
   rewrite Heqo; auto.
   (* postincr stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
-  destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?.
-  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?.
+  destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
@@ -1641,11 +1641,11 @@ Definition outcome_switch (out: outcome) : outcome :=
   | o => o
   end.
 
-Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
+Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem) : Prop :=
   match out, t with
   | Out_normal, Tvoid => v = Vundef
   | Out_return None, Tvoid => v = Vundef
-  | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty = Some v
+  | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty m = Some v
   | _, _ => False
   end.
 
@@ -1697,7 +1697,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) m' = Some true ->
       eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 ->
-      sem_cast v2 (typeof a2) type_bool = Some v ->
+      sem_cast v2 (typeof a2) type_bool m'' = Some v ->
       eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty)
   | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
@@ -1707,7 +1707,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) m' = Some false ->
       eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 ->
-      sem_cast v2 (typeof a2) type_bool = Some v ->
+      sem_cast v2 (typeof a2) type_bool m'' = Some v ->
       eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty)
   | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
@@ -1717,7 +1717,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) m' = Some b ->
       eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' ->
-      sem_cast v' (typeof (if b then a2 else a3)) ty = Some v ->
+      sem_cast v' (typeof (if b then a2 else a3)) ty m'' = Some v ->
       eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty)
   | eval_sizeof: forall e m ty' ty,
       eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty)
@@ -1727,7 +1727,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' ->
       eval_simple_lvalue ge e m2 l' b ofs ->
       eval_simple_rvalue ge e m2 r' v ->
-      sem_cast v (typeof r) (typeof l) = Some v' ->
+      sem_cast v (typeof r) (typeof l) m2 = Some v' ->
       assign_loc ge (typeof l) m2 b ofs v' t3 m3 ->
       ty = typeof l ->
       eval_expr e m RV (Eassign l r ty) (t1**t2**t3) m3 (Eval v' ty)
@@ -1738,7 +1738,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       deref_loc ge (typeof l) m2 b ofs t3 v1 ->
       eval_simple_rvalue ge e m2 r' v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 ->
-      sem_cast v3 tyres (typeof l) = Some v4 ->
+      sem_cast v3 tyres (typeof l) m2 = Some v4 ->
       assign_loc ge (typeof l) m2 b ofs v4 t4 m3 ->
       ty = typeof l ->
       eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v4 ty)
@@ -1746,8 +1746,8 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m LV l t1 m1 l' ->
       eval_simple_lvalue ge e m1 l' b ofs ->
       deref_loc ge ty m1 b ofs t2 v1 ->
-      sem_incrdecr ge id v1 ty = Some v2 ->
-      sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
+      sem_incrdecr ge id v1 ty m1 = Some v2 ->
+      sem_cast v2 (incrdecr_type ty) ty m1 = Some v3 ->
       assign_loc ge ty m1 b ofs v3 t3 m2 ->
       ty = typeof l ->
       eval_expr e m RV (Epostincr id l ty) (t1**t2**t3) m2 (Eval v1 ty)
@@ -1901,7 +1901,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       bind_parameters ge 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 ->
+      outcome_result_value out f.(fn_return) vres m3 ->
       Mem.free_list m3 (blocks_of_env ge e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
   | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 89d0b2bf..fd7a6b96 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -15,14 +15,9 @@
 
 (** Abstract syntax for the Compcert C language *)
 
-Require Import Coqlib.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Errors.
-Require Import Ctypes.
-Require Import Cop.
+Require Import Coqlib Maps Integers Floats Errors.
+Require Import AST Linking Values.
+Require Import Ctypes Cop.
 
 (** ** Expressions *)
 
@@ -191,9 +186,7 @@ Definition var_names (vars: list(ident * type)) : list ident :=
 (** Functions can either be defined ([Internal]) or declared as
   external functions ([External]). *)
 
-Inductive fundef : Type :=
-  | Internal: function -> fundef
-  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+Definition fundef := Ctypes.fundef function.
 
 (** The type of a function definition. *)
 
@@ -206,50 +199,15 @@ Definition type_of_fundef (f: fundef) : type :=
   | External id args res cc => Tfunction args res cc
   end.
 
-(** ** Programs *)
+(** ** Programs and compilation units *)
 
-(** A "pre-program", as produced by the elaborator is composed of:
+(** As defined in module [Ctypes], a program, or compilation unit, is
+  composed of:
 - a list of definitions of functions and global variables;
 - the names of functions and global variables that are public (not static);
 - the name of the function that acts as entry point ("main" function).
 - a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
 
-A program is composed of the same information, plus the corresponding
-composite environment, and a proof that this environment is consistent
-with the composite definitions. *)
-
-Record pre_program : Type := {
-  pprog_defs: list (ident * globdef fundef type);
-  pprog_public: list ident;
-  pprog_main: ident;
-  pprog_types: list composite_definition
-}.
-
-Record program : Type := {
-  prog_defs: list (ident * globdef fundef type);
-  prog_public: list ident;
-  prog_main: ident;
-  prog_types: list composite_definition;
-  prog_comp_env: composite_env;
-  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
-}.
-
-Definition program_of_program (p: program) : AST.program fundef type :=
-  {| AST.prog_defs := p.(prog_defs);
-     AST.prog_public := p.(prog_public);
-     AST.prog_main := p.(prog_main) |}.
-
-Coercion program_of_program: program >-> AST.program.
-
-Program Definition program_of_pre_program (p: pre_program) : res program :=
-  match build_composite_env p.(pprog_types) with
-  | Error e => Error e
-  | OK ce =>
-      OK {| prog_defs := p.(pprog_defs);
-            prog_public := p.(pprog_public);
-            prog_main := p.(pprog_main);
-            prog_types := p.(pprog_types);
-            prog_comp_env := ce;
-            prog_comp_env_eq := _ |}
-  end.
-
+Definition program := Ctypes.program function.
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 78345b42..9faa6d40 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -15,10 +15,8 @@
 
 (** Type expressions for the Compcert C and Clight languages *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Errors.
+Require Import Axioms Coqlib Maps Errors.
+Require Import AST Linking.
 Require Archi.
 
 (** * Syntax of types *)
@@ -157,6 +155,20 @@ Definition members : Type := list (ident * type).
 Inductive composite_definition : Type :=
   Composite (id: ident) (su: struct_or_union) (m: members) (a: attr).
 
+Definition name_composite_def (c: composite_definition) : ident :=
+  match c with Composite id su m a => id end.
+
+Definition composite_def_eq (x y: composite_definition): {x=y} + {x<>y}.
+Proof.
+  decide equality.
+- decide equality. decide equality. apply N.eq_dec. apply bool_dec.
+- apply list_eq_dec. decide equality. apply type_eq. apply ident_eq.
+- decide equality.
+- apply ident_eq.
+Defined.
+
+Global Opaque composite_def_eq. 
+
 (** For type-checking, compilation and semantics purposes, the composite
   definitions are collected in the following [composite_env] environment.
   The [composite] record contains additional information compared with
@@ -960,6 +972,29 @@ Record composite_consistent (env: composite_env) (co: composite) : Prop := {
 Definition composite_env_consistent (env: composite_env) : Prop :=
   forall id co, env!id = Some co -> composite_consistent env co.
 
+Lemma composite_consistent_stable:
+  forall (env env': composite_env)
+         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
+         co,
+  composite_consistent env co -> composite_consistent env' co.
+Proof.
+  intros. destruct H as [A B C D]. constructor. 
+  eapply complete_members_stable; eauto.
+  symmetry; rewrite B. f_equal. apply alignof_composite_stable; auto. 
+  symmetry; rewrite C. f_equal. apply sizeof_composite_stable; auto.
+  symmetry; rewrite D. apply rank_members_stable; auto.
+Qed.
+
+Lemma composite_of_def_consistent:
+  forall env id su m a co,
+  composite_of_def env id su m a = OK co ->
+  composite_consistent env co.
+Proof.
+  unfold composite_of_def; intros. 
+  destruct (env!id); try discriminate. destruct (complete_members env m) eqn:C; inv H.
+  constructor; auto.
+Qed. 
+
 Theorem build_composite_env_consistent:
   forall defs env, build_composite_env defs = OK env -> composite_env_consistent env.
 Proof.
@@ -973,28 +1008,15 @@ Proof.
 - destruct d1; monadInv H.
   eapply IHdefs; eauto.
   set (env1 := PTree.set id x env0) in *.
-  unfold composite_of_def in EQ.
-  destruct (env0!id) eqn:E; try discriminate.
-  destruct (complete_members env0 m) eqn:C; inversion EQ; clear EQ.
+  assert (env0!id = None). 
+  { unfold composite_of_def in EQ. destruct (env0!id). discriminate. auto. }
   assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1).
   { intros. unfold env1. rewrite PTree.gso; auto. congruence. }
-  red; intros. unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
+  red; intros. apply composite_consistent_stable with env0; auto.
+  unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
 + subst id0. inversion H2; clear H2. subst co.
-(*
-  assert (A: alignof_composite env1 m = alignof_composite env0 m)
-  by (apply alignof_composite_stable; assumption).
-*)
-  rewrite <- H1; constructor; simpl.
-* eapply complete_members_stable; eauto.
-* f_equal. symmetry. apply alignof_composite_stable; auto.
-* f_equal. symmetry. apply sizeof_composite_stable; auto.
-* symmetry. apply rank_members_stable; auto.
-+ exploit H0; eauto. intros [P Q R S].
-  constructor; intros.
-* eapply complete_members_stable; eauto.
-* rewrite Q. f_equal. symmetry. apply alignof_composite_stable; auto.
-* rewrite R. f_equal. symmetry. apply sizeof_composite_stable; auto.
-* rewrite S. symmetry; apply rank_members_stable; auto.
+  eapply composite_of_def_consistent; eauto.
++ eapply H0; eauto. 
 Qed.
 
 (** Moreover, every composite definition is reflected in the composite environment. *)
@@ -1018,6 +1040,29 @@ Proof.
   subst x; auto.
 Qed.
 
+Theorem build_composite_env_domain:
+  forall env defs id co,
+  build_composite_env defs = OK env ->
+  env!id = Some co ->
+  In (Composite id (co_su co) (co_members co) (co_attr co)) defs.
+Proof.
+  intros env0 defs0 id co.
+  assert (REC: forall l env env',
+    add_composite_definitions env l = OK env' ->
+    env'!id = Some co ->
+    env!id = Some co \/ In (Composite id (co_su co) (co_members co) (co_attr co)) l).
+  { induction l; simpl; intros. 
+  - inv H; auto.
+  - destruct a; monadInv H. exploit IHl; eauto.
+    unfold composite_of_def in EQ. destruct (env!id0) eqn:E; try discriminate.
+    destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
+    rewrite PTree.gsspec. intros [A|A]; auto.
+    destruct (peq id id0); auto.
+    inv A. rewrite <- H1; auto.
+  }
+  intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence.
+Qed.
+
 (** As a corollay, in a consistent environment, the rank of a composite type
   is strictly greater than the ranks of its member types. *)
 
@@ -1054,3 +1099,441 @@ Proof.
   exploit (rank_type_members ce); eauto.
   omega.
 Qed.
+
+(** * Programs and compilation units *)
+
+(** The definitions in this section are parameterized over a type [F] of 
+  internal function definitions, so that they apply both to CompCert C and to Clight. *)
+
+Set Implicit Arguments.
+
+Section PROGRAMS.
+
+Variable F: Type.
+
+(** Functions can either be defined ([Internal]) or declared as
+  external functions ([External]). *)
+
+Inductive fundef : Type :=
+  | Internal: F -> fundef
+  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+
+(** A program, or compilation unit, is composed of:
+- a list of definitions of functions and global variables;
+- the names of functions and global variables that are public (not static);
+- the name of the function that acts as entry point ("main" function).
+- a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
+
+Record program : Type := {
+  prog_defs: list (ident * globdef fundef type);
+  prog_public: list ident;
+  prog_main: ident;
+  prog_types: list composite_definition;
+  prog_comp_env: composite_env;
+  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
+}.
+
+Definition program_of_program (p: program) : AST.program fundef type :=
+  {| AST.prog_defs := p.(prog_defs);
+     AST.prog_public := p.(prog_public);
+     AST.prog_main := p.(prog_main) |}.
+
+Coercion program_of_program: program >-> AST.program.
+
+Program Definition make_program (types: list composite_definition)
+                                (defs: list (ident * globdef fundef type))
+                                (public: list ident)
+                                (main: ident) : res program :=
+  match build_composite_env types with
+  | Error e => Error e
+  | OK ce =>
+      OK {| prog_defs := defs;
+            prog_public := public;
+            prog_main := main;
+            prog_types := types;
+            prog_comp_env := ce;
+            prog_comp_env_eq := _ |}
+  end.
+
+End PROGRAMS.
+
+Arguments External {F} _ _ _ _.
+
+Unset Implicit Arguments.
+
+(** * Separate compilation and linking *)
+
+(** ** Linking types *)
+
+Instance Linker_types : Linker type := {
+  link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None;
+  linkorder := fun t1 t2 => t1 = t2
+}.
+Proof.
+  auto.
+  intros; congruence.
+  intros. destruct (type_eq x y); inv H. auto.
+Defined.
+
+Global Opaque Linker_types.
+
+(** ** Linking composite definitions *)
+
+Definition check_compat_composite (l: list composite_definition) (cd: composite_definition) : bool :=
+  List.forallb
+    (fun cd' =>
+      if ident_eq (name_composite_def cd') (name_composite_def cd) then composite_def_eq cd cd' else true)
+    l.
+
+Definition filter_redefs (l1 l2: list composite_definition) :=
+  let names1 := map name_composite_def l1 in
+  List.filter (fun cd => negb (In_dec ident_eq (name_composite_def cd) names1)) l2.
+
+Definition link_composite_defs (l1 l2: list composite_definition): option (list composite_definition) :=
+  if List.forallb (check_compat_composite l2) l1
+  then Some (l1 ++ filter_redefs l1 l2)
+  else None.
+
+Lemma link_composite_def_inv:
+  forall l1 l2 l,
+  link_composite_defs l1 l2 = Some l ->
+     (forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)
+  /\ l = l1 ++ filter_redefs l1 l2
+  /\ (forall x, In x l <-> In x l1 \/ In x l2).
+Proof.
+  unfold link_composite_defs; intros.
+  destruct (forallb (check_compat_composite l2) l1) eqn:C; inv H.
+  assert (A: 
+    forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1).
+  { rewrite forallb_forall in C. intros.
+    apply C in H. unfold check_compat_composite in H. rewrite forallb_forall in H. 
+    apply H in H0. rewrite H1, dec_eq_true in H0. symmetry; eapply proj_sumbool_true; eauto. }
+  split. auto. split. auto. 
+  unfold filter_redefs; intros. 
+  rewrite in_app_iff. rewrite filter_In. intuition auto. 
+  destruct (in_dec ident_eq (name_composite_def x) (map name_composite_def l1)); simpl; auto.
+  exploit list_in_map_inv; eauto. intros (y & P & Q).
+  assert (x = y) by eauto. subst y. auto.
+Qed.
+
+Instance Linker_composite_defs : Linker (list composite_definition) := {
+  link := link_composite_defs;
+  linkorder := @List.incl composite_definition
+}.
+Proof.
+- intros; apply incl_refl.
+- intros; red; intros; eauto.
+- intros. apply link_composite_def_inv in H; destruct H as (A & B & C).
+  split; red; intros; apply C; auto.
+Defined.
+
+(** Connections with [build_composite_env]. *)
+
+Lemma add_composite_definitions_append:
+  forall l1 l2 env env'',
+  add_composite_definitions env (l1 ++ l2) = OK env'' <->
+  exists env', add_composite_definitions env l1 = OK env' /\ add_composite_definitions env' l2 = OK env''.
+Proof.
+  induction l1; simpl; intros.
+- split; intros. exists env; auto. destruct H as (env' & A & B). congruence.
+- destruct a; simpl. destruct (composite_of_def env id su m a); simpl.
+  apply IHl1. 
+  split; intros. discriminate. destruct H as (env' & A & B); discriminate.
+Qed.
+
+Lemma composite_eq:
+  forall su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1
+         su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2,
+  su1 = su2 -> m1 = m2 -> a1 = a2 -> sz1 = sz2 -> al1 = al2 -> r1 = r2 ->
+  Build_composite su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1 = Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2.
+Proof.
+  intros. subst.
+  assert (pos1 = pos2) by apply proof_irr. 
+  assert (al2p1 = al2p2) by apply proof_irr.
+  assert (szal1 = szal2) by apply proof_irr.
+  subst. reflexivity.
+Qed.
+
+Lemma composite_of_def_eq:
+  forall env id co,
+  composite_consistent env co ->
+  env!id = None ->
+  composite_of_def env id (co_su co) (co_members co) (co_attr co) = OK co.
+Proof.
+  intros. destruct H as [A B C D]. unfold composite_of_def. rewrite H0, A.
+  destruct co; simpl in *. f_equal. apply composite_eq; auto. rewrite C, B; auto. 
+Qed.
+
+Lemma composite_consistent_unique:
+  forall env co1 co2,
+  composite_consistent env co1 ->
+  composite_consistent env co2 ->
+  co_su co1 = co_su co2 ->
+  co_members co1 = co_members co2 ->
+  co_attr co1 = co_attr co2 ->
+  co1 = co2.
+Proof.
+  intros. destruct H, H0. destruct co1, co2; simpl in *. apply composite_eq; congruence.
+Qed.
+
+Lemma composite_of_def_stable:
+  forall (env env': composite_env)
+         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
+         id su m a co,
+  env'!id = None ->
+  composite_of_def env id su m a = OK co ->
+  composite_of_def env' id su m a = OK co.
+Proof.
+  intros. 
+  unfold composite_of_def in H0. 
+  destruct (env!id) eqn:E; try discriminate.
+  destruct (complete_members env m) eqn:CM; try discriminate.
+  transitivity (composite_of_def env' id (co_su co) (co_members co) (co_attr co)).
+  inv H0; auto. 
+  apply composite_of_def_eq; auto. 
+  apply composite_consistent_stable with env; auto. 
+  inv H0; constructor; auto.
+Qed.
+
+Lemma link_add_composite_definitions:
+  forall l0 env0,
+  build_composite_env l0 = OK env0 ->
+  forall l env1 env1' env2,
+  add_composite_definitions env1 l = OK env1' ->
+  (forall id co, env1!id = Some co -> env2!id = Some co) ->
+  (forall id co, env0!id = Some co -> env2!id = Some co) ->
+  (forall id, env2!id = if In_dec ident_eq id (map name_composite_def l0) then env0!id else env1!id) ->
+  ((forall cd1 cd2, In cd1 l0 -> In cd2 l -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)) ->
+  { env2' |
+      add_composite_definitions env2 (filter_redefs l0 l) = OK env2'
+  /\ (forall id co, env1'!id = Some co -> env2'!id = Some co)
+  /\ (forall id co, env0!id = Some co -> env2'!id = Some co) }.
+Proof.
+  induction l; simpl; intros until env2; intros ACD AGREE1 AGREE0 AGREE2 UNIQUE.
+- inv ACD. exists env2; auto.
+- destruct a. destruct (composite_of_def env1 id su m a) as [x|e] eqn:EQ; try discriminate.
+  simpl in ACD.
+  generalize EQ. unfold composite_of_def at 1. 
+  destruct (env1!id) eqn:E1; try congruence.
+  destruct (complete_members env1 m) eqn:CM1; try congruence. 
+  intros EQ1.
+  simpl. destruct (in_dec ident_eq id (map name_composite_def l0)); simpl.
++ eapply IHl; eauto.
+* intros. rewrite PTree.gsspec in H0. destruct (peq id0 id); auto.
+  inv H0.
+  exploit list_in_map_inv; eauto. intros ([id' su' m' a'] & P & Q).
+  assert (X: Composite id su m a = Composite id' su' m' a').
+  { eapply UNIQUE. auto. auto. rewrite <- P; auto. }
+  inv X.
+  exploit build_composite_env_charact; eauto. intros (co' & U & V & W & X). 
+  assert (co' = co).
+  { apply composite_consistent_unique with env2.
+    apply composite_consistent_stable with env0; auto. 
+    eapply build_composite_env_consistent; eauto.
+    apply composite_consistent_stable with env1; auto.
+    inversion EQ1; constructor; auto. 
+    inversion EQ1; auto.
+    inversion EQ1; auto.
+    inversion EQ1; auto. }
+  subst co'. apply AGREE0; auto. 
+* intros. rewrite AGREE2. destruct (in_dec ident_eq id0 (map name_composite_def l0)); auto. 
+  rewrite PTree.gsspec. destruct (peq id0 id); auto. subst id0. contradiction.
++ assert (E2: env2!id = None).
+  { rewrite AGREE2. rewrite pred_dec_false by auto. auto. }
+  assert (E3: composite_of_def env2 id su m a = OK x).
+  { eapply composite_of_def_stable. eexact AGREE1. eauto. eauto. }
+  rewrite E3. simpl. eapply IHl; eauto. 
+* intros until co; rewrite ! PTree.gsspec. destruct (peq id0 id); auto.
+* intros until co; rewrite ! PTree.gsspec. intros. destruct (peq id0 id); auto.
+  subst id0. apply AGREE0 in H0. congruence.
+* intros. rewrite ! PTree.gsspec. destruct (peq id0 id); auto. subst id0. 
+  rewrite pred_dec_false by auto. auto.
+Qed.
+
+Theorem link_build_composite_env:
+  forall l1 l2 l env1 env2,
+  build_composite_env l1 = OK env1 ->
+  build_composite_env l2 = OK env2 ->
+  link l1 l2 = Some l ->
+  { env |
+     build_composite_env l = OK env
+  /\ (forall id co, env1!id = Some co -> env!id = Some co)
+  /\ (forall id co, env2!id = Some co -> env!id = Some co) }.
+Proof.
+  intros. edestruct link_composite_def_inv as (A & B & C); eauto.
+  edestruct link_add_composite_definitions as (env & P & Q & R).
+  eexact H.
+  eexact H0.
+  instantiate (1 := env1). intros. rewrite PTree.gempty in H2; discriminate.
+  auto.
+  intros. destruct (in_dec ident_eq id (map name_composite_def l1)); auto.
+  rewrite PTree.gempty. destruct (env1!id) eqn:E1; auto. 
+  exploit build_composite_env_domain. eexact H. eauto.
+  intros. apply (in_map name_composite_def) in H2. elim n; auto. 
+  auto.
+  exists env; split; auto. subst l. apply add_composite_definitions_append. exists env1; auto. 
+Qed.
+
+(** ** Linking function definitions *)
+
+Definition link_fundef {F: Type} (fd1 fd2: fundef F) :=
+  match fd1, fd2 with
+  | Internal _, Internal _ => None
+  | External ef1 targs1 tres1 cc1, External ef2 targs2 tres2 cc2 =>
+      if external_function_eq ef1 ef2
+      && typelist_eq targs1 targs2
+      && type_eq tres1 tres2
+      && calling_convention_eq cc1 cc2
+      then Some (External ef1 targs1 tres1 cc1)
+      else None
+  | Internal f, External ef targs tres cc =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  | External ef targs tres cc, Internal f =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  end.
+
+Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
+  | linkorder_fundef_refl: forall fd,
+      linkorder_fundef fd fd
+  | linkorder_fundef_ext_int: forall f id sg targs tres cc,
+      linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f).
+
+Instance Linker_fundef (F: Type): Linker (fundef F) := {
+  link := link_fundef;
+  linkorder := linkorder_fundef
+}.
+Proof.
+- intros; constructor.
+- intros. inv H; inv H0; constructor.
+- intros x y z EQ. destruct x, y; simpl in EQ.
++ discriminate.
++ destruct e; inv EQ. split; constructor.
++ destruct e; inv EQ. split; constructor.
++ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv EQ.
+  InvBooleans. subst. split; constructor.
+Defined.
+
+Remark link_fundef_either:
+  forall (F: Type) (f1 f2 f: fundef F), link f1 f2 = Some f -> f = f1 \/ f = f2.
+Proof.
+  simpl; intros. unfold link_fundef in H. destruct f1, f2; try discriminate.
+- destruct e; inv H. auto.
+- destruct e; inv H. auto.
+- destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0); inv H; auto.
+Qed.
+
+Global Opaque Linker_fundef.
+
+(** ** Linking programs *)
+
+Definition lift_option {A: Type} (opt: option A) : { x | opt = Some x } + { opt = None }.
+Proof.
+  destruct opt. left; exists a; auto. right; auto. 
+Defined.
+
+Definition link_program {F:Type} (p1 p2: program F): option (program F) :=
+  match link (program_of_program p1) (program_of_program p2) with
+  | None => None
+  | Some p =>
+      match lift_option (link p1.(prog_types) p2.(prog_types)) with
+      | inright _ => None
+      | inleft (exist typs EQ) =>
+          match link_build_composite_env
+                   p1.(prog_types) p2.(prog_types) typs
+                   p1.(prog_comp_env) p2.(prog_comp_env)
+                   p1.(prog_comp_env_eq) p2.(prog_comp_env_eq) EQ with
+          | exist env (conj P Q) =>
+              Some {| prog_defs := p.(AST.prog_defs);
+                      prog_public := p.(AST.prog_public);
+                      prog_main := p.(AST.prog_main);
+                      prog_types := typs;
+                      prog_comp_env := env;
+                      prog_comp_env_eq := P |}
+          end
+      end
+  end.
+
+Definition linkorder_program {F: Type} (p1 p2: program F) : Prop :=
+     linkorder (program_of_program p1) (program_of_program p2)
+  /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co).
+
+Instance Linker_program (F: Type): Linker (program F) := {
+  link := link_program;
+  linkorder := linkorder_program
+}.
+Proof.
+- intros; split. apply linkorder_refl. auto. 
+- intros. destruct H, H0. split. eapply linkorder_trans; eauto.
+  intros; auto.
+- intros until z. unfold link_program. 
+  destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate.
+  destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate.
+  destruct (link_build_composite_env (prog_types x) (prog_types y) typs
+       (prog_comp_env x) (prog_comp_env y) (prog_comp_env_eq x)
+       (prog_comp_env_eq y) EQ) as (env & P & Q & R).
+  destruct (link_linkorder _ _ _ LP). 
+  intros X; inv X.
+  split; split; auto.
+Defined.
+
+Global Opaque Linker_program.
+
+(** ** Commutation between linking and program transformations *)
+
+Section LINK_MATCH_PROGRAM.
+
+Context {F G: Type}.
+Variable match_fundef: fundef F -> fundef G -> Prop.
+
+Hypothesis link_match_fundef:
+  forall f1 tf1 f2 tf2 f,
+  link f1 f2 = Some f ->
+  match_fundef f1 tf1 -> match_fundef f2 tf2 ->
+  exists tf, link tf1 tf2 = Some tf /\ match_fundef f tf.
+
+Let match_program (p: program F) (tp: program G) : Prop :=
+    Linking.match_program (fun ctx f tf => match_fundef f tf) eq p tp
+ /\ prog_types tp = prog_types p.
+
+Theorem link_match_program:
+  forall p1 p2 tp1 tp2 p,
+  link p1 p2 = Some p -> match_program p1 tp1 -> match_program p2 tp2 ->
+  exists tp, link tp1 tp2 = Some tp /\ match_program p tp.
+Proof.
+  intros. destruct H0, H1. 
+Local Transparent Linker_program.
+  simpl in H; unfold link_program in H.
+  destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
+  assert (A: exists tpp,
+               link (program_of_program tp1) (program_of_program tp2) = Some tpp
+             /\ Linking.match_program (fun ctx f tf => match_fundef f tf) eq pp tpp).
+  { eapply Linking.link_match_program. 
+  - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto.
+  - intros.
+    Local Transparent Linker_types.
+    simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto.
+  - eauto.
+  - eauto.
+  - eauto.
+  - apply (link_linkorder _ _ _ LP).
+  - apply (link_linkorder _ _ _ LP). }
+  destruct A as (tpp & TLP & MP).
+  simpl; unfold link_program. rewrite TLP.
+  destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|EQ]; try discriminate.
+  destruct (link_build_composite_env (prog_types p1) (prog_types p2) typs
+           (prog_comp_env p1) (prog_comp_env p2) (prog_comp_env_eq p1)
+           (prog_comp_env_eq p2) EQ) as (env & P & Q). 
+  rewrite <- H2, <- H3 in EQ.
+  destruct (lift_option (link (prog_types tp1) (prog_types tp2))) as [[ttyps EQ']|EQ']; try congruence.
+  assert (ttyps = typs) by congruence. subst ttyps. 
+  destruct (link_build_composite_env (prog_types tp1) (prog_types tp2) typs
+         (prog_comp_env tp1) (prog_comp_env tp2) (prog_comp_env_eq tp1)
+         (prog_comp_env_eq tp2) EQ') as (tenv & R & S).
+  assert (tenv = env) by congruence. subst tenv.
+  econstructor; split; eauto. inv H. split; auto.
+  unfold program_of_program; simpl. destruct pp, tpp; exact MP.
+Qed.
+
+End LINK_MATCH_PROGRAM.
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index aa320f20..440e4e84 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -15,21 +15,11 @@
 
 (** Typing rules and type-checking for the Compcert C language *)
 
-Require Import Coqlib.
 Require Import String.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
-Require Import Errors.
+Require Import Coqlib Maps Integers Floats Errors.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events.
+Require Import Ctypes Cop Csyntax Csem.
 
 Local Open Scope error_monad_scope.
 
@@ -911,8 +901,8 @@ Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fund
 Definition typecheck_program (p: program) : res program :=
   let e := bind_globdef (PTree.empty _) p.(prog_defs) in
   let ce := p.(prog_comp_env) in
-  do defs <- transf_globdefs (retype_fundef ce e) (fun v => OK v) p.(prog_defs);
-  OK {| prog_defs := defs;
+  do tp <- transform_partial_program (retype_fundef ce e) p;
+  OK {| prog_defs := tp.(AST.prog_defs);
         prog_public := p.(prog_public);
         prog_main := p.(prog_main);
         prog_types := p.(prog_types);
@@ -1325,32 +1315,29 @@ Theorem typecheck_program_sound:
   forall p p', typecheck_program p = OK p' -> wt_program p'.
 Proof.
   unfold typecheck_program; intros. monadInv H.
-  rename x into defs.
+  rename x into tp.
   constructor; simpl.
   set (ce := prog_comp_env p) in *.
   set (e := bind_globdef (PTree.empty type) (prog_defs p)) in *.
-  set (e' := bind_globdef (PTree.empty type) defs) in *.
-  assert (MATCH:
-    list_forall2 (match_globdef (fun f tf => retype_fundef ce e f = OK tf) (fun v tv => tv = v)) (prog_defs p) defs).
-  {
-    revert EQ; generalize (prog_defs p) defs.
-    induction l as [ | [id gd] l ]; intros l'; simpl; intros.
-    inv EQ. constructor.
-    destruct gd as [f | v].
-    destruct (retype_fundef ce e f) as [tf|msg] eqn:R; monadInv EQ.
-    constructor; auto. constructor; auto.
-    monadInv EQ. constructor; auto. destruct v; constructor; auto. }
+  set (e' := bind_globdef (PTree.empty type) (AST.prog_defs tp)) in *.
+  assert (M: match_program (fun ctx f tf => retype_fundef ce e f = OK tf) eq p tp)
+  by (eapply match_transform_partial_program; eauto).
+  destruct M as (MATCH & _). simpl in MATCH.
   assert (ENVS: e' = e).
-  { unfold e, e'. revert MATCH; generalize (prog_defs p) defs (PTree.empty type).
+  { unfold e, e'. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp) (PTree.empty type).
     induction l as [ | [id gd] l ]; intros l' t M; inv M.
-    auto. inv H1; simpl; auto. replace (type_of_fundef f2) with (type_of_fundef f1); auto.
-    unfold retype_fundef in H4. destruct f1; monadInv H4; auto. monadInv EQ0; auto.
+    auto.
+    destruct b1 as [id' gd']; destruct H1; simpl in *. inv H0; simpl.
+    replace (type_of_fundef f2) with (type_of_fundef f1); auto.
+    unfold retype_fundef in H2. destruct f1; monadInv H2; auto. monadInv EQ0; auto.
+    inv H1. simpl. auto.
   }
   rewrite ENVS.
-  intros id f. revert MATCH; generalize (prog_defs p) defs. induction 1; simpl; intros.
+  intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp).
+  induction 1; simpl; intros.
   contradiction.
-  destruct H0; auto. subst b1; inv H. destruct f1; simpl in H2.
-  monadInv H2. eapply retype_function_sound; eauto. congruence.
+  destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. 
+  destruct f1; monadInv H4. eapply retype_function_sound; eauto.
 Qed.
 
 (** * Subject reduction *)
@@ -1370,7 +1357,7 @@ Qed.
 Hint Resolve pres_cast_int_int: ty.
 
 Lemma pres_sem_cast:
-  forall v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 = Some v2 -> wt_val v2 ty2.
+  forall m v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 m = Some v2 -> wt_val v2 ty2.
 Proof.
   unfold sem_cast, classify_cast; induction 1; simpl; intros; DestructCases; auto with ty.
 - constructor. apply (pres_cast_int_int I8 s).
@@ -1385,7 +1372,10 @@ Proof.
 - constructor. apply (pres_cast_int_int I8 s).
 - constructor. apply (pres_cast_int_int I16 s).
 - destruct (Float32.cmp Ceq f Float32.zero); auto with ty.
+- constructor. reflexivity.
 - destruct (Int.eq n Int.zero); auto with ty.
+- constructor. reflexivity.
+- constructor. reflexivity.
 Qed.
 
 Lemma pres_sem_binarith:
@@ -1394,7 +1384,7 @@ Lemma pres_sem_binarith:
     (sem_long: signedness -> int64 -> int64 -> option val)
     (sem_float: float -> float -> option val)
     (sem_single: float32 -> float32 -> option val)
-    v1 ty1 v2 ty2 v ty msg,
+    v1 ty1 v2 ty2 m v ty msg,
     (forall sg n1 n2,
      match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) ->
     (forall sg n1 n2,
@@ -1403,14 +1393,14 @@ Lemma pres_sem_binarith:
      match sem_float n1 n2 with None | Some (Vfloat _) | Some Vundef => True | _ => False end) ->
     (forall n1 n2,
      match sem_single n1 n2 with None | Some (Vsingle _) | Some Vundef => True | _ => False end) ->
-    sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 = Some v ->
+    sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 m = Some v ->
     binarith_type ty1 ty2 msg = OK ty ->
     wt_val v ty.
 Proof with (try discriminate).
   intros. unfold sem_binarith, binarith_type in *.
   set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *.
-  destruct (sem_cast v1 ty1 ty') as [v1'|] eqn:CAST1...
-  destruct (sem_cast v2 ty2 ty') as [v2'|] eqn:CAST2...
+  destruct (sem_cast v1 ty1 ty' m) as [v1'|] eqn:CAST1...
+  destruct (sem_cast v2 ty2 ty' m) as [v2'|] eqn:CAST2...
   DestructCases.
 - specialize (H s i i0). rewrite H3 in H.
   destruct v; auto with ty; contradiction.
@@ -1426,12 +1416,12 @@ Lemma pres_sem_binarith_int:
   forall
     (sem_int: signedness -> int -> int -> option val)
     (sem_long: signedness -> int64 -> int64 -> option val)
-    v1 ty1 v2 ty2 v ty msg,
+    v1 ty1 v2 ty2 m v ty msg,
     (forall sg n1 n2,
      match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) ->
     (forall sg n1 n2,
      match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) ->
-    sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 = Some v ->
+    sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 m = Some v ->
     binarith_int_type ty1 ty2 msg = OK ty ->
     wt_val v ty.
 Proof.
@@ -2119,28 +2109,3 @@ Proof.
 Qed.
 
 End PRESERVATION.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index b1a39c64..7228cd75 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -47,7 +47,7 @@ If [a] is a l-value, the returned value denotes:
 *)
 
 Definition do_cast (v: val) (t1 t2: type) : res val :=
-  match sem_cast v t1 t2 with
+  match sem_cast v t1 t2 Mem.empty with
   | Some v' => OK v'
   | None => Error(msg "undefined cast")
   end.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 9c662f5e..d5f39d7d 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -120,7 +120,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Ebinop op r1 r2 ty) v
   | esr_cast: forall ty r1 v1 v,
       eval_simple_rvalue r1 v1 ->
-      sem_cast v1 (typeof r1) ty = Some v ->
+      sem_cast v1 (typeof r1) ty m = Some v ->
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
       eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
@@ -129,7 +129,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_seqand_true: forall r1 r2 ty v1 v2 v3,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true ->
       eval_simple_rvalue r2 v2 ->
-      sem_cast v2 (typeof r2) type_bool = Some v3 ->
+      sem_cast v2 (typeof r2) type_bool m = Some v3 ->
       eval_simple_rvalue (Eseqand r1 r2 ty) v3
   | esr_seqand_false: forall r1 r2 ty v1,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false ->
@@ -137,7 +137,7 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_seqor_false: forall r1 r2 ty v1 v2 v3,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false ->
       eval_simple_rvalue r2 v2 ->
-      sem_cast v2 (typeof r2) type_bool = Some v3 ->
+      sem_cast v2 (typeof r2) type_bool m = Some v3 ->
       eval_simple_rvalue (Eseqor r1 r2 ty) v3
   | esr_seqor_true: forall r1 r2 ty v1,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true ->
@@ -145,13 +145,13 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_condition: forall r1 r2 r3 ty v v1 b v',
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b ->
       eval_simple_rvalue (if b then r2 else r3) v' ->
-      sem_cast v' (typeof (if b then r2 else r3)) ty = Some v ->
+      sem_cast v' (typeof (if b then r2 else r3)) ty m = Some v ->
       eval_simple_rvalue (Econdition r1 r2 r3 ty) v
   | esr_comma: forall r1 r2 ty v1 v,
       eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v ->
       eval_simple_rvalue (Ecomma r1 r2 ty) v
   | esr_paren: forall r tycast ty v v',
-      eval_simple_rvalue r v -> sem_cast v (typeof r) tycast = Some v' ->
+      eval_simple_rvalue r v -> sem_cast v (typeof r) tycast m = Some v' ->
       eval_simple_rvalue (Eparen r tycast ty) v'.
 
 End SIMPLE_EXPRS.
@@ -355,14 +355,16 @@ Proof.
 Qed.
 
 Lemma sem_cast_match:
-  forall v1 ty1 ty2 v2 v1' v2',
-  sem_cast v1 ty1 ty2 = Some v2 ->
+  forall v1 ty1 ty2 m v2 v1' v2',
+  sem_cast v1 ty1 ty2 m = Some v2 ->
   do_cast v1' ty1 ty2 = OK v2' ->
   Val.inject inj v1' v1 ->
   Val.inject inj v2' v2.
 Proof.
-  intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0.
-  exploit sem_cast_inject. eexact E. eauto.
+  intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2 Mem.empty) as [v2''|] eqn:E; inv H0.
+  exploit (sem_cast_inj inj Mem.empty m).
+  intros. rewrite mem_empty_not_weak_valid_pointer in H2. discriminate.
+  eexact E. eauto.
   intros [v' [A B]]. congruence.
 Qed.
 
@@ -605,7 +607,7 @@ Theorem transl_init_single_steps:
   forall ty a data f m v1 ty1 m' v chunk b ofs m'',
   transl_init_single ge ty a = OK data ->
   star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
-  sem_cast v1 ty1 ty = Some v ->
+  sem_cast v1 ty1 ty m' = Some v ->
   access_mode ty = By_value chunk ->
   Mem.store chunk m' b ofs v = Some m'' ->
   Genv.store_init_data ge m b ofs data = Some m''.
@@ -647,7 +649,7 @@ Qed.
 Lemma transl_init_single_size:
   forall ty a data,
   transl_init_single ge ty a = OK data ->
-  Genv.init_data_size data = sizeof ge ty.
+  init_data_size data = sizeof ge ty.
 Proof.
   intros. monadInv H. destruct x0.
 - monadInv EQ2.
@@ -664,7 +666,7 @@ Proof.
   inv EQ2; auto.
 Qed.
 
-Notation idlsize := Genv.init_data_list_size.
+Notation idlsize := init_data_list_size.
 
 Remark padding_size:
   forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.
@@ -760,7 +762,7 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
   | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'',
       star step ge (ExprState dummy_function a Kstop empty_env m)
                 E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') ->
-      sem_cast v1 ty1 ty = Some v ->
+      sem_cast v1 ty1 ty m' = Some v ->
       access_mode ty = By_value chunk ->
       Mem.store chunk m' b ofs v = Some m'' ->
       exec_init m b ofs ty (Init_single a) m''
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index b8a2cb8d..e08411a5 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -80,9 +80,9 @@ let rec expr p (prec, e) =
   | Econst_int(n, _) ->
       fprintf p "%ld" (camlint_of_coqint n)
   | Econst_float(f, _) ->
-      fprintf p "%F" (camlfloat_of_coqfloat f)
+      fprintf p "%.15F" (camlfloat_of_coqfloat f)
   | Econst_single(f, _) ->
-      fprintf p "%Ff" (camlfloat_of_coqfloat32 f)
+      fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f)
   | Econst_long(n, Tlong(Unsigned, _)) ->
       fprintf p "%LuLLU" (camlint64_of_coqint n)
   | Econst_long(n, _) ->
@@ -254,10 +254,10 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | Clight.External(EF_external(_,_), args, res, cconv) ->
+  | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
                 (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
-  | Clight.External(_, _, _, _) ->
+  | Ctypes.External(_, _, _, _) ->
       ()
   | Internal f ->
       print_function p id f
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index d518d6bb..4287f7f9 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -179,9 +179,9 @@ let print_typed_value p v ty =
   | Vint n, _ ->
       fprintf p "%ld" (camlint_of_coqint n)
   | Vfloat f, _ ->
-      fprintf p "%F" (camlfloat_of_coqfloat f)
+      fprintf p "%.15F" (camlfloat_of_coqfloat f)
   | Vsingle f, _ ->
-      fprintf p "%Ff" (camlfloat_of_coqfloat32 f)
+      fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f)
   | Vlong n, Tlong(Unsigned, _) ->
       fprintf p "%LuLLU" (camlint64_of_coqint n)
   | Vlong n, _ ->
@@ -261,6 +261,8 @@ let rec expr p (prec, e) =
                 (camlstring_of_coqstring txt) exprlist (false, args)
   | Ebuiltin(EF_external(id, sg), _, args, _) ->
       fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
+  | Ebuiltin(EF_runtime(id, sg), _, args, _) ->
+      fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
   | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
       extended_asm p txt None args clob
   | Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
@@ -424,12 +426,12 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | Csyntax.External(EF_external(_,_), args, res, cconv) ->
+  | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
                 (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
-  | Csyntax.External(_, _, _, _) ->
+  | Ctypes.External(_, _, _, _) ->
       ()
-  | Csyntax.Internal f ->
+  | Ctypes.Internal f ->
       print_function p id f
 
 let string_of_init id =
@@ -454,8 +456,8 @@ let print_init p = function
   | Init_int16 n -> fprintf p "%ld" (camlint_of_coqint n)
   | Init_int32 n -> fprintf p "%ld" (camlint_of_coqint n)
   | Init_int64 n -> fprintf p "%LdLL" (camlint64_of_coqint n)
-  | Init_float32 n -> fprintf p "%F" (camlfloat_of_coqfloat n)
-  | Init_float64 n -> fprintf p "%F" (camlfloat_of_coqfloat n)
+  | Init_float32 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n)
+  | Init_float64 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n)
   | Init_space n -> fprintf p "/* skip %ld */@ " (camlint_of_coqint n)
   | Init_addrof(symb, ofs) ->
       let ofs = camlint_of_coqint ofs in
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index a5a6ad66..bfdd8ab9 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -114,7 +114,7 @@ Fixpoint eval_simpl_expr (a: expr) : option val :=
   | Ecast b ty =>
       match eval_simpl_expr b with
       | None => None
-      | Some v => sem_cast v (typeof b) ty
+      | Some v => sem_cast v (typeof b) ty Mem.empty
       end
   | _ => None
   end.
@@ -327,10 +327,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       let ty2 := Csyntax.typeof r2 in
       match dst with
       | For_val | For_set _ =>
-          do t <- gensym ty2;
+          do t <- gensym ty1;
           ret (finish dst
-                 (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil)
-                 (Ecast (Etempvar t ty2) ty1))
+                 (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign a1 (Etempvar t ty1) :: nil)
+                 (Etempvar t ty1))
       | For_effects =>
           ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil,
                dummy_expr)
@@ -342,12 +342,12 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       do (sl3, a3) <- transl_valof ty1 a1;
       match dst with
       | For_val | For_set _ =>
-          do t <- gensym tyres;
+          do t <- gensym ty1;
           ret (finish dst
                  (sl1 ++ sl2 ++ sl3 ++
-                  Sset t (Ebinop op a3 a2 tyres) ::
-                  make_assign a1 (Etempvar t tyres) :: nil)
-                 (Ecast (Etempvar t tyres) ty1))
+                  Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
+                  make_assign a1 (Etempvar t ty1) :: nil)
+                 (Etempvar t ty1))
       | For_effects =>
           ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil,
                dummy_expr)
@@ -512,9 +512,9 @@ Local Open Scope error_monad_scope.
 
 Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
   match fd with
-  | Csyntax.Internal f =>
+  | Internal f =>
       do tf <- transl_function f; OK (Internal tf)
-  | Csyntax.External ef targs tres cc =>
+  | External ef targs tres cc =>
       OK (External ef targs tres cc)
   end.
 
@@ -523,6 +523,6 @@ Definition transl_program (p: Csyntax.program) : res program :=
   OK {| prog_defs := AST.prog_defs p1;
         prog_public := AST.prog_public p1;
         prog_main := AST.prog_main p1;
-        prog_types := Csyntax.prog_types p;
-        prog_comp_env := Csyntax.prog_comp_env p;
-        prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}.
+        prog_types := prog_types p;
+        prog_comp_env := prog_comp_env p;
+        prog_comp_env_eq := prog_comp_env_eq p |}.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 0c7c9ce7..64e52df8 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -12,30 +12,34 @@
 
 (** Correctness proof for expression simplification. *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Errors.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Smallstep.
-Require Import Globalenvs.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
-Require Import Cstrategy.
-Require Import Clight.
-Require Import SimplExpr.
-Require Import SimplExprspec.
+Require Import Coqlib Maps Errors Integers.
+Require Import AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Ctypes Cop Csyntax Csem Cstrategy Clight.
+Require Import SimplExpr SimplExprspec.
+
+(** ** Relational specification of the translation. *)
+
+Definition match_prog (p: Csyntax.program) (tp: Clight.program) :=
+    match_program (fun ctx f tf => tr_fundef f tf) eq p tp
+ /\ prog_types tp = prog_types p.
+
+Lemma transf_program_match:
+  forall p tp, transl_program p = OK tp -> match_prog p tp.
+Proof.
+  unfold transl_program; intros. monadInv H. split; auto.
+  unfold program_of_program; simpl. destruct x; simpl.
+  eapply match_transform_partial_program_contextual. eexact EQ. 
+  intros. apply transl_fundef_spec; auto. 
+Qed.
+
+(** ** Semantic preservation *)
 
 Section PRESERVATION.
 
 Variable prog: Csyntax.program.
 Variable tprog: Clight.program.
-Hypothesis TRANSL: transl_program prog = OK tprog.
+Hypothesis TRANSL: match_prog prog tprog.
 
 Let ge := Csem.globalenv prog.
 Let tge := Clight.globalenv tprog.
@@ -45,22 +49,17 @@ Let tge := Clight.globalenv tprog.
 Lemma comp_env_preserved:
   Clight.genv_cenv tge = Csem.genv_cenv ge.
 Proof.
-  monadInv TRANSL. unfold tge; rewrite <- H0; auto.
+  simpl. destruct TRANSL. generalize (prog_comp_env_eq tprog) (prog_comp_env_eq prog). 
+  congruence.
 Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros. eapply Genv.find_symbol_match. eapply transl_program_spec; eauto.
-  simpl. tauto.
-Qed.
+Proof (Genv.find_symbol_match (proj1 TRANSL)).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof.
-  intros. eapply Genv.public_symbol_match. eapply transl_program_spec; eauto.
-  simpl. tauto.
-Qed.
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match (proj1 TRANSL)).
 
 Lemma function_ptr_translated:
   forall b f,
@@ -68,9 +67,8 @@ Lemma function_ptr_translated:
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ tr_fundef f tf.
 Proof.
-  intros. eapply Genv.find_funct_ptr_match.
-  eapply transl_program_spec; eauto.
-  assumption.
+  intros.
+  edestruct (Genv.find_funct_ptr_match (proj1 TRANSL)) as (ctx & tf & A & B & C); eauto.
 Qed.
 
 Lemma functions_translated:
@@ -79,27 +77,8 @@ Lemma functions_translated:
   exists tf,
   Genv.find_funct tge v = Some tf /\ tr_fundef f tf.
 Proof.
-  intros. eapply Genv.find_funct_match.
-  eapply transl_program_spec; eauto.
-  assumption.
-Qed.
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  intros. destruct (Genv.find_var_info ge b) as [v|] eqn:V.
-- exploit Genv.find_var_info_match. eapply transl_program_spec; eauto. eassumption.
-  intros [tv [A B]]. inv B. assumption.
-- destruct (Genv.find_var_info tge b) as [v'|] eqn:V'; auto.
-  exploit Genv.find_var_info_rev_match. eapply transl_program_spec; eauto. eassumption.
-  simpl. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try tauto.
-  intros [v [A B]]. inv B. change (Genv.globalenv prog) with (Csem.genv_genv ge) in A. congruence.
-Qed.
-
-Lemma block_is_volatile_preserved:
-  forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b.
-Proof.
-  intros. unfold Genv.block_is_volatile. rewrite varinfo_preserved. auto.
+  intros.
+  edestruct (Genv.find_funct_match (proj1 TRANSL)) as (ctx & tf & A & B & C); eauto.
 Qed.
 
 Lemma type_of_fundef_preserved:
@@ -167,8 +146,7 @@ Proof.
   (* By_value, not volatile *)
   rewrite H1. split; auto. eapply deref_loc_value; eauto.
   (* By_value, volatile *)
-  rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto.
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved.
+  rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto. apply senv_preserved.
   (* By reference *)
   rewrite H0. destruct (type_is_volatile ty); split; auto; eapply deref_loc_reference; eauto.
   (* By copy *)
@@ -187,8 +165,7 @@ Proof.
   (* By_value, not volatile *)
   rewrite H1. split; auto. eapply assign_loc_value; eauto.
   (* By_value, volatile *)
-  rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto.
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved.
+  rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto. apply senv_preserved.
   (* By copy *)
   rewrite H0. rewrite <- comp_env_preserved in *.
   destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto.
@@ -752,12 +729,27 @@ Qed.
 
 (** Semantics of smart constructors *)
 
+Remark sem_cast_deterministic:
+  forall v ty ty' m1 v1 m2 v2,
+  sem_cast v ty ty' m1 = Some v1 ->
+  sem_cast v ty ty' m2 = Some v2 ->
+  v1 = v2.
+Proof.
+  unfold sem_cast; intros. destruct (classify_cast ty ty'); try congruence.
+  destruct v; try congruence.
+  destruct (Mem.weak_valid_pointer m1 b (Int.unsigned i)); inv H.
+  destruct (Mem.weak_valid_pointer m2 b (Int.unsigned i)); inv H0.
+  auto.
+Qed.
+
 Lemma eval_simpl_expr_sound:
   forall e le m a v, eval_expr tge e le m a v ->
   match eval_simpl_expr a with Some v' => v' = v | None => True end.
 Proof.
   induction 1; simpl; auto.
-  destruct (eval_simpl_expr a); auto. subst. rewrite H0. auto.
+  destruct (eval_simpl_expr a); auto. subst.
+  destruct (sem_cast v1 (typeof a) ty Mem.empty) as [v'|] eqn:C; auto.
+  eapply sem_cast_deterministic; eauto.
   inv H; simpl; auto.
 Qed.
 
@@ -811,7 +803,7 @@ Lemma step_make_assign:
   Csem.assign_loc ge ty m b ofs v t m' ->
   eval_lvalue tge e le m a1 b ofs ->
   eval_expr tge e le m a2 v2 ->
-  sem_cast v2 (typeof a2) ty = Some v ->
+  sem_cast v2 (typeof a2) ty m = Some v ->
   typeof a1 = ty ->
   step1 tge (State f (make_assign a1 a2) k e le m)
           t (State f Sskip k e le m').
@@ -1649,18 +1641,19 @@ Proof.
   (* for value *)
   exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
   exploit tr_simple_lvalue. eauto.
-    eapply tr_expr_invariant with (le' := PTree.set t0 v le). eauto.
+    eapply tr_expr_invariant with (le' := PTree.set t0 v' le). eauto.
     intros. apply PTree.gso. intuition congruence.
   intros [SL1 [TY1 EV1]].
   subst; simpl Kseqlist.
   econstructor; split.
   left. eapply plus_left. constructor.
-  eapply star_left. constructor. eauto.
+  eapply star_left. constructor. econstructor. eauto. rewrite <- TY2; eauto. 
   eapply star_left. constructor.
   apply star_one. eapply step_make_assign; eauto.
-  constructor. apply PTree.gss. reflexivity. reflexivity. traceEq.
+  constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. 
+  reflexivity. reflexivity. traceEq.
   econstructor. auto. apply S.
-  apply tr_val_gen. auto. intros. econstructor; eauto. constructor.
+  apply tr_val_gen. auto. intros. constructor.
   rewrite H4; auto. apply PTree.gss.
   intros. apply PTree.gso. intuition congruence.
   auto. auto.
@@ -1692,7 +1685,7 @@ Proof.
   exploit tr_simple_rvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto.
   intros. apply INV. NOTIN. simpl. intros [SL2 [TY2 EV2]].
   exploit tr_simple_lvalue. eauto.
-    eapply tr_expr_invariant with (le := le) (le' := PTree.set t v3 le'). eauto.
+    eapply tr_expr_invariant with (le := le) (le' := PTree.set t v4 le'). eauto.
     intros. rewrite PTree.gso. apply INV. NOTIN. intuition congruence.
   intros [? [? EV1'']].
   subst; simpl Kseqlist.
@@ -1700,13 +1693,14 @@ Proof.
   left. rewrite app_ass. rewrite Kseqlist_app.
   eapply star_plus_trans. eexact EXEC.
   simpl. eapply plus_four. econstructor. econstructor.
-    econstructor. eexact EV3. eexact EV2.
+    econstructor. econstructor. eexact EV3. eexact EV2.
     rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; eauto.
+    eassumption.
   econstructor. eapply step_make_assign; eauto.
-    constructor. apply PTree.gss.
+    constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto.
     reflexivity. traceEq.
   econstructor. auto. apply S.
-  apply tr_val_gen. auto. intros. econstructor; eauto. constructor.
+  apply tr_val_gen. auto. intros. constructor.
   rewrite H10; auto. apply PTree.gss.
   intros. rewrite PTree.gso. apply INV.
   red; intros; elim H10; auto.
@@ -1890,8 +1884,7 @@ Proof.
   econstructor; split.
   left. eapply plus_left. constructor.  apply star_one.
   econstructor; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   traceEq.
   econstructor; eauto.
   change sl2 with (nil ++ sl2). apply S. constructor. simpl; auto. auto.
@@ -1901,8 +1894,7 @@ Proof.
   econstructor; split.
   left. eapply plus_left. constructor. apply star_one.
   econstructor; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   traceEq.
   econstructor; eauto.
   change sl2 with (nil ++ sl2). apply S.
@@ -2198,8 +2190,7 @@ Proof.
   inv H5.
   econstructor; split.
   left; apply plus_one. econstructor; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   constructor; auto.
 
 (* return *)
@@ -2229,15 +2220,14 @@ Lemma transl_initial_states:
   Csem.initial_state prog S ->
   exists S', Clight.initial_state tprog S' /\ match_states S S'.
 Proof.
-  intros. inv H. generalize TRANSL; intros TR; monadInv TR. rewrite H4.
-  exploit transl_program_spec; eauto. intros MP.
+  intros. inv H.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor.
-  exploit Genv.init_mem_match; eauto.
-  change (Genv.globalenv tprog) with (genv_genv tge).
-  rewrite symbols_preserved. rewrite <- H4; simpl.
-  rewrite (transform_partial_program_main _ _ EQ). eauto. 
+  eapply (Genv.init_mem_match (proj1 TRANSL)); eauto.
+  replace (prog_main tprog) with (prog_main prog).
+  rewrite symbols_preserved. eauto. 
+  destruct TRANSL. destruct H as (A & B & C). simpl in B. auto. 
   eexact FIND.
   rewrite <- H3. apply type_of_fundef_preserved. auto.
   constructor. auto. constructor.
@@ -2254,7 +2244,7 @@ Theorem transl_program_correct:
   forward_simulation (Cstrategy.semantics prog) (Clight.semantics1 tprog).
 Proof.
   eapply forward_simulation_star_wf with (order := ltof _ measure).
-  eexact public_preserved.
+  eapply senv_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
   apply well_founded_ltof.
@@ -2262,3 +2252,18 @@ Proof.
 Qed.
 
 End PRESERVATION.
+
+(** ** Commutation with linking *)
+
+Instance TransfSimplExprLink : TransfLink match_prog.
+Proof.
+  red; intros. eapply Ctypes.link_match_program; eauto. 
+- intros.
+Local Transparent Linker_fundef.
+  simpl in *; unfold link_fundef in *. inv H3; inv H4; try discriminate.
+  destruct ef; inv H2. exists (Internal tf); split; auto. constructor; auto.
+  destruct ef; inv H2. exists (Internal tf); split; auto. constructor; auto.
+  destruct (external_function_eq ef ef0 && typelist_eq targs targs0 &&
+            type_eq tres tres0 && calling_convention_eq cconv cconv0); inv H2.
+  exists (External ef targs tres cconv); split; auto. constructor.
+Qed.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 4077d7df..453a4c9a 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -12,18 +12,9 @@
 
 (** Relational specification of expression simplification. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Memory.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Clight.
-Require Import SimplExpr.
+Require Import Coqlib Maps Errors Integers Floats.
+Require Import AST Linking Memory.
+Require Import Ctypes Cop Csyntax Clight SimplExpr.
 
 Section SPEC.
 
@@ -222,10 +213,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       ty2 = Csyntax.typeof e2 ->
       tr_expr le dst (Csyntax.Eassign e1 e2 ty)
                    (sl1 ++ sl2 ++
-                    Sset t a2 ::
-                    make_assign a1 (Etempvar t ty2) ::
-                    final dst (Ecast (Etempvar t ty2) ty1))
-                   (Ecast (Etempvar t ty2) ty1) tmp
+                    Sset t (Ecast a2 ty1) ::
+                    make_assign a1 (Etempvar t ty1) ::
+                    final dst (Etempvar t ty1))
+                   (Etempvar t ty1) tmp
   | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
@@ -246,10 +237,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       ty1 = Csyntax.typeof e1 ->
       tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty)
                    (sl1 ++ sl2 ++ sl3 ++
-                    Sset t (Ebinop op a3 a2 tyres) ::
-                    make_assign a1 (Etempvar t tyres) ::
-                    final dst (Ecast (Etempvar t tyres) ty1))
-                   (Ecast (Etempvar t tyres) ty1) tmp
+                    Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
+                    make_assign a1 (Etempvar t ty1) ::
+                    final dst (Etempvar t ty1))
+                   (Etempvar t ty1) tmp
   | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_rvalof ty1 a1 sl2 a2 tmp2 ->
@@ -375,8 +366,7 @@ Qed.
   between Csyntax values and Cminor expressions: in the case of
   [tr_expr], the Cminor expression must not depend on memory,
   while in the case of [tr_top] it can depend on the current memory
-  state.  This special case is extended to values occurring under
-  one or several [Csyntax.Eparen]. *)
+  state. *)
 
 Section TR_TOP.
 
@@ -389,19 +379,9 @@ Inductive tr_top: destination -> Csyntax.expr -> list statement -> expr -> list
   | tr_top_val_val: forall v ty a tmp,
       typeof a = ty -> eval_expr ge e le m a v ->
       tr_top For_val (Csyntax.Eval v ty) nil a tmp
-(*
-  | tr_top_val_set: forall t tyl v ty a any tmp,
-      typeof a = ty -> eval_expr ge e le m a v ->
-      tr_top (For_set tyl t) (Csyntax.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp
-*)
   | tr_top_base: forall dst r sl a tmp,
       tr_expr le dst r sl a tmp ->
       tr_top dst r sl a tmp.
-(*
-  | tr_top_paren_test: forall tyl t r ty sl a tmp,
-      tr_top (For_set (ty :: tyl) t) r sl a tmp ->
-      tr_top (For_set tyl t) (Csyntax.Eparen r ty) sl a tmp.
-*)
 
 End TR_TOP.
 
@@ -1088,8 +1068,7 @@ Opaque transl_expression transl_expr_stmt.
   monadInv TR; constructor; eauto.
 Qed.
 
-(** Relational presentation for the transformation of functions, fundefs, and va
-riables. *)
+(** Relational presentation for the transformation of functions, fundefs, and variables. *)
 
 Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
   | tr_function_intro: forall f tf,
@@ -1103,9 +1082,9 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
 Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
   | tr_internal: forall f tf,
       tr_function f tf ->
-      tr_fundef (Csyntax.Internal f) (Clight.Internal tf)
+      tr_fundef (Internal f) (Internal tf)
   | tr_external: forall ef targs tres cconv,
-      tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv).
+      tr_fundef (External ef targs tres cconv) (External ef targs tres cconv).
 
 Lemma transl_function_spec:
   forall f tf,
@@ -1128,30 +1107,5 @@ Proof.
 + constructor.
 Qed.
 
-Lemma transl_globdefs_spec:
-  forall l l',
-  transf_globdefs transl_fundef (fun v : type => OK v) l = OK l' ->
-  list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'.
-Proof.
-  induction l; simpl; intros.
-- inv H. constructor.
-- destruct a as [id gd]. destruct gd.
-  + destruct (transl_fundef f) as [tf | ?] eqn:E1; Errors.monadInv H.
-    constructor; eauto. constructor. eapply transl_fundef_spec; eauto.
-  + Errors.monadInv H. 
-    constructor; eauto. destruct v; constructor; auto.
-Qed.
-
-Theorem transl_program_spec:
-  forall p tp,
-  transl_program p = OK tp ->
-  match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp.
-Proof.
-  unfold transl_program, transform_partial_program; intros. Errors.monadInv H. Errors.monadInv EQ; simpl.
-  split; auto. exists x0; split.
-  eapply transl_globdefs_spec; eauto.
-  rewrite <- app_nil_end; auto.
-Qed.
-
 End SPEC.
 
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index c4b1054d..580f02c2 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -15,13 +15,9 @@
 
 Require Import FSets.
 Require FSetAVL.
-Require Import Coqlib.
-Require Import Ordered.
-Require Import Errors.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
+Require Import Coqlib Ordered Errors.
+Require Import AST Linking.
+Require Import Ctypes Cop Clight.
 Require Compopts.
 
 Open Scope error_monad_scope.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index a47036bf..2cd82d8f 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -13,80 +13,58 @@
 (** Semantic preservation for the SimplLocals pass. *)
 
 Require Import FSets.
-Require FSetAVL.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Ordered.
-Require Import AST.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Smallstep.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
-Require Import SimplLocals.
+Require Import Coqlib Errors Ordered Maps Integers Floats.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Ctypes Cop Clight SimplLocals.
 
 Module VSF := FSetFacts.Facts(VSet).
 Module VSP := FSetProperties.Properties(VSet).
 
+Definition match_prog (p tp: program) : Prop :=
+    match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp
+ /\ prog_types tp = prog_types p.
+
+Lemma match_transf_program:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  unfold transf_program; intros. monadInv H. 
+  split; auto. apply match_transform_partial_program. rewrite EQ. destruct x; auto.
+Qed.
+
 Section PRESERVATION.
 
 Variable prog: program.
 Variable tprog: program.
-Hypothesis TRANSF: transf_program prog = OK tprog.
+Hypothesis TRANSF: match_prog prog tprog.
 Let ge := globalenv prog.
 Let tge := globalenv tprog.
 
 Lemma comp_env_preserved:
   genv_cenv tge = genv_cenv ge.
 Proof.
-  monadInv TRANSF. unfold tge; rewrite <- H0; auto.
-Qed.
-
-Lemma transf_programs:
-  AST.transform_partial_program transf_fundef (program_of_program prog) = OK (program_of_program tprog).
-Proof.
-  monadInv TRANSF. rewrite EQ. destruct x; reflexivity.
+  unfold tge, ge. destruct prog, tprog; simpl. destruct TRANSF as [_ EQ]. simpl in EQ. congruence.
 Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  exact (Genv.find_symbol_transf_partial _ _ transf_programs).
-Qed.
+Proof (Genv.find_symbol_match (proj1 TRANSF)).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof.
-  exact (Genv.public_symbol_transf_partial _ _ transf_programs).
-Qed.
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  exact (Genv.find_var_info_transf_partial _ _ transf_programs).
-Qed.
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match (proj1 TRANSF)).
 
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
   exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof.
-  exact (Genv.find_funct_transf_partial _ _ transf_programs).
-Qed.
+Proof (Genv.find_funct_transf_partial (proj1 TRANSF)).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof.
-  exact (Genv.find_funct_ptr_transf_partial _ _ transf_programs).
-Qed.
+Proof (Genv.find_funct_ptr_transf_partial (proj1 TRANSF)).
 
 Lemma type_of_fundef_preserved:
   forall fd tfd,
@@ -201,97 +179,7 @@ Proof.
   xomegaContradiction.
 Qed.
 
-(** Properties of values obtained by casting to a given type. *)
-
-Inductive val_casted: val -> type -> Prop :=
-  | val_casted_int: forall sz si attr n,
-      cast_int_int sz si n = n ->
-      val_casted (Vint n) (Tint sz si attr)
-  | val_casted_float: forall attr n,
-       val_casted (Vfloat n) (Tfloat F64 attr)
-  | val_casted_single: forall attr n,
-       val_casted (Vsingle n) (Tfloat F32 attr)
-  | val_casted_long: forall si attr n,
-      val_casted (Vlong n) (Tlong si attr)
-  | val_casted_ptr_ptr: forall b ofs ty attr,
-      val_casted (Vptr b ofs) (Tpointer ty attr)
-  | val_casted_int_ptr: forall n ty attr,
-      val_casted (Vint n) (Tpointer ty attr)
-  | val_casted_ptr_int: forall b ofs si attr,
-      val_casted (Vptr b ofs) (Tint I32 si attr)
-  | val_casted_struct: forall id attr b ofs,
-      val_casted (Vptr b ofs) (Tstruct id attr)
-  | val_casted_union: forall id attr b ofs,
-      val_casted (Vptr b ofs) (Tunion id attr)
-  | val_casted_void: forall v,
-      val_casted v Tvoid.
-
-Remark cast_int_int_idem:
-  forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i.
-Proof.
-  intros. destruct sz; simpl; auto.
-  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
-  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
-  destruct (Int.eq i Int.zero); auto.
-Qed.
-
-Lemma cast_val_is_casted:
-  forall v ty ty' v', sem_cast v ty ty' = Some v' -> val_casted v' ty'.
-Proof.
-  unfold sem_cast; intros. destruct ty'; simpl in *.
-(* void *)
-  constructor.
-(* int *)
-  destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H.
-  constructor. apply (cast_int_int_idem I8 s).
-  constructor. apply (cast_int_int_idem I8 s).
-  destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s).
-  destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s).
-  constructor. apply (cast_int_int_idem I16 s).
-  constructor. apply (cast_int_int_idem I16 s).
-  destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s).
-  destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s).
-  constructor. auto.
-  constructor.
-  constructor. auto.
-  destruct (cast_single_int s f); inv H1. constructor. auto.
-  destruct (cast_float_int s f); inv H1. constructor; auto.
-  constructor; auto.
-  constructor.
-  constructor; auto.
-  constructor.
-  constructor; auto.
-  constructor.
-  constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
-  constructor. simpl. destruct (Int64.eq i Int64.zero); auto.
-  constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto.
-  constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto.
-  constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor. simpl. destruct (Int.eq i Int.zero); auto.
-(* long *)
-  destruct ty; try (destruct f); try discriminate.
-  destruct v; inv H. constructor.
-  destruct v; inv H. constructor.
-  destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor.
-  destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor.
-  destruct v; inv H. constructor.
-  destruct v; inv H. constructor.
-  destruct v; inv H. constructor.
-(* float *)
-  destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor.
-(* pointer *)
-  destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor.
-(* impossible cases *)
-  discriminate.
-  discriminate.
-(* structs *)
-  destruct ty; try discriminate; destruct v; try discriminate.
-  destruct (ident_eq i0 i); inv H; constructor.
-(* unions *)
-  destruct ty; try discriminate; destruct v; try discriminate.
-  destruct (ident_eq i0 i); inv H; constructor.
-Qed.
+(** Properties of values resulting from a cast *)
 
 Lemma val_casted_load_result:
   forall v ty chunk,
@@ -316,15 +204,6 @@ Proof.
   discriminate.
 Qed.
 
-Lemma cast_val_casted:
-  forall v ty, val_casted v ty -> sem_cast v ty ty = Some v.
-Proof.
-  intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto.
-  destruct sz; congruence.
-  unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
-  unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
-Qed.
-
 Lemma val_casted_inject:
   forall f v v' ty,
   Val.inject f v v' -> val_casted v ty -> val_casted v' ty.
@@ -363,7 +242,7 @@ Qed.
 Lemma make_cast_correct:
   forall e le m a v1 tto v2,
   eval_expr tge e le m a v1 ->
-  sem_cast v1 (typeof a) tto = Some v2 ->
+  sem_cast v1 (typeof a) tto m = Some v2 ->
   eval_expr tge e le m (make_cast a tto) v2.
 Proof.
   intros.
@@ -386,9 +265,9 @@ Qed.
 (** Debug annotations. *)
 
 Lemma cast_typeconv:
-  forall v ty,
+  forall v ty m,
   val_casted v ty ->
-  sem_cast v ty (typeconv ty) = Some v.
+  sem_cast v ty (typeconv ty) m = Some v.
 Proof.
   induction 1; simpl; auto.
 - destruct sz; auto.
@@ -423,7 +302,7 @@ Qed.
 Lemma step_Sset_debug:
   forall f id ty a k e le m v v',
   eval_expr tge e le m a v ->
-  sem_cast v (typeof a) ty = Some v' ->
+  sem_cast v (typeof a) ty m = Some v' ->
   plus step2 tge (State f (Sset_debug id ty a) k e le m)
               E0 (State f Sskip k e (PTree.set id v' le) m).
 Proof.
@@ -2172,8 +2051,7 @@ Proof.
   exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat.
   intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
   econstructor; split.
-  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto with compat.
   eapply match_envs_set_opttemp; eauto.
   eapply match_envs_extcall; eauto.
@@ -2334,8 +2212,7 @@ Proof.
   eapply match_cont_globalenv. eexact (MCONT VSet.empty).
   intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
   econstructor; split.
-  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
   intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_cont_extcall; eauto. xomega. xomega.
@@ -2358,10 +2235,10 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   econstructor; split.
   econstructor.
-  eapply Genv.init_mem_transf_partial. eexact transf_programs. eauto.
-  change (prog_main tprog) with (AST.prog_main tprog).
-  rewrite (transform_partial_program_main _ _ transf_programs).
+  eapply (Genv.init_mem_transf_partial (proj1 TRANSF)). eauto.
+  replace (prog_main tprog) with (prog_main prog). 
   instantiate (1 := b). rewrite <- H1. apply symbols_preserved.
+  generalize (match_program_main (proj1 TRANSF)). simpl; auto.
   eauto.
   rewrite <- H3; apply type_of_fundef_preserved; auto.
   econstructor; eauto.
@@ -2391,10 +2268,27 @@ Theorem transf_program_correct:
   forward_simulation (semantics1 prog) (semantics2 tprog).
 Proof.
   eapply forward_simulation_plus.
-  eexact public_preserved.
+  apply senv_preserved.
   eexact initial_states_simulation.
   eexact final_states_simulation.
   eexact step_simulation.
 Qed.
 
 End PRESERVATION.
+
+(** ** Commutation with linking *)
+
+Instance TransfSimplLocalsLink : TransfLink match_prog.
+Proof.
+  red; intros. eapply Ctypes.link_match_program; eauto. 
+- intros.
+Local Transparent Linker_fundef.
+  simpl in *; unfold link_fundef in *.
+  destruct f1; monadInv H3; destruct f2; monadInv H4; try discriminate.
+  destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto.
+  destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto.
+  destruct (external_function_eq e e0 && typelist_eq t t1 &&
+            type_eq t0 t2 && calling_convention_eq c c0); inv H2.
+  econstructor; split; eauto. 
+Qed.
+