Represent struct and union types by name instead of by structure.

20 files changed, 1518 insertions, 1308 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 4d5d6c07..ea278ac1 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -100,6 +100,10 @@ let atom_location a =
   with Not_found ->
     Cutil.no_loc
 
+(** The current environment of composite definitions *)
+
+let comp_env : composite_env ref = ref Maps.PTree.empty
+
 (** Hooks -- overriden in machine-dependent CPragmas module *)
 
 let process_pragma_hook = ref (fun (s: string) -> false)
@@ -243,12 +247,12 @@ let make_builtin_memcpy args =
   match args with
   | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) ->
       let sz1 =
-        match Initializers.constval sz with
+        match Initializers.constval !comp_env sz with
         | Errors.OK(Vint n) -> n
         | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be 
 a constant)"; Integers.Int.zero in
       let al1 =
-        match Initializers.constval al with
+        match Initializers.constval !comp_env al with
         | Errors.OK(Vint n) -> n
         | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be 
 a constant)"; Integers.Int.one in
@@ -270,7 +274,7 @@ let va_list_ptr e =
 let make_builtin_va_arg env ty e =
   let (helper, ty_ret) =
     match ty with
-    | Tint _ | Tpointer _ | Tcomp_ptr _ ->
+    | Tint _ | Tpointer _ ->
         ("__compcert_va_int32", Tint(I32, Unsigned, noattr))
     | Tlong _ ->
         ("__compcert_va_int64", Tlong(Unsigned, noattr))
@@ -303,27 +307,6 @@ let convertAttr a =
       let n = Cutil.alignas_attribute a in
       if n > 0 then Some (N.of_int (log2 n)) else None }
 
-let mergeAttr a1 a2 =
-  { attr_volatile = a1.attr_volatile || a2.attr_volatile;
-    attr_alignas =
-      match a1.attr_alignas, a2.attr_alignas with
-      | None, aa -> aa
-      | aa, None -> aa
-      | Some n1, Some n2 -> Some (if N.le n1 n2 then n1 else n2) }
-
-let mergeTypAttr ty a2 =
-  match ty with
-  | Tvoid -> ty
-  | Tint(sz, sg, a1) -> Tint(sz, sg, mergeAttr a1 a2)
-  | Tfloat(sz, a1) -> Tfloat(sz, mergeAttr a1 a2)
-  | Tlong(sg, a1) -> Tlong(sg, mergeAttr a1 a2)
-  | Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2)
-  | Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2)
-  | Tfunction(targs, tres, cc) -> ty
-  | Tstruct(id, fld, a1) -> Tstruct(id, fld, mergeAttr a1 a2)
-  | Tunion(id, fld, a1) -> Tunion(id, fld, mergeAttr a1 a2)
-  | Tcomp_ptr(id, a1) -> Tcomp_ptr(id, mergeAttr a1 a2)
-
 let convertCallconv va attr =
   let sr =
     Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in
@@ -353,93 +336,48 @@ let convertFkind = function
       if not !Clflags.option_flongdouble then unsupported "'long double' type"; 
       F64
 
-(** A cache for structs and unions already converted *)
-
-let compositeCache : (C.ident, coq_type) Hashtbl.t = Hashtbl.create 77
-
-let convertTyp env t =
-
-  let rec convertTyp seen t =
-    match Cutil.unroll env t with
-    | C.TVoid a -> Tvoid
-    | C.TInt(C.ILongLong, a) ->
-        Tlong(Signed, convertAttr a)
-    | C.TInt(C.IULongLong, a) ->
-        Tlong(Unsigned, convertAttr a)
-    | C.TInt(ik, a) ->
-        let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a)
-    | C.TFloat(fk, a) ->
-        Tfloat(convertFkind fk, convertAttr a)
-    | C.TPtr(ty, a) ->
-        begin match Cutil.unroll env ty with
-        | C.TStruct(id, _) when List.mem id seen ->
-            Tcomp_ptr(intern_string ("struct " ^ id.name), convertAttr a)
-        | C.TUnion(id, _) when List.mem id seen ->
-            Tcomp_ptr(intern_string ("union " ^ id.name), convertAttr a)
-        | _ ->
-            Tpointer(convertTyp seen ty, convertAttr a)
-        end
-    | C.TArray(ty, None, a) ->
-        (* Cparser verified that the type ty[] occurs only in
-           contexts that are safe for Clight, so just treat as ty[0]. *)
-        (* warning "array type of unspecified size"; *)
-        Tarray(convertTyp seen ty, coqint_of_camlint 0l, convertAttr a)
-    | C.TArray(ty, Some sz, a) ->
-        Tarray(convertTyp seen ty, convertInt sz, convertAttr a)
-    | C.TFun(tres, targs, va, a) ->
-        if Cutil.is_composite_type env tres then
-          unsupported "return type is a struct or union (consider adding option -fstruct-return)";
-        Tfunction(begin match targs with
-                  | None -> Tnil
-                  | Some tl -> convertParams seen tl
-                  end,
-                  convertTyp seen tres,
-                  convertCallconv va a)
-    | C.TNamed _ ->
-        assert false
-    | C.TStruct(id, a) ->
-        let a' = convertAttr a in
-        begin try
-          merge_attributes (Hashtbl.find compositeCache id) a'
-        with Not_found ->
-          let flds =
-            try
-              convertFields (id :: seen) (Env.find_struct env id)
-            with Env.Error e ->
-              error (Env.error_message e); Fnil in
-          Tstruct(intern_string("struct " ^ id.name), flds, a')
-        end
-    | C.TUnion(id, a) ->
-        let a' = convertAttr a in
-        begin try
-          merge_attributes (Hashtbl.find compositeCache id) a'
-        with Not_found ->
-          let flds =
-            try
-              convertFields (id :: seen) (Env.find_union env id)
-            with Env.Error e ->
-              error (Env.error_message e); Fnil in
-          Tunion(intern_string("union " ^ id.name), flds, a')
-        end
-    | C.TEnum(id, a) ->
-        let (sg, sz) = convertIkind Cutil.enum_ikind in
-        Tint(sz, sg, convertAttr a)
-
-  and convertParams seen = function
+let rec convertTyp env t =
+  match t with
+  | C.TVoid a -> Tvoid
+  | C.TInt(C.ILongLong, a) ->
+      Tlong(Signed, convertAttr a)
+  | C.TInt(C.IULongLong, a) ->
+      Tlong(Unsigned, convertAttr a)
+  | C.TInt(ik, a) ->
+      let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a)
+  | C.TFloat(fk, a) ->
+      Tfloat(convertFkind fk, convertAttr a)
+  | C.TPtr(ty, a) ->
+      Tpointer(convertTyp env ty, convertAttr a)
+  | C.TArray(ty, None, a) ->
+      (* Cparser verified that the type ty[] occurs only in
+         contexts that are safe for Clight, so just treat as ty[0]. *)
+      (* warning "array type of unspecified size"; *)
+      Tarray(convertTyp env ty, coqint_of_camlint 0l, convertAttr a)
+  | C.TArray(ty, Some sz, a) ->
+      Tarray(convertTyp env ty, convertInt sz, convertAttr a)
+  | C.TFun(tres, targs, va, a) ->
+      if Cutil.is_composite_type env tres then
+        unsupported "return type is a struct or union (consider adding option -fstruct-return)";
+      Tfunction(begin match targs with
+                | None -> Tnil
+                | Some tl -> convertParams env tl
+                end,
+                convertTyp env tres,
+                convertCallconv va a)
+  | C.TNamed _ ->
+      convertTyp env (Cutil.unroll env t)
+  | C.TStruct(id, a) ->
+      Tstruct(intern_string id.name, convertAttr a)
+  | C.TUnion(id, a) ->
+      Tunion(intern_string id.name, convertAttr a)
+  | C.TEnum(id, a) ->
+      let (sg, sz) = convertIkind Cutil.enum_ikind in
+      Tint(sz, sg, convertAttr a)
+
+and convertParams env = function
     | [] -> Tnil
-    | (id, ty) :: rem ->
-        Tcons(convertTyp seen ty, convertParams seen rem)
-
-  and convertFields seen ci =
-    convertFieldList seen ci.Env.ci_members
-
-  and convertFieldList seen = function
-    | [] -> Fnil
-    | f :: fl ->
-        Fcons(intern_string f.fld_name, convertTyp seen f.fld_typ,
-              convertFieldList seen fl)
-
-  in convertTyp [] t
+    | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem)
 
 let rec convertTypArgs env tl el =
   match tl, el with
@@ -450,12 +388,16 @@ let rec convertTypArgs env tl el =
   | (id, t1) :: tl, e1 :: el ->
       Tcons(convertTyp env t1, convertTypArgs env tl el)
 
-let cacheCompositeDef env su id attr flds =
-  let ty =
-    match su with
-    | C.Struct -> C.TStruct(id, attr)
-    | C.Union  -> C.TUnion(id, attr) in
-  Hashtbl.add compositeCache id (convertTyp env ty)
+let convertField env f =
+  if f.fld_bitfield <> None then
+    unsupported "bit field in struct or union (consider adding option -fbitfields)";
+  (intern_string f.fld_name, convertTyp env f.fld_typ)
+
+let convertCompositedef env su id attr members =
+  Composite(intern_string id.name,
+            begin match su with C.Struct -> Struct | C.Union -> Union end,
+            List.map (convertField env) members,
+            convertAttr attr)
 
 let rec projFunType env ty =
   match Cutil.unroll env ty with
@@ -958,7 +900,8 @@ and convertInitList env il =
   | i :: il' -> Init_cons(convertInit env i, convertInitList env il')
 
 let convertInitializer env ty i =
-  match Initializers.transl_init (convertTyp env ty) (convertInit env i)
+  match Initializers.transl_init
+               !comp_env (convertTyp env ty) (convertInit env i)
   with
   | Errors.OK init -> init
   | Errors.Error msg ->
@@ -970,8 +913,8 @@ let convertInitializer env ty i =
 let convertGlobvar loc env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   let ty' = convertTyp env ty in 
-  let sz = Ctypes.sizeof ty' in
-  let al = Ctypes.alignof ty' in
+  let sz = Ctypes.sizeof !comp_env ty' in
+  let al = Ctypes.alignof !comp_env ty' in
   let attr = Cutil.attributes_of_type env ty in
   let init' =
     match optinit with
@@ -998,16 +941,6 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
   (id', Gvar {gvar_info = ty'; gvar_init = init';
               gvar_readonly = readonly; gvar_volatile = volatile})
 
-(** Sanity checks on composite declarations. *)
-
-let checkComposite env si id attr flds =
-  let checkField f =
-    if f.fld_bitfield <> None then
-      unsupported "bit field in struct or union (consider adding option -fbitfields)" in
-  List.iter checkField flds;
-  if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then
-    unsupported "packed struct (consider adding option -fpacked-struct)"
-
 (** Convert a list of global declarations.
   Result is a list of CompCert C global declarations (functions +
   variables). *)
@@ -1031,21 +964,31 @@ let rec convertGlobdecls env res gl =
           end
       | C.Gfundef fd ->
           convertGlobdecls env (convertFundef g.gloc env fd :: res) gl'
-      | C.Gcompositedecl _ | C.Gtypedef _ | C.Genumdef _ ->
-          (* typedefs are unrolled, structs are expanded inline, and
-             enum tags are folded.  So we just skip their declarations. *)
-          convertGlobdecls env res gl'
-      | C.Gcompositedef(su, id, attr, flds) ->
-          (* sanity checks on fields *)
-          checkComposite env su id attr flds;
-          (* convert it to a CompCert C type and cache this type *)
-          cacheCompositeDef env su id attr flds;
+      | C.Gcompositedecl _ | C.Gcompositedef _ | C.Gtypedef _ | C.Genumdef _ ->
+          (* Composites are treated in a separate pass,
+             typedefs are unrolled, and enum tags are folded.
+             So we just skip their declarations. *)
           convertGlobdecls env res gl'
       | C.Gpragma s ->
           if not (!process_pragma_hook s) then
             warning ("'#pragma " ^ s ^ "' directive ignored");
           convertGlobdecls env res gl'
 
+(** Convert struct and union declarations.  
+    Result is a list of CompCert C composite declarations. *)
+
+let rec convertCompositedefs env res gl =
+  match gl with
+  | [] -> List.rev res
+  | g :: gl' ->
+      updateLoc g.gloc;
+      match g.gdesc with
+      | C.Gcompositedef(su, id, a, m) ->
+          convertCompositedefs env
+             (convertCompositedef env su id a m :: res) gl'
+      | _ ->
+          convertCompositedefs env res gl'
+
 (** Build environment of typedefs, structs, unions and enums *)
 
 let rec translEnv env = function
@@ -1130,17 +1073,29 @@ let convertProgram p =
   stringNum := 0;
   Hashtbl.clear decl_atom;
   Hashtbl.clear stringTable;
-  Hashtbl.clear compositeCache;
-  let p = Builtins.declarations() @ p in
+  let p = cleanupGlobals (Builtins.declarations() @ p) in
   try
-    let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in
-    let gl2 = globals_for_strings gl1 in
-    let p' = { AST.prog_defs = gl2;
-               AST.prog_public = public_globals gl2;
-               AST.prog_main = intern_string "main" } in
-    if !numErrors > 0
-    then None
-    else Some p'
+    let env = translEnv Env.empty p in
+    let typs = convertCompositedefs env [] p in
+    match build_composite_env typs with
+    | Errors.Error msg ->
+        error (sprintf "Incorrect struct or union definition: %s"
+                       (string_of_errmsg msg));
+        None
+    | Errors.OK ce ->
+        comp_env := ce;
+        let gl1 = convertGlobdecls env [] p in
+        let gl2 = globals_for_strings gl1 in
+        comp_env := Maps.PTree.empty;
+        let p' =
+          { prog_defs = gl2;
+            prog_public = public_globals gl2;
+            prog_main = intern_string "main";
+            prog_types = typs;
+            prog_comp_env = ce } in
+        if !numErrors > 0
+        then None
+        else Some p'
   with Env.Error msg ->
     error (Env.error_message msg); None
 
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 5c062158..952d148d 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -284,31 +284,31 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o
   end.
 
 Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop :=
-  (alignof_blockcopy ty | Int.unsigned ofs') /\ (alignof_blockcopy ty | Int.unsigned ofs) /\
+  (alignof_blockcopy ge ty | Int.unsigned ofs') /\ (alignof_blockcopy ge ty | Int.unsigned ofs) /\
   (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
-           \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
-           \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs').
+           \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs
+           \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs').
 
 Remark check_assign_copy:
   forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int),
   { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
 Proof with try (right; intuition omega).
   intros. unfold assign_copy_ok. 
-  assert (alignof_blockcopy ty > 0) by apply alignof_blockcopy_pos.
-  destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs')); auto...
-  destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs)); auto...
+  assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos.
+  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs')); auto...
+  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs)); auto...
   assert (Y: {b' <> b \/
               Int.unsigned ofs' = Int.unsigned ofs \/
-              Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/
-              Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'} +
+              Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/
+              Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'} +
            {~(b' <> b \/
               Int.unsigned ofs' = Int.unsigned ofs \/
-              Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/
-              Int.unsigned ofs + sizeof ty <= Int.unsigned ofs')}).
+              Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/
+              Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs')}).
   destruct (eq_block b' b); auto.
   destruct (zeq (Int.unsigned ofs') (Int.unsigned ofs)); auto.
-  destruct (zle (Int.unsigned ofs' + sizeof ty) (Int.unsigned ofs)); auto.
-  destruct (zle (Int.unsigned ofs + sizeof ty) (Int.unsigned ofs')); auto.
+  destruct (zle (Int.unsigned ofs' + sizeof ge ty) (Int.unsigned ofs)); auto.
+  destruct (zle (Int.unsigned ofs + sizeof ge ty) (Int.unsigned ofs')); auto.
   right; intuition omega.
   destruct Y... left; intuition omega. 
 Defined.
@@ -324,7 +324,7 @@ Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v
       match v with
       | Vptr b' ofs' =>
           if check_assign_copy ty b ofs b' ofs' then
-            do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty);
+            do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty);
             do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes;
             Some(w, E0, m')
           else None
@@ -746,12 +746,14 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r with
       | Some(Vptr b ofs, ty') =>
           match ty' with
-          | Tstruct id fList _ =>
-              match field_offset f fList with
+          | Tstruct id _ =>
+              do co <- ge.(genv_cenv)!id;
+              match field_offset ge f (co_members co) with
               | Error _ => stuck
               | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m)
               end
-          | Tunion id fList _ =>
+          | Tunion id _ =>
+              do co <- ge.(genv_cenv)!id;
               topred (Lred (Eloc b ofs ty) m)
           | _ => stuck
           end
@@ -787,7 +789,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   | RV, Ebinop op r1 r2 ty =>
       match is_val r1, is_val r2 with
       | Some(v1, ty1), Some(v2, ty2) =>
-          do v <- sem_binary_operation op v1 ty1 v2 ty2 m;
+          do v <- sem_binary_operation ge op v1 ty1 v2 ty2 m;
           topred (Rred (Eval v ty) m E0)
       | _, _ =>
          incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m)
@@ -828,9 +830,9 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
       end
   | RV, Esizeof ty' ty =>
-      topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m E0)
+      topred (Rred (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0)
   | RV, Ealignof ty' ty =>
-      topred (Rred (Eval (Vint (Int.repr (alignof ty'))) ty) m E0)
+      topred (Rred (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0)
   | RV, Eassign l1 r2 ty =>
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
@@ -988,8 +990,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Efield (Eval v ty1) f ty =>
       exists b, exists ofs, v = Vptr b ofs /\
       match ty1 with
-      | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta
-      | Tunion _ _ _ => True
+      | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = OK delta
+      | Tunion  id _ => exists co, ge.(genv_cenv)!id = Some co
       | _ => False
       end
   | Eval v ty => False
@@ -998,7 +1000,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Eunop op (Eval v1 ty1) ty =>
       exists v, sem_unary_operation op v1 ty1 = Some v
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
-      exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v
+      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
   | Eseqand (Eval v1 ty1) r2 ty =>
@@ -1043,8 +1045,8 @@ Proof.
   exists b; auto.
   exists b; auto.
   exists b; exists ofs; auto.
-  exists b; exists ofs; split; auto. exists delta; auto.
-  exists b; exists ofs; auto.
+  exists b; exists ofs; split; auto. exists co, delta; auto. 
+  exists b; exists ofs; split; auto. exists co; auto.
 Qed.
 
 Lemma rred_invert:
@@ -1385,10 +1387,12 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct v...
   destruct ty'... 
   (* top struct *)
-  destruct (field_offset f f0) as [delta|] eqn:?...
-  apply topred_ok; auto. apply red_field_struct; auto.
+  destruct (ge.(genv_cenv)!i0) as [co|] eqn:?...
+  destruct (field_offset ge f (co_members co)) as [delta|] eqn:?...
+  apply topred_ok; auto. eapply red_field_struct; eauto.
   (* top union *)
-  apply topred_ok; auto. apply red_field_union; auto.
+  destruct (ge.(genv_cenv)!i0) as [co|] eqn:?...
+  apply topred_ok; auto. eapply red_field_union; eauto.
   (* in depth *)
   eapply incontext_ok; eauto. 
 (* Evalof *)
@@ -1425,7 +1429,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
   rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). 
   (* top *)
-  destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|] eqn:?...
+  destruct (sem_binary_operation ge op v1 ty1 v2 ty2 m) as [v|] eqn:?...
   apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor.
   (* depth *)
   eapply incontext2_ok; eauto. 
@@ -1589,9 +1593,9 @@ Proof.
 (* deref *) 
   auto.
 (* field struct *)
-  rewrite H; auto.
+  rewrite H, H0; auto.
 (* field union *)
-  auto.
+  rewrite H; auto.
 Qed.
 
 Lemma rred_topred:
@@ -1895,21 +1899,21 @@ Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l
   match l with
   | nil => (e,m)
   | (id, ty) :: l' =>
-      let (m1,b1) := Mem.alloc m 0 (sizeof ty) in 
+      let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in 
       do_alloc_variables (PTree.set id (b1, ty) e) m1 l'
 end.
 
 Lemma do_alloc_variables_sound:
-  forall l e m, alloc_variables e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)).
+  forall l e m, alloc_variables ge e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)).
 Proof.
   induction l; intros; simpl. 
   constructor.
-  destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1] eqn:?; simpl.
+  destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ge ty)) as [m1 b1] eqn:?; simpl.
   econstructor; eauto.
 Qed.
 
 Lemma do_alloc_variables_complete:
-  forall e1 m1 l e2 m2, alloc_variables e1 m1 l e2 m2 ->
+  forall e1 m1 l e2 m2, alloc_variables ge e1 m1 l e2 m2 ->
   do_alloc_variables e1 m1 l = (e2, m2).
 Proof.
   induction 1; simpl. 
@@ -1985,7 +1989,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
             if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m)
         | Kreturn k =>
             do v' <- sem_cast v ty f.(fn_return);
-            do m' <- Mem.free_list m (blocks_of_env e);
+            do m' <- Mem.free_list m (blocks_of_env ge e);
             ret (Returnstate v' (call_cont k) m')
         | Kswitch1 sl k =>
             do n <- sem_switch_arg v ty;
@@ -2024,11 +2028,11 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
   | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m)
 
   | State f (Sreturn None) k e m =>
-      do m' <- Mem.free_list m (blocks_of_env e);
+      do m' <- Mem.free_list m (blocks_of_env ge e);
       ret (Returnstate Vundef (call_cont k) m')
   | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m)
   | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => 
-      do m' <- Mem.free_list m (blocks_of_env e);
+      do m' <- Mem.free_list m (blocks_of_env ge e);
       ret (Returnstate Vundef k m')
 
   | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m)
@@ -2209,7 +2213,7 @@ End EXEC.
 Local Open Scope option_monad_scope.
 
 Definition do_initial_state (p: program): option (genv * state) :=
-  let ge := Genv.globalenv p in
+  let ge := globalenv p in
   do m0 <- Genv.init_mem p;
   do b <- Genv.find_symbol ge p.(prog_main);
   do f <- Genv.find_funct_ptr ge b;
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 40206d38..7a45b453 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -57,12 +57,9 @@ Inductive expr : Type :=
   | Eunop: unary_operation -> expr -> type -> expr  (**r unary operation *)
   | Ebinop: binary_operation -> expr -> expr -> type -> expr (**r binary operation *)
   | Ecast: expr -> type -> expr   (**r type cast ([(ty) e]) *)
-  | Efield: expr -> ident -> type -> expr. (**r access to a member of a struct or union *)
-
-(** [sizeof] and [alignof] are derived forms. *)
-
-Definition Esizeof (ty' ty: type) : expr := Econst_int (Int.repr(sizeof ty')) ty.
-Definition Ealignof (ty' ty: type) : expr := Econst_int (Int.repr(alignof ty')) ty.
+  | Efield: expr -> ident -> type -> expr (**r access to a member of a struct or union *)
+  | Esizeof: type -> type -> expr         (**r size of a type *)
+  | Ealignof: type -> type -> expr.       (**r alignment of a type *)
 
 (** Extract the type part of a type-annotated Clight expression. *)
 
@@ -80,6 +77,8 @@ Definition typeof (e: expr) : type :=
   | Ebinop _ _ _ ty => ty
   | Ecast _ ty => ty
   | Efield _ _ ty => ty
+  | Esizeof _ ty => ty
+  | Ealignof _ ty => ty
   end.
 
 (** ** Statements *)
@@ -164,19 +163,57 @@ Definition type_of_fundef (f: fundef) : type :=
 
 (** ** Programs *)
 
-(** A program is a collection of named functions, plus a collection
-  of named global variables, carrying their types and optional initialization 
-  data.  See module [AST] for more details. *)
+(** A program 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
+}.
 
-Definition program : Type := AST.program fundef type.
+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.
 
 (** * Operational semantics *)
 
 (** The semantics uses two environments.  The global environment
   maps names of functions and global variables to memory block references,
-  and function pointers to their definitions.  (See module [Globalenvs].) *)
+  and function pointers to their definitions.  (See module [Globalenvs].)
+  It also contains a composite environment, used by type-dependent operations. *)
 
-Definition genv := Genv.t fundef type.
+Record genv := { genv_genv :> Genv.t fundef type; genv_cenv :> composite_env }.
+
+Definition globalenv (p: program) :=
+  {| genv_genv := Genv.globalenv p; genv_cenv := p.(prog_comp_env) |}.
 
 (** The local environment maps local variables to block references and
   types.  The current value of the variable is stored in the
@@ -214,22 +251,26 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop :=
   This is allowed only if [ty] indicates an access by value or by copy.
   [m'] is the updated memory state. *)
 
-Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
+Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: int):
                                             val -> mem -> Prop :=
   | assign_loc_value: forall v chunk m',
       access_mode ty = By_value chunk ->
       Mem.storev chunk m (Vptr b ofs) v = Some m' ->
-      assign_loc ty m b ofs v m'
+      assign_loc ce ty m b ofs v m'
   | assign_loc_copy: forall b' ofs' bytes m',
       access_mode ty = By_copy ->
-      (sizeof ty > 0 -> (alignof_blockcopy ty | Int.unsigned ofs')) ->
-      (sizeof ty > 0 -> (alignof_blockcopy ty | Int.unsigned ofs)) ->
+      (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs')) ->
+      (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs)) ->
       b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
-              \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
-              \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' ->
-      Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty) = Some bytes ->
+              \/ Int.unsigned ofs' + sizeof ce ty <= Int.unsigned ofs
+              \/ Int.unsigned ofs + sizeof ce ty <= Int.unsigned ofs' ->
+      Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ce ty) = Some bytes ->
       Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' ->
-      assign_loc ty m b ofs (Vptr b' ofs') m'.
+      assign_loc ce ty m b ofs (Vptr b' ofs') m'.
+
+Section SEMANTICS.
+
+Variable ge: genv.
 
 (** Allocation of function-local variables.
   [alloc_variables e1 m1 vars e2 m2] allocates one memory block
@@ -246,7 +287,7 @@ Inductive alloc_variables: env -> mem ->
       alloc_variables e m nil e m
   | alloc_variables_cons:
       forall e m id ty vars m1 b1 m2 e2,
-      Mem.alloc m 0 (sizeof ty) = (m1, b1) ->
+      Mem.alloc m 0 (sizeof ge ty) = (m1, b1) ->
       alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 ->
       alloc_variables e m ((id, ty) :: vars) e2 m2.
 
@@ -264,7 +305,7 @@ Inductive bind_parameters (e: env):
   | bind_parameters_cons:
       forall m id ty params v1 vl b m1 m2,
       PTree.get id e = Some(b, ty) ->
-      assign_loc ty m b Int.zero v1 m1 ->
+      assign_loc ge ty m b Int.zero v1 m1 ->
       bind_parameters e m1 params vl m2 ->
       bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
 
@@ -289,7 +330,7 @@ Fixpoint bind_parameter_temps (formals: list (ident * type)) (args: list val)
 (** Return the list of blocks in the codomain of [e], with low and high bounds. *)
 
 Definition block_of_binding (id_b_ty: ident * (block * type)) :=
-  match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end.
+  match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ge ty) end.
 
 Definition blocks_of_env (e: env) : list (block * Z * Z) :=
   List.map block_of_binding (PTree.elements e).
@@ -333,10 +374,6 @@ Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement :=
   | LScons _ s sl' => Ssequence s (seq_of_labeled_statement sl')
   end.
 
-Section SEMANTICS.
-
-Variable ge: genv.
-
 (** ** Evaluation of expressions *)
 
 Section EXPR.
@@ -371,12 +408,16 @@ Inductive eval_expr: expr -> val -> Prop :=
   | eval_Ebinop: forall op a1 a2 ty v1 v2 v,
       eval_expr a1 v1 ->
       eval_expr a2 v2 ->
-      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
+      sem_binary_operation ge op v1 (typeof a1) v2 (typeof a2) m = Some v ->
       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 ->
       eval_expr (Ecast a ty) v
+  | eval_Esizeof: forall ty1 ty,
+      eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
+  | eval_Ealignof: forall ty1 ty,
+      eval_expr (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1)))
   | eval_Elvalue: forall a loc ofs v,
       eval_lvalue a loc ofs -> 
       deref_loc (typeof a) m loc ofs v ->
@@ -397,14 +438,16 @@ with eval_lvalue: expr -> block -> int -> Prop :=
   | eval_Ederef: forall a ty l ofs,
       eval_expr a (Vptr l ofs) ->
       eval_lvalue (Ederef a ty) l ofs
- | eval_Efield_struct:   forall a i ty l ofs id fList att delta,
+ | eval_Efield_struct:   forall a i ty l ofs id co att delta,
       eval_expr a (Vptr l ofs) ->
-      typeof a = Tstruct id fList att ->
-      field_offset i fList = OK delta ->
+      typeof a = Tstruct id att ->
+      ge.(genv_cenv)!id = Some co ->
+      field_offset ge i (co_members co) = OK delta ->
       eval_lvalue (Efield a i ty) l (Int.add ofs (Int.repr delta))
- | eval_Efield_union:   forall a i ty l ofs id fList att,
+ | eval_Efield_union:   forall a i ty l ofs id co att,
       eval_expr a (Vptr l ofs) ->
-      typeof a = Tunion id fList att ->
+      typeof a = Tunion id att ->
+      ge.(genv_cenv)!id = Some co ->
       eval_lvalue (Efield a i ty) l ofs.
 
 Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
@@ -538,7 +581,7 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_lvalue e le m a1 loc ofs ->
       eval_expr e le m a2 v2 ->
       sem_cast v2 (typeof a2) (typeof a1) = Some v ->
-      assign_loc (typeof a1) m loc ofs v m' ->
+      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')
 
@@ -676,45 +719,48 @@ End SEMANTICS.
 
 (** The two semantics for function parameters.  First, parameters as local variables. *)
 
-Inductive function_entry1 (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop :=
+Inductive function_entry1 (ge: genv) (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop :=
   | function_entry1_intro: forall m1,
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      bind_parameters e m1 f.(fn_params) vargs m' ->
+      alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
+      bind_parameters ge e m1 f.(fn_params) vargs m' ->
       le = create_undef_temps f.(fn_temps) ->
-      function_entry1 f vargs m e le m'.
+      function_entry1 ge f vargs m e le m'.
 
-Definition step1 (ge: genv) := step ge function_entry1.
+Definition step1 (ge: genv) := step ge (function_entry1 ge).
 
 (** Second, parameters as temporaries. *)
 
-Inductive function_entry2 (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop :=
+Inductive function_entry2 (ge: genv)  (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop :=
   | function_entry2_intro:
       list_norepet (var_names f.(fn_vars)) ->
       list_norepet (var_names f.(fn_params)) ->
       list_disjoint (var_names f.(fn_params)) (var_names f.(fn_temps)) ->
-      alloc_variables empty_env m f.(fn_vars) e m' ->
+      alloc_variables ge empty_env m f.(fn_vars) e m' ->
       bind_parameter_temps f.(fn_params) vargs (create_undef_temps f.(fn_temps)) = Some le ->
-      function_entry2 f vargs m e le m'.
+      function_entry2 ge f vargs m e le m'.
 
-Definition step2 (ge: genv) := step ge function_entry2.
+Definition step2 (ge: genv) := step ge (function_entry2 ge).
 
 (** Wrapping up these definitions in two small-step semantics. *)
 
 Definition semantics1 (p: program) :=
-  Semantics step1 (initial_state p) final_state (Genv.globalenv p).
+  let ge := globalenv p in
+  Semantics_gen step1 (initial_state p) final_state ge ge.
 
 Definition semantics2 (p: program) :=
-  Semantics step2 (initial_state p) final_state (Genv.globalenv p).
+  let ge := globalenv p in
+  Semantics_gen step2 (initial_state p) final_state ge ge.
 
 (** This semantics is receptive to changes in events. *)
 
 Lemma semantics_receptive:
   forall (p: program), receptive (semantics1 p).
 Proof.
-  intros. constructor; simpl; intros.
+  intros. unfold semantics1.
+  set (ge := globalenv p). constructor; simpl; intros.
 (* receptiveness *)
-  assert (t1 = E0 -> exists s2, step1 (Genv.globalenv p) s t2 s2).
+  assert (t1 = E0 -> exists s2, step1 ge s t2 s2).
     intros. subst. inv H0. exists s1; auto.
   inversion H; subst; auto.
   (* builtin *)
@@ -724,7 +770,7 @@ Proof.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
   exists (Returnstate vres2 k m2). econstructor; eauto.
 (* trace length *)
-  red; intros. inv H; simpl; try omega.
+  red; simpl; intros. inv H; simpl; try omega.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index d61e4eef..5b092db7 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -82,7 +82,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
       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 ->
-      assign_loc (typeof a1) m loc ofs v m' ->
+      assign_loc ge (typeof a1) m loc ofs v m' ->
       exec_stmt e le m (Sassign a1 a2)
                E0 le m' Out_normal
   | exec_Sset:     forall e le m id a v,
@@ -164,12 +164,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
 
 with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
   | eval_funcall_internal: forall le m f vargs t e m1 m2 m3 out vres m4,
-      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
+      alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      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 ->
-      Mem.free_list m3 (blocks_of_env e) = Some m4 ->
+      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',
       external_call ef ge vargs m t vres m' ->
@@ -232,9 +232,9 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro
 
 with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
   | evalinf_funcall_internal: forall m f vargs t e m1 m2,
-      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
+      alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       execinf_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t ->
       evalinf_funcall m (Internal f) vargs t.
 
@@ -244,7 +244,7 @@ End BIGSTEP.
 
 Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
   | bigstep_program_terminates_intro: forall b f m0 m1 t r,
-      let ge := Genv.globalenv p in 
+      let ge := globalenv p in 
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
@@ -254,7 +254,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
 
 Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
   | bigstep_program_diverges_intro: forall b f m0 t,
-      let ge := Genv.globalenv p in 
+      let ge := globalenv p in 
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
@@ -270,7 +270,7 @@ Definition bigstep_semantics (p: program) :=
 Section BIGSTEP_TO_TRANSITIONS.
 
 Variable prog: program.
-Let ge : genv := Genv.globalenv prog.
+Let ge : genv := globalenv prog.
 
 Inductive outcome_state_match
        (e: env) (le: temp_env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index a5d4c662..4e572277 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -93,17 +93,17 @@ Inductive classify_cast_cases : Type :=
   | cast_case_s2bool                               (**r single -> bool *)
   | cast_case_l2bool                               (**r long -> bool *)
   | cast_case_p2bool                               (**r pointer -> bool *)
-  | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *)
-  | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *)
+  | cast_case_struct (id1 id2: ident)              (**r struct -> struct *)
+  | cast_case_union  (id1 id2: ident)              (**r union -> union *)
   | cast_case_void                                 (**r any -> void *)
   | cast_case_default.
 
 Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   match tto, tfrom with
-  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
+  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
   | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool
   | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool
-  | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
+  | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
   | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
   | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2
   | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2
@@ -113,7 +113,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
   | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1
   | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1
-  | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
+  | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
   | Tlong _ _, Tlong _ _ => cast_case_l2l
   | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
   | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
@@ -122,10 +122,10 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2
   | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1
   | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1
-  | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned
-  | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
-  | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
-  | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2
+  | Tpointer _ _, Tlong _ _ => cast_case_l2i I32 Unsigned
+  | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
+  | Tstruct id2 _, Tstruct id1 _ => cast_case_struct id1 id2
+  | Tunion id2 _, Tunion id1 _ => cast_case_union id1 id2
   | Tvoid, _ => cast_case_void
   | _, _ => cast_case_default
   end.
@@ -325,16 +325,16 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
           end
       | _ => None
       end
-  | cast_case_struct id1 fld1 id2 fld2 =>
+  | cast_case_struct id1 id2 =>
       match v with
       | Vptr b ofs =>
-          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
+          if ident_eq id1 id2 then Some v else None
       | _ => None
       end
-  | cast_case_union id1 fld1 id2 fld2 =>
+  | cast_case_union id1 id2 =>
       match v with
       | Vptr b ofs =>
-          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
+          if ident_eq id1 id2 then Some v else None
       | _ => None
       end
   | cast_case_void =>
@@ -359,7 +359,7 @@ Inductive classify_bool_cases : Type :=
 Definition classify_bool (ty: type) : classify_bool_cases :=
   match typeconv ty with
   | Tint _ _ _ => bool_case_i
-  | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p
+  | Tpointer _ _ => bool_case_p
   | Tfloat F64 _ => bool_case_f
   | Tfloat F32 _ => bool_case_s
   | Tlong _ _ => bool_case_l
@@ -402,7 +402,6 @@ Definition bool_val (v: val) (t: type) : option bool :=
   | bool_default => None
   end.
 
-
 (** ** Unary operators *)
 
 (** *** Boolean negation *)
@@ -639,32 +638,32 @@ Definition classify_add (ty1: type) (ty2: type) :=
   | _, _ => add_default
   end.
 
-Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : 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 ty)) n2)))
+        Some (Vptr b1 (Int.add ofs1 (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 ty)) n1)))
+        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
       | _,  _ => None
       end   
   | add_case_pl ty =>                 (**r pointer plus long *)
       match v1,v2 with
       | Vptr b1 ofs1, Vlong n2 => 
         let n2 := Int.repr (Int64.unsigned n2) in
-        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
+        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
       | _,  _ => None
       end   
   | add_case_lp ty =>                 (**r long plus pointer *)
       match v1,v2 with
       | Vlong n1, Vptr b2 ofs2 => 
         let n1 := Int.repr (Int64.unsigned n1) in
-        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
+        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
       | _,  _ => None
       end   
   | add_default =>
@@ -692,27 +691,27 @@ Definition classify_sub (ty1: type) (ty2: type) :=
   | _, _ => sub_default
   end.
 
-Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : 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 ty)) n2)))
+          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
       | _,  _ => None
       end
   | sub_case_pl ty =>            (**r pointer minus long *)
       match v1,v2 with
       | Vptr b1 ofs1, Vlong n2 => 
           let n2 := Int.repr (Int64.unsigned n2) in
-          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
+          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
       | _,  _ => None
       end
   | sub_case_pp ty =>          (**r pointer minus pointer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vptr b2 ofs2 =>
           if eq_block b1 b2 then
-            if Int.eq (Int.repr (sizeof ty)) Int.zero then None
-            else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty))))
+            if Int.eq (Int.repr (sizeof cenv ty)) Int.zero then None
+            else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof cenv ty))))
           else None
       | _, _ => None
       end
@@ -983,12 +982,13 @@ Definition sem_unary_operation
   end.
 
 Definition sem_binary_operation
+    (cenv: composite_env)
     (op: binary_operation)
     (v1: val) (t1: type) (v2: val) (t2:type)
     (m: mem): option val :=
   match op with
-  | Oadd => sem_add v1 t1 v2 t2
-  | Osub => sem_sub v1 t1 v2 t2 
+  | 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 
@@ -1005,10 +1005,10 @@ Definition sem_binary_operation
   | Oge => sem_cmp Cge v1 t1 v2 t2 m
   end.
 
-Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) :=
+Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) :=
   match id with
-  | Incr => sem_add v ty (Vint Int.one) type_int32s
-  | Decr => sem_sub v ty (Vint Int.one) type_int32s
+  | Incr => sem_add cenv v ty (Vint Int.one) type_int32s
+  | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s
   end.
 
 Definition incrdecr_type (ty: type) :=
@@ -1086,8 +1086,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 (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto.
-- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto.
+- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto.
+- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto.
 - econstructor; eauto.
 Qed.
 
@@ -1191,10 +1191,10 @@ Proof.
 Qed.
 
 Lemma sem_binary_operation_inj:
-  forall op v1 ty1 v2 ty2 v tv1 tv2,
-  sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
+  forall cenv op v1 ty1 v2 ty2 v tv1 tv2,
+  sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v ->
   val_inject f v1 tv1 -> val_inject f v2 tv2 ->
-  exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
 Proof.
   unfold sem_binary_operation; intros; destruct op.
 - (* add *)
@@ -1215,7 +1215,7 @@ Proof.
   + 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 (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3.
+    destruct (Int.eq (Int.repr (sizeof cenv ty)) Int.zero); inv H3.
     rewrite Int.sub_shifted. TrivialInject.
   + inv H0; inv H1; inv H. TrivialInject.
     econstructor. eauto. rewrite Int.sub_add_l. auto.
@@ -1278,11 +1278,11 @@ Qed.
 End GENERIC_INJECTION.
 
 Lemma sem_binary_operation_inject:
-  forall f m m' op v1 ty1 v2 ty2 v tv1 tv2,
-  sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
+  forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2,
+  sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v ->
   val_inject f v1 tv1 -> val_inject f v2 tv2 ->
   Mem.inject f m m' ->
-  exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
 Proof.
   intros. eapply sem_binary_operation_inj; eauto. 
   intros; eapply Mem.valid_pointer_inject_val; eauto.
@@ -1309,7 +1309,7 @@ Proof.
   assert (A: classify_bool t =
     match t with
     | Tint _ _ _ => bool_case_i
-    | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
+    | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
     | Tfloat F64 _ => bool_case_f
     | Tfloat F32 _ => bool_case_s
     | Tlong _ _ => bool_case_l
@@ -1332,7 +1332,6 @@ Proof.
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i Int.zero); auto. 
-  destruct (Int.eq i0 Int.zero); auto. 
 Qed.
 
 (** Relation between Boolean value and Boolean negation. *)
@@ -1528,5 +1527,4 @@ End ArithConv.
 
 
 
-
  
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 06cea006..e6e3a321 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -34,9 +34,13 @@ Require Import Smallstep.
 
 (** The semantics uses two environments.  The global environment
   maps names of functions and global variables to memory block references,
-  and function pointers to their definitions.  (See module [Globalenvs].) *)
+  and function pointers to their definitions.  (See module [Globalenvs].)
+  It also contains a composite environment, used by type-dependent operations. *)
 
-Definition genv := Genv.t fundef type.
+Record genv := { genv_genv :> Genv.t fundef type; genv_cenv :> composite_env }.
+
+Definition globalenv (p: program) :=
+  {| genv_genv := Genv.globalenv p; genv_cenv := p.(prog_comp_env) |}.
 
 (** The local environment maps local variables to block references and types.
   The current value of the variable is stored in the associated memory
@@ -46,6 +50,11 @@ Definition env := PTree.t (block * type). (* map variable -> location & type *)
 
 Definition empty_env: env := (PTree.empty (block * type)).
 
+
+Section SEMANTICS.
+
+Variable ge: genv.
+
 (** [deref_loc ty m b ofs t v] computes the value of a datum
   of type [ty] residing in memory [m] at block [b], offset [ofs].
   If the type [ty] indicates an access by value, the corresponding
@@ -54,22 +63,22 @@ Definition empty_env: env := (PTree.empty (block * type)).
   returned, and [t] the trace of observables (nonempty if this is
   a volatile access). *)
 
-Inductive deref_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> Prop :=
+Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> Prop :=
   | deref_loc_value: forall chunk v,
       access_mode ty = By_value chunk ->
       type_is_volatile ty = false ->
       Mem.loadv chunk m (Vptr b ofs) = Some v ->
-      deref_loc ge ty m b ofs E0 v
+      deref_loc ty m b ofs E0 v
   | deref_loc_volatile: forall chunk t v,
       access_mode ty = By_value chunk -> type_is_volatile ty = true ->
       volatile_load ge chunk m b ofs t v ->
-      deref_loc ge ty m b ofs t v
+      deref_loc ty m b ofs t v
   | deref_loc_reference:
       access_mode ty = By_reference ->
-      deref_loc ge ty m b ofs E0 (Vptr b ofs)
+      deref_loc ty m b ofs E0 (Vptr b ofs)
   | deref_loc_copy:
       access_mode ty = By_copy ->
-      deref_loc ge ty m b ofs E0 (Vptr b ofs).
+      deref_loc ty m b ofs E0 (Vptr b ofs).
 
 (** Symmetrically, [assign_loc ty m b ofs v t m'] returns the
   memory state after storing the value [v] in the datum
@@ -78,27 +87,27 @@ Inductive deref_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block)
   [m'] is the updated memory state and [t] the trace of observables
   (nonempty if this is a volatile store). *)
 
-Inductive assign_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block) (ofs: int):
+Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
                                             val -> trace -> mem -> Prop :=
   | assign_loc_value: forall v chunk m',
       access_mode ty = By_value chunk ->
       type_is_volatile ty = false ->
       Mem.storev chunk m (Vptr b ofs) v = Some m' ->
-      assign_loc ge ty m b ofs v E0 m'
+      assign_loc ty m b ofs v E0 m'
   | assign_loc_volatile: forall v chunk t m',
       access_mode ty = By_value chunk -> type_is_volatile ty = true ->
       volatile_store ge chunk m b ofs v t m' ->
-      assign_loc ge ty m b ofs v t m'
+      assign_loc ty m b ofs v t m'
   | assign_loc_copy: forall b' ofs' bytes m',
       access_mode ty = By_copy ->
-      (alignof_blockcopy ty | Int.unsigned ofs') ->
-      (alignof_blockcopy ty | Int.unsigned ofs) ->
+      (alignof_blockcopy ge ty | Int.unsigned ofs') ->
+      (alignof_blockcopy ge ty | Int.unsigned ofs) ->
       b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
-              \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
-              \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' ->
-      Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty) = Some bytes ->
+              \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs
+              \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs' ->
+      Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty) = Some bytes ->
       Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' ->
-      assign_loc ge ty m b ofs (Vptr b' ofs') E0 m'.
+      assign_loc ty m b ofs (Vptr b' ofs') E0 m'.
 
 (** Allocation of function-local variables.
   [alloc_variables e1 m1 vars e2 m2] allocates one memory block
@@ -115,7 +124,7 @@ Inductive alloc_variables: env -> mem ->
       alloc_variables e m nil e m
   | alloc_variables_cons:
       forall e m id ty vars m1 b1 m2 e2,
-      Mem.alloc m 0 (sizeof ty) = (m1, b1) ->
+      Mem.alloc m 0 (sizeof ge ty) = (m1, b1) ->
       alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 ->
       alloc_variables e m ((id, ty) :: vars) e2 m2.
 
@@ -124,23 +133,23 @@ Inductive alloc_variables: env -> mem ->
   in the memory blocks corresponding to the variables [params].
   [m1] is the initial memory state and [m2] the final memory state. *)
 
-Inductive bind_parameters {F V: Type} (ge: Genv.t F V) (e: env):
+Inductive bind_parameters (e: env):
                            mem -> list (ident * type) -> list val ->
                            mem -> Prop :=
   | bind_parameters_nil:
       forall m,
-      bind_parameters ge e m nil nil m
+      bind_parameters e m nil nil m
   | bind_parameters_cons:
       forall m id ty params v1 vl b m1 m2,
       PTree.get id e = Some(b, ty) ->
-      assign_loc ge ty m b Int.zero v1 E0 m1 ->
-      bind_parameters ge e m1 params vl m2 ->
-      bind_parameters ge e m ((id, ty) :: params) (v1 :: vl) m2.
+      assign_loc ty m b Int.zero v1 E0 m1 ->
+      bind_parameters e m1 params vl m2 ->
+      bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
 
 (** Return the list of blocks in the codomain of [e], with low and high bounds. *)
 
 Definition block_of_binding (id_b_ty: ident * (block * type)) :=
-  match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end.
+  match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ge ty) end.
 
 Definition blocks_of_env (e: env) : list (block * Z * Z) :=
   List.map block_of_binding (PTree.elements e).
@@ -185,10 +194,6 @@ Inductive cast_arguments: exprlist -> typelist -> list val -> Prop :=
       sem_cast v ty targ1 = Some v1 -> cast_arguments el targs vl ->
       cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
 
-Section SEMANTICS.
-
-Variable ge: genv.
-
 (** ** Reduction semantics for expressions *)
 
 Section EXPR.
@@ -215,19 +220,21 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop :=
   | red_deref: forall b ofs ty1 ty m,
       lred (Ederef (Eval (Vptr b ofs) ty1) ty) m
            (Eloc b ofs ty) m
-  | red_field_struct: forall b ofs id fList a f ty m delta,
-      field_offset f fList = OK delta ->
-      lred (Efield (Eval (Vptr b ofs) (Tstruct id fList a)) f ty) m
+  | red_field_struct: forall b ofs id co a f ty m delta,
+      ge.(genv_cenv)!id = Some co ->
+      field_offset ge f (co_members co) = OK delta ->
+      lred (Efield (Eval (Vptr b ofs) (Tstruct id a)) f ty) m
            (Eloc b (Int.add ofs (Int.repr delta)) ty) m
-  | red_field_union: forall b ofs id fList a f ty m,
-      lred (Efield (Eval (Vptr b ofs) (Tunion id fList a)) f ty) m
+  | red_field_union: forall b ofs id co a f ty m,
+      ge.(genv_cenv)!id = Some co ->
+      lred (Efield (Eval (Vptr b ofs) (Tunion id a)) f ty) m
            (Eloc b ofs ty) m.
 
 (** Head reductions for r-values *)
 
 Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
   | red_rvalof: forall b ofs ty m t v,
-      deref_loc ge ty m b ofs t v ->
+      deref_loc ty m b ofs t v ->
       rred (Evalof (Eloc b ofs ty) ty) m
          t (Eval v ty) m
   | red_addrof: forall b ofs ty1 ty m,
@@ -238,7 +245,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       rred (Eunop op (Eval v1 ty1) ty) m
         E0 (Eval v ty) m
   | red_binop: forall op v1 ty1 v2 ty2 ty m v,
-      sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
+      sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v ->
       rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m
         E0 (Eval v ty) m
   | red_cast: forall ty v1 ty1 m v,
@@ -267,22 +274,22 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
         E0 (Eparen (if b then r1 else r2) ty ty) m
   | red_sizeof: forall ty1 ty m,
       rred (Esizeof ty1 ty) m
-        E0 (Eval (Vint (Int.repr (sizeof ty1))) ty) m
+        E0 (Eval (Vint (Int.repr (sizeof ge ty1))) ty) m
   | red_alignof: forall ty1 ty m,
       rred (Ealignof ty1 ty) m
-        E0 (Eval (Vint (Int.repr (alignof 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 ->
-      assign_loc ge ty1 m b ofs v t m' ->
+      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'
   | red_assignop: forall op b ofs ty1 v2 ty2 tyres m t v1,
-      deref_loc ge ty1 m b ofs t v1 ->
+      deref_loc ty1 m b ofs t v1 ->
       rred (Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty1) m
          t (Eassign (Eloc b ofs ty1)
                     (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1) m
   | red_postincr: forall id b ofs ty m t v1 op,
-      deref_loc ge ty m b ofs t v1 ->
+      deref_loc ty m b ofs t v1 ->
       op = match id with Incr => Oadd | Decr => Osub end ->
       rred (Epostincr id (Eloc b ofs ty) ty) m
          t (Ecomma (Eassign (Eloc b ofs ty) 
@@ -739,7 +746,7 @@ Inductive sstep: state -> trace -> state -> Prop :=
   | step_internal_function: forall f vargs k m e m1 m2,
       list_norepet (var_names (fn_params f) ++ var_names (fn_vars f)) ->
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
+      bind_parameters e m1 f.(fn_params) vargs m2 ->
       sstep (Callstate (Internal f) vargs k m)
          E0 (State f f.(fn_body) k e m2)
 
@@ -766,7 +773,7 @@ End SEMANTICS.
 
 Inductive initial_state (p: program): state -> Prop :=
   | initial_state_intro: forall b f m0,
-      let ge := Genv.globalenv p in
+      let ge := globalenv p in
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
@@ -782,19 +789,20 @@ Inductive final_state: state -> int -> Prop :=
 (** Wrapping up these definitions in a small-step semantics. *)
 
 Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+  Semantics_gen step (initial_state p) final_state (globalenv p) (globalenv p).
 
 (** This semantics has the single-event property. *)
 
 Lemma semantics_single_events: 
   forall p, single_events (semantics p).
 Proof.
-  intros; red; intros. destruct H. 
-  set (ge := globalenv (semantics p)) in *.
+  unfold semantics; intros; red; simpl; intros.
+  set (ge := globalenv p) in *.
   assert (DEREF: forall chunk m b ofs t v, deref_loc ge chunk m b ofs t v -> (length t <= 1)%nat).
     intros. inv H0; simpl; try omega. inv H3; simpl; try omega.
   assert (ASSIGN: forall chunk m b ofs t v m', assign_loc ge chunk m b ofs v t m' -> (length t <= 1)%nat).
     intros. inv H0; simpl; try omega. inv H3; simpl; try omega.
+  destruct H.
   inv H; simpl; try omega. inv H0; eauto; simpl; try omega.
   eapply external_call_trace_length; eauto.
   inv H; simpl; try omega. eapply external_call_trace_length; eauto.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 3b23a547..cb83731a 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -21,6 +21,7 @@
 *)
 
 Require Import Coqlib.
+Require Import Maps.
 Require Import Errors.
 Require Import Integers.
 Require Import Floats.
@@ -160,8 +161,8 @@ Definition make_cast (from to: type) (e: expr) :=
   | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero))
   | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
   | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero))
-  | cast_case_struct id1 fld1 id2 fld2 => OK e
-  | cast_case_union id1 fld1 id2 fld2 => OK e
+  | cast_case_struct id1 id2 => OK e
+  | cast_case_union id1 id2 => OK e
   | cast_case_void => OK e
   | cast_case_default => Error (msg "Cshmgen.make_cast")
   end.
@@ -234,34 +235,34 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation)
   | bin_default => Error (msg "Cshmgen.make_binarith")
   end.
 
-Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+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 ty)) in
+      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
       OK (Ebinop Oadd e1 (Ebinop Omul n e2))
   | add_case_ip ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
       OK (Ebinop Oadd e2 (Ebinop Omul n e1))
   | add_case_pl ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
       OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | add_case_lp ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) 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
   end.
 
-Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+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 ty)) in
+      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
       OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
       OK (Ebinop Odivu (Ebinop Osub e1 e2) n)
   | sub_case_pl ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) 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
@@ -349,8 +350,8 @@ Definition make_load (addr: expr) (ty_res: type) :=
 (** [make_memcpy dst src ty] returns a [memcpy] builtin appropriate for
   by-copy assignment of a value of Clight type [ty]. *)
 
-Definition make_memcpy (dst src: expr) (ty: type) :=
-  Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof_blockcopy 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).
 
 (** [make_store addr ty rhs] stores the value of the
@@ -358,10 +359,10 @@ Definition make_memcpy (dst src: expr) (ty: type) :=
    Csharpminor expression [addr].  
    [ty] is the type of the memory location. *)
 
-Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
+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 addr rhs ty)
+  | By_copy => OK (make_memcpy ce addr rhs ty)
   | _ => Error (msg "Cshmgen.make_store")
   end.
 
@@ -375,12 +376,13 @@ Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr
   | Cop.Oabsfloat => make_absfloat a ta
   end.
 
-Definition transl_binop (op: Cop.binary_operation)
+Definition transl_binop (ce: composite_env) 
+                        (op: Cop.binary_operation)
                         (a: expr) (ta: type)
                         (b: expr) (tb: type) : res expr :=
   match op with
-  | Cop.Oadd => make_add a ta b tb
-  | Cop.Osub => make_sub a ta b tb
+  | Cop.Oadd => make_add ce a ta b tb
+  | Cop.Osub => make_sub ce a ta b tb
   | Cop.Omul => make_mul a ta b tb
   | Cop.Odiv => make_div a ta b tb
   | Cop.Omod => make_mod a ta b tb
@@ -397,13 +399,31 @@ Definition transl_binop (op: Cop.binary_operation)
   | Cop.Oge => make_cmp Cge a ta b tb
   end.
 
+(** ** Translation of field accesses *)
+
+Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr) : res expr :=
+  match ty with
+  | Tstruct id _ =>
+      match ce!id with
+      | None =>
+          Error (MSG "Undefined struct " :: CTX id :: nil)
+      | Some co =>
+          do ofs <- field_offset ce f (co_members co);
+          OK (Ebinop Oadd a (make_intconst (Int.repr ofs)))
+      end
+  | Tunion id _ =>
+      OK a
+  | _ =>
+      Error(msg "Cshmgen.make_field_access")
+  end.
+
 (** * Translation of expressions *)
 
 (** [transl_expr a] returns the Csharpminor code that computes the value
    of expression [a]. The computation is performed in the error monad
    (see module [Errors]) to enable error reporting. *)
 
-Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr :=
+Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr :=
   match a with
   | Clight.Econst_int n _ =>
       OK(make_intconst n)
@@ -418,34 +438,28 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr :=
   | Clight.Etempvar id ty =>
       OK(Evar id)
   | Clight.Ederef b ty =>
-      do tb <- transl_expr b;
+      do tb <- transl_expr ce b;
       make_load tb ty
   | Clight.Eaddrof b _ =>
-      transl_lvalue b
+      transl_lvalue ce b
   | Clight.Eunop op b _ =>
-      do tb <- transl_expr b;
+      do tb <- transl_expr ce b;
       transl_unop op tb (typeof b)
   | Clight.Ebinop op b c _ =>
-      do tb <- transl_expr b;
-      do tc <- transl_expr c;
-      transl_binop op tb (typeof b) tc (typeof c)
+      do tb <- transl_expr ce b;
+      do tc <- transl_expr ce c;
+      transl_binop ce op tb (typeof b) tc (typeof c)
   | Clight.Ecast b ty =>
-      do tb <- transl_expr b;
+      do tb <- transl_expr ce b;
       make_cast (typeof b) ty tb
-  | Clight.Efield b i ty => 
-      match typeof b with
-      | Tstruct _ fld _ =>
-          do tb <- transl_expr b;
-          do ofs <- field_offset i fld;
-          make_load
-            (Ebinop Oadd tb (make_intconst (Int.repr ofs)))
-            ty
-      | Tunion _ fld _ =>
-          do tb <- transl_expr b;
-          make_load tb ty
-      | _ =>
-          Error(msg "Cshmgen.transl_expr(field)")
-      end
+  | Clight.Efield b i ty =>
+      do tb <- transl_expr ce b;
+      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')))
+  | Clight.Ealignof ty' ty =>
+      OK(make_intconst (Int.repr (alignof ce ty')))
   end
 
 (** [transl_lvalue a] returns the Csharpminor code that evaluates
@@ -453,23 +467,15 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr :=
    where the value of [a] is stored.
 *)
 
-with transl_lvalue (a: Clight.expr) {struct a} : res expr :=
+with transl_lvalue (ce: composite_env) (a: Clight.expr) {struct a} : res expr :=
   match a with
   | Clight.Evar id _ =>
       OK (Eaddrof id)
   | Clight.Ederef b _ =>
-      transl_expr b
+      transl_expr ce b
   | Clight.Efield b i ty => 
-      match typeof b with
-      | Tstruct _ fld _ =>
-          do tb <- transl_expr b;
-          do ofs <- field_offset i fld;
-          OK (Ebinop Oadd tb (make_intconst (Int.repr ofs)))
-      | Tunion _ fld _ =>
-          transl_expr b
-      | _ =>
-          Error(msg "Cshmgen.transl_lvalue(field)")
-      end
+      do tb <- transl_expr ce b;
+      make_field_access ce (typeof b) i tb
   | _ => 
       Error(msg "Cshmgen.transl_lvalue")
   end.
@@ -479,20 +485,20 @@ with transl_lvalue (a: Clight.expr) {struct a} : res expr :=
    casted to the corresponding types in [tyl].
    Used for function applications. *)
 
-Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist)
+Fixpoint transl_arglist (ce: composite_env) (al: list Clight.expr) (tyl: typelist)
                          {struct al}: res (list expr) :=
   match al, tyl with
   | nil, Tnil => OK nil
   | a1 :: a2, Tcons ty1 ty2 =>
-      do ta1 <- transl_expr a1;
+      do ta1 <- transl_expr ce a1;
       do ta1' <- make_cast (typeof a1) ty1 ta1;
-      do ta2 <- transl_arglist a2 ty2;      
+      do ta2 <- transl_arglist ce a2 ty2;      
       OK (ta1' :: ta2)
   | a1 :: a2, Tnil =>
       (* Tolerance for calls to K&R or variadic functions *)
-      do ta1 <- transl_expr a1;
+      do ta1 <- transl_expr ce a1;
       do ta1' <- make_cast (typeof a1) (default_argument_conversion (typeof a1)) ta1;
-      do ta2 <- transl_arglist a2 Tnil;
+      do ta2 <- transl_arglist ce a2 Tnil;
       OK (ta1' :: ta2)
   | _, _ =>
       Error(msg "Cshmgen.transl_arglist: arity mismatch")
@@ -536,24 +542,24 @@ loop s1 s2          --->     block {
                              // break in s1 and s2 branches here
 *)
 
-Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
+Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
                           (s: Clight.statement) {struct s} : res stmt :=
   match s with
   | Clight.Sskip =>
       OK Sskip
   | Clight.Sassign b c =>
-      do tb <- transl_lvalue b;
-      do tc <- transl_expr c;
+      do tb <- transl_lvalue ce b;
+      do tc <- transl_expr ce c;
       do tc' <- make_cast (typeof c) (typeof b) tc;
-      make_store tb (typeof b) tc'
+      make_store ce tb (typeof b) tc'
   | Clight.Sset x b =>
-      do tb <- transl_expr b;
+      do tb <- transl_expr ce b;
       OK(Sset x tb)
   | Clight.Scall x b cl =>
       match classify_fun (typeof b) with
       | fun_case_f args res cconv =>
-          do tb <- transl_expr b;
-          do tcl <- transl_arglist cl args;
+          do tb <- transl_expr ce b;
+          do tcl <- transl_arglist ce cl args;
           OK(Scall x {| sig_args := typlist_of_arglist cl args;
                         sig_res  := opttyp_of_type res;
                         sig_cc   := cconv |}
@@ -561,80 +567,80 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
       | _ => Error(msg "Cshmgen.transl_stmt(call)")
       end
   | Clight.Sbuiltin x ef tyargs bl =>
-      do tbl <- transl_arglist bl tyargs;
+      do tbl <- transl_arglist ce bl tyargs;
       OK(Sbuiltin x ef tbl)
   | Clight.Ssequence s1 s2 =>
-      do ts1 <- transl_statement tyret nbrk ncnt s1;
-      do ts2 <- transl_statement tyret nbrk ncnt s2;
+      do ts1 <- transl_statement ce tyret nbrk ncnt s1;
+      do ts2 <- transl_statement ce tyret nbrk ncnt s2;
       OK (Sseq ts1 ts2)
   | Clight.Sifthenelse e s1 s2 =>
-      do te <- transl_expr e;
-      do ts1 <- transl_statement tyret nbrk ncnt s1;
-      do ts2 <- transl_statement tyret nbrk ncnt s2;
+      do te <- transl_expr ce e;
+      do ts1 <- transl_statement ce tyret nbrk ncnt s1;
+      do ts2 <- transl_statement ce tyret nbrk ncnt s2;
       OK (Sifthenelse (make_boolean te (typeof e)) ts1 ts2)
   | Clight.Sloop s1 s2 =>
-      do ts1 <- transl_statement tyret 1%nat 0%nat s1;
-      do ts2 <- transl_statement tyret 0%nat (S ncnt) s2;
+      do ts1 <- transl_statement ce tyret 1%nat 0%nat s1;
+      do ts2 <- transl_statement ce tyret 0%nat (S ncnt) s2;
       OK (Sblock (Sloop (Sseq (Sblock ts1) ts2)))
   | Clight.Sbreak =>
       OK (Sexit nbrk)
   | Clight.Scontinue =>
       OK (Sexit ncnt)
   | Clight.Sreturn (Some e) =>
-      do te <- transl_expr e;
+      do te <- transl_expr ce e;
       do te' <- make_cast (typeof e) tyret te;
       OK (Sreturn (Some te'))
   | Clight.Sreturn None =>
       OK (Sreturn None)
   | Clight.Sswitch a sl =>
-      do ta <- transl_expr a;
-      do tsl <- transl_lbl_stmt tyret 0%nat (S ncnt) sl;
+      do ta <- transl_expr ce a;
+      do tsl <- transl_lbl_stmt ce tyret 0%nat (S ncnt) sl;
       match classify_switch (typeof a) with
       | switch_case_i => OK (Sblock (Sswitch false ta tsl))
       | switch_case_l => OK (Sblock (Sswitch true ta tsl))
       | switch_default => Error(msg "Cshmgen.transl_stmt(switch)")
       end
   | Clight.Slabel lbl s =>
-      do ts <- transl_statement tyret nbrk ncnt s;
+      do ts <- transl_statement ce tyret nbrk ncnt s;
       OK (Slabel lbl ts)
   | Clight.Sgoto lbl =>
       OK (Sgoto lbl)
   end
 
-with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat)
+with transl_lbl_stmt (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
                      (sl: Clight.labeled_statements)
                      {struct sl}: res lbl_stmt :=
   match sl with
   | Clight.LSnil =>
       OK LSnil
   | Clight.LScons n s sl' =>
-      do ts <- transl_statement tyret nbrk ncnt s;
-      do tsl' <- transl_lbl_stmt tyret nbrk ncnt sl';
+      do ts <- transl_statement ce tyret nbrk ncnt s;
+      do tsl' <- transl_lbl_stmt ce tyret nbrk ncnt sl';
       OK (LScons n ts tsl')
   end.
 
 (*** Translation of functions *)
 
-Definition transl_var (v: ident * type) := (fst v, sizeof (snd v)).
+Definition transl_var (ce: composite_env) (v: ident * type) := (fst v, sizeof ce (snd v)).
 
 Definition signature_of_function (f: Clight.function) :=
   {| sig_args := map typ_of_type (map snd (Clight.fn_params f));
      sig_res  := opttyp_of_type (Clight.fn_return f);
      sig_cc   := Clight.fn_callconv f |}.
 
-Definition transl_function (f: Clight.function) : res function :=
-  do tbody <- transl_statement f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f);
+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);
   OK (mkfunction 
        (signature_of_function f)
        (map fst (Clight.fn_params f))
-       (map transl_var (Clight.fn_vars f))
+       (map (transl_var ce) (Clight.fn_vars f))
        (map fst (Clight.fn_temps f))
        tbody).
 
-Definition transl_fundef (f: Clight.fundef) : res fundef :=
+Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef :=
   match f with
   | Clight.Internal g => 
-      do tg <- transl_function g; OK(AST.Internal tg)
+      do tg <- transl_function ce g; OK(AST.Internal tg)
   | Clight.External ef args res cconv =>
       if signature_eq (ef_sig ef) (signature_of_type args res cconv)
       then OK(AST.External ef)
@@ -646,4 +652,5 @@ Definition transl_fundef (f: Clight.fundef) : res fundef :=
 Definition transl_globvar (ty: type) := OK tt.
 
 Definition transl_program (p: Clight.program) : res program :=
-  transform_partial_program2 transl_fundef transl_globvar p.
+  transform_partial_program2 (transl_fundef p.(prog_comp_env)) transl_globvar p.
+
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index dc47df04..7f61c657 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -40,8 +40,8 @@ Proof.
 Qed.
 
 Lemma transl_fundef_sig1:
-  forall f tf args res cc,
-  transl_fundef f = OK tf ->
+  forall ce f tf args res cc,
+  transl_fundef ce f = OK tf ->
   classify_fun (type_of_fundef f) = fun_case_f args res cc ->
   funsig tf = signature_of_type args res cc.
 Proof.
@@ -54,8 +54,8 @@ Proof.
 Qed.
 
 Lemma transl_fundef_sig2:
-  forall f tf args res cc,
-  transl_fundef f = OK tf ->
+  forall ce f tf args res cc,
+  transl_fundef ce f = OK tf ->
   type_of_fundef f = Tfunction args res cc ->
   funsig tf = signature_of_type args res cc.
 Proof.
@@ -70,8 +70,8 @@ Qed.
 Lemma transl_expr_lvalue:
   forall ge e le m a loc ofs ta,
   Clight.eval_lvalue ge e le m a loc ofs ->
-  transl_expr a = OK ta ->
-  (exists tb, transl_lvalue a = OK tb /\ make_load tb (typeof a) = OK ta).
+  transl_expr ge a = OK ta ->
+  (exists tb, transl_lvalue ge a = OK tb /\ make_load tb (typeof a) = OK ta).
 Proof.
   intros until ta; intros EVAL TR. inv EVAL; simpl in TR.
   (* var local *)
@@ -81,39 +81,36 @@ Proof.
   (* deref *)
   monadInv TR. exists x; auto.
   (* field struct *)
-  rewrite H0 in TR. monadInv TR.
-  econstructor; split. simpl. rewrite H0.
-  rewrite EQ; rewrite EQ1; simpl; eauto. auto.
+  monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. 
   (* field union *)
-  rewrite H0 in TR. monadInv TR.
-  econstructor; split. simpl. rewrite H0. rewrite EQ; simpl; eauto. auto.
+  monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. 
 Qed.
 
 (** Properties of labeled statements *)
 
 Lemma transl_lbl_stmt_1:
-  forall tyret nbrk ncnt n sl tsl,
-  transl_lbl_stmt tyret nbrk ncnt sl = OK tsl ->
-  transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl).
+  forall ce tyret nbrk ncnt n sl tsl,
+  transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
+  transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl).
 Proof.
   intros until n.
   assert (DFL: forall sl tsl,
-    transl_lbl_stmt tyret nbrk ncnt sl = OK tsl ->
-    transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)).
+    transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
+    transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)).
   {
     induction sl; simpl; intros. 
     inv H; auto.
     monadInv H. simpl. destruct o; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto.
   }
   assert (CASE: forall sl tsl,
-    transl_lbl_stmt tyret nbrk ncnt sl = OK tsl ->
+    transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
     match Clight.select_switch_case n sl with
     | None =>
         select_switch_case n tsl = None
     | Some sl' =>
         exists tsl',
            select_switch_case n tsl = Some tsl'
-        /\ transl_lbl_stmt tyret nbrk ncnt sl' = OK tsl'
+        /\ transl_lbl_stmt ce tyret nbrk ncnt sl' = OK tsl'
     end).
   {
     induction sl; simpl; intros.
@@ -130,9 +127,9 @@ Proof.
 Qed.
 
 Lemma transl_lbl_stmt_2:
-  forall tyret nbrk ncnt sl tsl,
-  transl_lbl_stmt tyret nbrk ncnt sl = OK tsl ->
-  transl_statement tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl).
+  forall ce tyret nbrk ncnt sl tsl,
+  transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
+  transl_statement ce tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl).
 Proof.
   induction sl; intros.
   monadInv H. auto. 
@@ -143,6 +140,7 @@ Qed.
 
 Section CONSTRUCTORS.
 
+Variable ce: composite_env.
 Variable ge: genv.
 
 Lemma make_intconst_correct:
@@ -305,9 +303,9 @@ Proof.
   simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
   destruct (Int.eq i Int.zero); auto.
   (* struct *)
-  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto.
+  destruct (ident_eq id1 id2); inv H2; auto.
   (* union *)
-  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto.
+  destruct (ident_eq id1 id2); inv H2; auto.
 Qed.
 
 Lemma make_boolean_correct:
@@ -467,7 +465,7 @@ End MAKE_BIN.
 
 Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
 
-Lemma make_add_correct: binary_constructor_correct make_add sem_add.
+Lemma make_add_correct: binary_constructor_correct (make_add ce) (sem_add ce).
 Proof.
   red; unfold make_add, sem_add;
   intros until m; intros SEM MAKE EV1 EV2;
@@ -479,14 +477,14 @@ Proof.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
-Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub.
+Lemma make_sub_correct: binary_constructor_correct (make_sub ce) (sem_sub ce).
 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 (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0.
+  destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ce ty)) Int.zero) eqn:E; inv H0.
   econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. 
 - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - eapply make_binarith_correct; eauto; intros; auto.
@@ -648,8 +646,8 @@ Qed.
 
 Lemma transl_binop_correct:
   forall op a tya b tyb c va vb v e le m,
-  transl_binop op a tya b tyb = OK c ->  
-  sem_binary_operation op va tya vb tyb m = Some v ->
+  transl_binop ce op a tya b tyb = OK c ->  
+  sem_binary_operation ce 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.
@@ -691,12 +689,12 @@ Proof.
 Qed.
 
 Lemma make_memcpy_correct:
-  forall f dst src ty k e le m b ofs v m',
+  forall ce f dst src ty k e le m b ofs v m',
   eval_expr ge e le m dst (Vptr b ofs) ->
   eval_expr ge e le m src v ->
-  assign_loc ty m b ofs v m' ->
+  assign_loc ce ty m b ofs v m' ->
   access_mode ty = By_copy ->
-  step ge (State f (make_memcpy dst src ty) k e le m) E0 (State f Sskip k e le m').
+  step ge (State f (make_memcpy ce dst src ty) 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. 
@@ -710,10 +708,10 @@ Qed.
  
 Lemma make_store_correct:
   forall addr ty rhs code e le m b ofs v m' f k,
-  make_store addr ty rhs = OK code ->
+  make_store ce 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 ty m b ofs v m' ->
+  assign_loc ce 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.
@@ -736,32 +734,32 @@ Variable prog: Clight.program.
 Variable tprog: Csharpminor.program.
 Hypothesis TRANSL: transl_program prog = OK tprog.
 
-Let ge := Genv.globalenv prog.
+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 transl_globvar _ TRANSL).
+Proof (Genv.find_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
 
 Lemma public_preserved:
   forall s, Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof (Genv.public_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL).
+Proof (Genv.public_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ 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 f = OK tf.
-Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar _ TRANSL).
+  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 f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar _ TRANSL).
+  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 transl_globvar _ TRANSL).
+Proof (Genv.block_is_volatile_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
 
 (** * Matching between environments *)
 
@@ -772,7 +770,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 ty);
+      e!id = Some (b, ty) -> te!id = Some(b, sizeof ge ty);
     me_local_inv:
       forall id b sz,
       te!id = Some (b, sz) -> exists ty, e!id = Some(b, ty)
@@ -791,18 +789,18 @@ Qed.
 Lemma match_env_same_blocks:
   forall e te,
   match_env e te ->
-  blocks_of_env te = Clight.blocks_of_env e.
+  blocks_of_env te = Clight.blocks_of_env ge e.
 Proof.
   intros.
   set (R := fun (x: (block * type)) (y: (block * Z)) =>
          match x, y with
-         | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ty
+         | (b1, ty), (b2, sz) => b2 = b1 /\ sz = 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 ty); split. eapply me_local; eauto. red; auto.
+  intros id [b ty] GET. exists (b, 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.
@@ -818,7 +816,7 @@ Qed.
 Lemma match_env_free_blocks:
   forall e te m m',
   match_env e te ->
-  Mem.free_list m (Clight.blocks_of_env e) = Some m' ->
+  Mem.free_list m (Clight.blocks_of_env ge e) = Some m' ->
   Mem.free_list m (blocks_of_env te) = Some m'.
 Proof.
   intros. rewrite (match_env_same_blocks _ _ H). auto.
@@ -839,16 +837,16 @@ Qed.
 
 Lemma match_env_alloc_variables:
   forall e1 m1 vars e2 m2,
-  Clight.alloc_variables e1 m1 vars e2 m2 ->
+  Clight.alloc_variables ge e1 m1 vars e2 m2 ->
   forall te1,
   match_env e1 te1 ->
   exists te2,
-  Csharpminor.alloc_variables te1 m1 (map transl_var vars) te2 m2
+  Csharpminor.alloc_variables te1 m1 (map (transl_var ge) vars) te2 m2
   /\ match_env e2 te2.
 Proof.
   induction 1; intros; simpl.
   exists te1; split. constructor. auto.
-  exploit (IHalloc_variables (PTree.set id (b1, sizeof ty) te1)).
+  exploit (IHalloc_variables (PTree.set id (b1, sizeof ge ty) te1)).
   constructor.
     (* me_local *)
     intros until ty0. repeat rewrite PTree.gsspec.
@@ -913,11 +911,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 a = OK ta) ,
+   forall ta (TR: transl_expr ge 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 a = OK ta),
+   forall ta (TR: transl_lvalue ge a = OK ta),
    Csharpminor.eval_expr tge te le m ta (Vptr b ofs)).
 Proof.
   apply eval_expr_lvalue_ind; intros; try (monadInv TR).
@@ -939,6 +937,10 @@ Proof.
   eapply transl_binop_correct; eauto.
 (* cast *)
   eapply make_cast_correct; eauto.
+(* sizeof *)
+  apply make_intconst_correct.
+(* alignof *)
+  apply make_intconst_correct.
 (* rvalue out of lvalue *)
   exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]].
   eapply make_load_correct; eauto.  
@@ -952,32 +954,34 @@ Proof.
 (* deref *)
   simpl in TR. eauto. 
 (* field struct *)
-  simpl in TR. rewrite H1 in TR. monadInv TR.
+  change (prog_comp_env prog) with (genv_cenv ge) in EQ0.
+  unfold make_field_access in EQ0; rewrite H1, H2 in EQ0; monadInv EQ0.
   eapply eval_Ebinop; eauto.
   apply make_intconst_correct. 
   simpl. congruence.
 (* field union *)
-  simpl in TR. rewrite H1 in TR. eauto.
+  unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0.
+  auto.
 Qed.
 
 Lemma transl_expr_correct:
    forall a v,
    Clight.eval_expr ge e le m a v ->
-   forall ta, transl_expr a = OK ta ->
+   forall ta, transl_expr ge 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 a = OK ta ->
+   forall ta, transl_lvalue ge 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 al tyl = OK tal ->
+  forall tal, transl_arglist ge al tyl = OK tal ->
   Csharpminor.eval_exprlist tge te le m tal vl.
 Proof.
   induction 1; intros.
@@ -1035,21 +1039,21 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P
   | 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 tyret nbrk ncnt s = OK ts ->
+      transl_statement ge tyret nbrk ncnt s = OK ts ->
       match_cont tyret nbrk ncnt k tk ->
       match_cont tyret nbrk ncnt
                  (Clight.Kseq s k)
                  (Kseq ts tk)
   | match_Kloop1: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
-      transl_statement tyret 1%nat 0%nat s1 = OK ts1 ->
-      transl_statement tyret 0%nat (S ncnt) s2 = OK ts2 ->
+      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
                  (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 tyret 1%nat 0%nat s1 = OK ts1 ->
-      transl_statement tyret 0%nat (S ncnt) s2 = OK ts2 ->
+      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)
                  (Clight.Kloop2 s1 s2 k)
@@ -1060,7 +1064,7 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P
                  (Clight.Kswitch k)
                  (Kblock tk)
   | match_Kcall_some: forall tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk,
-      transl_function f = OK tf ->
+      transl_function ge f = OK tf ->
       match_env e te ->
       match_cont (Clight.fn_return f) nbrk' ncnt' k tk ->
       match_cont tyret nbrk ncnt 
@@ -1070,8 +1074,8 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P
 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 f = OK tf)
-          (TR: transl_statement (Clight.fn_return f) nbrk ncnt s = OK ts)
+          (TRF: transl_function ge f = OK tf)
+          (TR: transl_statement ge (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),
@@ -1079,7 +1083,7 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
                    (State tf ts' tk' te le m)
   | match_callstate:
       forall fd args k m tfd tk targs tres cconv
-          (TR: transl_fundef fd = OK tfd)
+          (TR: transl_fundef ge fd = OK tfd)
           (MK: match_cont Tvoid 0%nat 0%nat k tk)
           (ISCC: Clight.is_call_cont k)
           (TY: type_of_fundef fd = Tfunction targs tres cconv),
@@ -1093,7 +1097,7 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
 
 Remark match_states_skip:
   forall f e le te nbrk ncnt k tf tk m,
-  transl_function f = OK tf ->
+  transl_function ge f = OK tf ->
   match_env e te ->
   match_cont (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).
@@ -1109,27 +1113,27 @@ Variable tyret: type.
 
 Lemma transl_find_label:
   forall s nbrk ncnt k ts tk
-  (TR: transl_statement tyret nbrk ncnt s = OK ts)
+  (TR: transl_statement ge tyret nbrk ncnt s = OK ts)
   (MC: match_cont 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 tyret nbrk' ncnt' s' = OK ts'
+      /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts'
       /\ match_cont tyret nbrk' ncnt' k' tk'
   end
 
 with transl_find_label_ls:
   forall ls nbrk ncnt k tls tk
-  (TR: transl_lbl_stmt tyret nbrk ncnt ls = OK tls)
+  (TR: transl_lbl_stmt ge tyret nbrk ncnt ls = OK tls)
   (MC: match_cont 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 tyret nbrk' ncnt' s' = OK ts'
+      /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts'
       /\ match_cont tyret nbrk' ncnt' k' tk'
   end.
 
@@ -1340,7 +1344,8 @@ Proof.
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
-  econstructor; eauto. 
+  econstructor; eauto.
+Local Opaque ge. 
   simpl. rewrite H5; simpl. rewrite H7; simpl. eauto. 
   constructor. 
 
@@ -1464,9 +1469,10 @@ Lemma transl_initial_states:
 Proof.
   intros. inv H.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
-  assert (C: Genv.find_symbol tge (prog_main tprog) = Some b).
-    rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog).
-    auto. symmetry. unfold transl_program in TRANSL. 
+  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. 
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index f8c3963e..3b0eb84f 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -97,13 +97,16 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
       eval_simple_lvalue (Ederef r ty) b ofs
-  | esl_field_struct: forall r f ty b ofs id fList a delta,
+  | esl_field_struct: forall r f ty b ofs id co a delta,
       eval_simple_rvalue r (Vptr b ofs) ->
-      typeof r = Tstruct id fList a -> field_offset f fList = OK delta ->
+      typeof r = Tstruct id a -> 
+      ge.(genv_cenv)!id = Some co ->
+      field_offset ge f (co_members co) = OK delta ->
       eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta))
-  | esl_field_union: forall r f ty b ofs id fList a,
+  | esl_field_union: forall r f ty b ofs id co a,
       eval_simple_rvalue r (Vptr b ofs) ->
-      typeof r = Tunion id fList a ->
+      typeof r = Tunion id a ->
+      ge.(genv_cenv)!id = Some co ->
       eval_simple_lvalue (Efield r f ty) b ofs
 
 with eval_simple_rvalue: expr -> val -> Prop :=
@@ -123,16 +126,16 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Eunop op r1 ty) v
   | esr_binop: forall op r1 r2 ty v1 v2 v,
       eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 ->
-      sem_binary_operation op v1 (typeof r1) v2 (typeof r2) m = Some v ->
+      sem_binary_operation ge op v1 (typeof r1) v2 (typeof r2) m = Some v ->
       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 ->
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
-      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1)))
+      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
   | esr_alignof: forall ty1 ty,
-      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1))).
+      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))).
 
 Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
   | esrl_nil:
@@ -291,7 +294,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge (typeof l) m b ofs t1 v1 ->
       eval_simple_rvalue e m r v2 ->
-      sem_binary_operation op v1 (typeof l) v2 (typeof r) m = Some v3 ->
+      sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 ->
       sem_cast v3 tyres (typeof l) = Some v4 ->
       assign_loc ge (typeof l) m b ofs v4 t2 m' ->
       ty = typeof l ->
@@ -304,7 +307,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       eval_simple_lvalue e m l b ofs ->
       deref_loc ge (typeof l) m b ofs t v1 ->
       eval_simple_rvalue e m r v2 ->
-      match sem_binary_operation op v1 (typeof l) v2 (typeof r) m with
+      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
@@ -320,7 +323,7 @@ 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 id v1 ty = Some v2 ->
+      sem_incrdecr ge id v1 ty = Some v2 ->
       sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
       assign_loc ge ty m b ofs v3 t2 m' ->
       ty = typeof l ->
@@ -332,7 +335,7 @@ 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 id v1 ty with
+      match sem_incrdecr ge id v1 ty with
       | None => True
       | Some v2 =>
           match sem_cast v2 (incrdecr_type ty) ty with
@@ -525,8 +528,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Efield (Eval v ty1) f ty =>
       exists b, exists ofs, v = Vptr b ofs /\
       match ty1 with
-      | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta
-      | Tunion _ _ _ => True
+      | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = Errors.OK delta
+      | Tunion id _ => exists co, ge.(genv_cenv)!id = Some co
       | _ => False
       end
   | Eval v ty => False
@@ -535,7 +538,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Eunop op (Eval v1 ty1) ty =>
       exists v, sem_unary_operation op v1 ty1 = Some v
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
-      exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v
+      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
   | Eseqand (Eval v1 ty1) r2 ty =>
@@ -581,8 +584,8 @@ Proof.
   exists b; auto.
   exists b; auto.
   exists b; exists ofs; auto.
-  exists b; exists ofs; split; auto. exists delta; auto.
-  exists b; exists ofs; auto.
+  exists b; exists ofs; split; auto. exists co, delta; auto.
+  exists b; exists ofs; split; auto. exists co; auto.
 Qed.
 
 Lemma rred_invert:
@@ -705,11 +708,11 @@ Lemma eval_simple_steps:
    (forall a v, eval_simple_rvalue e m a v ->
     forall C, context RV RV C ->
     star Csem.step ge (ExprState f (C a) k e m)
-                  E0 (ExprState f (C (Eval v (typeof a))) k e m))
+                   E0 (ExprState f (C (Eval v (typeof a))) k e m))
 /\ (forall a b ofs, eval_simple_lvalue e m a b ofs ->
     forall C, context LV RV C ->
     star Csem.step ge (ExprState f (C a) k e m)
-                  E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)).
+                   E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)).
 Proof.
 
 Ltac Steps REC C' := eapply star_trans; [apply (REC C'); eauto | idtac | simpl; reflexivity].
@@ -816,8 +819,8 @@ Ltac StepR REC C' a :=
   StepR IHa (fun x => C(Efield x f0 ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl.
   intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) eqn:?; try contradiction.
-  destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto.
-  exists b; exists ofs; econstructor; eauto.
+  destruct TY as (co & delta & CE & OFS). exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto.
+  destruct TY as (co & CE).  exists b; exists ofs; econstructor; eauto.
 (* valof *)
   destruct (andb_prop _ _ S) as [S1 S2]. clear S. rewrite negb_true_iff in S2.
   StepL IHa (fun x => C(Evalof x ty)) a.
@@ -1197,7 +1200,7 @@ Proof.
   eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto.
   eapply plus_left.
   left; apply step_rred; auto. econstructor; eauto.
-  destruct (sem_binary_operation op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?.
+  destruct (sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?.
   eapply star_left.
   left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto.  
   apply star_one. 
@@ -1230,10 +1233,10 @@ Proof.
   eapply plus_left.
   left; apply step_rred; auto. econstructor; eauto.
   set (op := match id with Incr => Oadd | Decr => Osub end).
-  assert (SEM: sem_binary_operation op v1 (typeof l) (Vint Int.one) type_int32s m =
-              sem_incrdecr id v1 (typeof l)).
+  assert (SEM: sem_binary_operation ge op v1 (typeof l) (Vint Int.one) type_int32s m =
+              sem_incrdecr ge id v1 (typeof l)).
     destruct id; auto.
-  destruct (sem_incrdecr id v1 (typeof l)) as [v2|].
+  destruct (sem_incrdecr ge id v1 (typeof l)) 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.
@@ -1325,7 +1328,7 @@ Proof.
   exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs (typeof b1)) x tyres ty))); eauto.
   intros [v [E2 S2]].
   exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]].
-  destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?.
+  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 (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')).
   destruct H2 as [t2 [m' D]].
@@ -1340,7 +1343,7 @@ 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 id v1 ty) as [v2|] eqn:?.
+  destruct (sem_incrdecr ge id v1 ty) as [v2|] eqn:?.
   destruct (sem_cast v2 (incrdecr_type ty) ty) 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]].
@@ -1431,12 +1434,13 @@ End STRATEGY.
 (** The semantics that follows the strategy. *)
 
 Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+  let ge := globalenv p in
+  Semantics_gen step (initial_state p) final_state ge ge.
 
 (** This semantics is receptive to changes in events. *)
 
 Remark deref_loc_trace:
-  forall F V (ge: Genv.t F V) ty m b ofs t v,
+  forall ge ty m b ofs t v,
   deref_loc ge ty m b ofs t v ->
   match t with nil => True | ev :: nil => True | _ => False end.
 Proof.
@@ -1444,7 +1448,7 @@ Proof.
 Qed.
 
 Remark deref_loc_receptive:
-  forall F V (ge: Genv.t F V) ty m b ofs ev1 t1 v ev2,
+  forall ge ty m b ofs ev1 t1 v ev2,
   deref_loc ge ty m b ofs (ev1 :: t1) v ->
   match_traces ge (ev1 :: nil) (ev2 :: nil) ->
   t1 = nil /\ exists v', deref_loc ge ty m b ofs (ev2 :: nil) v'.
@@ -1456,7 +1460,7 @@ Proof.
 Qed.
 
 Remark assign_loc_trace:
-  forall F V (ge: Genv.t F V) ty m b ofs t v m',
+  forall ge ty m b ofs t v m',
   assign_loc ge ty m b ofs v t m' ->
   match t with nil => True | ev :: nil => output_event ev | _ => False end.
 Proof.
@@ -1464,7 +1468,7 @@ Proof.
 Qed.
 
 Remark assign_loc_receptive:
-  forall F V (ge: Genv.t F V) ty m b ofs ev1 t1 v m' ev2,
+  forall ge ty m b ofs ev1 t1 v m' ev2,
   assign_loc ge ty m b ofs v (ev1 :: t1) m' ->
   match_traces ge (ev1 :: nil) (ev2 :: nil) ->
   ev1 :: t1 = ev2 :: nil.
@@ -1479,6 +1483,7 @@ Lemma semantics_strongly_receptive:
 Proof.
   intros. constructor; simpl; intros.
 (* receptiveness *)
+  set (ge := globalenv p) in *.
   inversion H; subst.
   inv H1.
   (* valof volatile *)
@@ -1492,9 +1497,9 @@ Proof.
   subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
   econstructor; econstructor; eauto.
   inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
-  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
+  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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')).
+  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. 
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. 
@@ -1505,9 +1510,9 @@ Proof.
   rewrite Heqo; auto.
   (* assignop stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
-  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
+  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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')).
+  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. 
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. 
@@ -1521,9 +1526,9 @@ 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 id v1' (typeof l)) as [v2'|] eqn:?.
+  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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')).
+  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. 
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. 
@@ -1534,9 +1539,9 @@ Proof.
   rewrite Heqo; auto.
   (* postincr stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
-  destruct (sem_incrdecr id v1' (typeof l)) as [v2'|] eqn:?.
+  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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')).
+  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. 
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. 
@@ -1732,7 +1737,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_simple_lvalue ge e m2 l' b ofs ->
       deref_loc ge (typeof l) m2 b ofs t3 v1 ->
       eval_simple_rvalue ge e m2 r' v2 ->
-      sem_binary_operation op v1 (typeof l) v2 (typeof r) m2 = Some v3 ->
+      sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 ->
       sem_cast v3 tyres (typeof l) = Some v4 ->
       assign_loc ge (typeof l) m2 b ofs v4 t4 m3 ->
       ty = typeof l ->
@@ -1741,7 +1746,7 @@ 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 id v1 ty = Some v2 ->
+      sem_incrdecr ge id v1 ty = Some v2 ->
       sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
       assign_loc ge ty m1 b ofs v3 t3 m2 ->
       ty = typeof l ->
@@ -1893,11 +1898,11 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
 with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
   | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4,
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
+      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 ->
-      Mem.free_list m3 (blocks_of_env e) = Some m4 ->
+      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',
       external_call ef ge vargs m t vres m' ->
@@ -2115,7 +2120,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
 with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
   | evalinf_funcall_internal: forall m f vargs t e m1 m2,
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
+      alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       execinf_stmt e m2 f.(fn_body) t ->
       evalinf_funcall m (Internal f) vargs t.
@@ -3019,7 +3024,7 @@ End BIGSTEP.
 
 Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
   | bigstep_program_terminates_intro: forall b f m0 m1 t r,
-      let ge := Genv.globalenv p in 
+      let ge := globalenv p in 
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
@@ -3029,7 +3034,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
 
 Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
   | bigstep_program_diverges_intro: forall b f m0 t,
-      let ge := Genv.globalenv p in 
+      let ge := globalenv p in 
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index fa74f11c..8ea4e077 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -20,6 +20,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 Require Import AST.
+Require Import Errors.
 Require Import Ctypes.
 Require Import Cop.
 
@@ -207,8 +208,44 @@ Definition type_of_fundef (f: fundef) : type :=
 
 (** ** Programs *)
 
-(** A program is a collection of named functions, plus a collection
-  of named global variables, carrying their types and optional initialization 
-  data.  See module [AST] for more details. *)
+(** A program 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
+}.
+
+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 : Type := AST.program fundef type.
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index c437a6bc..091c5276 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -16,6 +16,7 @@
 (** Type expressions for the Compcert C and Clight languages *)
 
 Require Import Coqlib.
+Require Import Maps.
 Require Import AST.
 Require Import Errors.
 Require Archi.
@@ -63,32 +64,6 @@ Definition noattr := {| attr_volatile := false; attr_alignas := None |}.
   of the function arguments (list [targs]), and the type of the
   function result ([tres]).  Variadic functions and old-style unprototyped
   functions are not supported.
-- In C, struct and union types are named and compared by name.
-  This enables the definition of recursive struct types such as
-<<
-  struct s1 { int n; struct * s1 next; };
->>
-  Note that recursion within types must go through a pointer type.
-  For instance, the following is not allowed in C.
-<<
-  struct s2 { int n; struct s2 next; };
->>
-  In Compcert C, struct and union types [Tstruct id fields] and
-  [Tunion id fields] are compared by structure: the [fields]
-  argument gives the names and types of the members.  The identifier
-  [id] is a local name which can be used in conjuction with the
-  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr id]
-  stands for a pointer type to the nearest enclosing [Tstruct]
-  or [Tunion] type named [id].  For instance. the structure [s1]
-  defined above in C is expressed by
-<<
-  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
-               (Fcons "next" (Tcomp_ptr "s1")
-               Fnil))
->>
-  Note that the incorrect structure [s2] above cannot be expressed at
-  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
-  structure or union, but not to the structure or union directly.
 *)
 
 Inductive type : Type :=
@@ -99,35 +74,27 @@ Inductive type : Type :=
   | Tpointer: type -> attr -> type                 (**r pointer types ([*ty]) *)
   | Tarray: type -> Z -> attr -> type              (**r array types ([ty[len]]) *)
   | Tfunction: typelist -> type -> calling_convention -> type    (**r function types *)
-  | Tstruct: ident -> fieldlist -> attr -> type    (**r struct types *)
-  | Tunion: ident -> fieldlist -> attr -> type     (**r union types *)
-  | Tcomp_ptr: ident -> attr -> type               (**r pointer to named struct or union *)
-
+  | Tstruct: ident -> attr -> type                 (**r struct types *)
+  | Tunion: ident -> attr -> type                  (**r union types *)
 with typelist : Type :=
   | Tnil: typelist
-  | Tcons: type -> typelist -> typelist
-
-with fieldlist : Type :=
-  | Fnil: fieldlist
-  | Fcons: ident -> type -> fieldlist -> fieldlist.
+  | Tcons: type -> typelist -> typelist.
 
 Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2}
-with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}
-with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}.
+with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}.
 Proof.
   assert (forall (x y: intsize), {x=y} + {x<>y}) by decide equality.
   assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality.
   assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality.
   assert (forall (x y: attr), {x=y} + {x<>y}).
   { decide equality. decide equality. apply N.eq_dec. apply bool_dec. }
-  generalize ident_eq zeq bool_dec. intros E1 E2 E3.
+  generalize ident_eq zeq bool_dec ident_eq; intros.
   decide equality.
   decide equality.
   decide equality.
-  generalize ident_eq. intros E1. decide equality.
 Defined.
 
-Opaque type_eq typelist_eq fieldlist_eq.
+Opaque type_eq typelist_eq.
 
 (** Extract the attributes of a type. *)
 
@@ -140,9 +107,8 @@ Definition attr_of_type (ty: type) :=
   | Tpointer elt a => a
   | Tarray elt sz a => a
   | Tfunction args res cc => noattr
-  | Tstruct id fld a => a
-  | Tunion id fld a => a
-  | Tcomp_ptr id a => a
+  | Tstruct id a => a
+  | Tunion id a => a
   end.
 
 (** Change the top-level attributes of a type *)
@@ -156,9 +122,8 @@ Definition change_attributes (f: attr -> attr) (ty: type) : type :=
   | Tpointer elt a => Tpointer elt (f a)
   | Tarray elt sz a => Tarray elt sz (f a)
   | Tfunction args res cc => ty
-  | Tstruct id fld a => Tstruct id fld (f a)
-  | Tunion id fld a => Tunion id fld (f a)
-  | Tcomp_ptr id a => Tcomp_ptr id (f a)
+  | Tstruct id a => Tstruct id (f a)
+  | Tunion id a => Tunion id (f a)
   end.
 
 (** Erase the top-level attributes of a type *)
@@ -181,6 +146,39 @@ Definition attr_union (a1 a2: attr) : attr :=
 Definition merge_attributes (ty: type) (a: attr) : type :=
   change_attributes (attr_union a) ty.
 
+(** Syntax for [struct] and [union] definitions.  [struct] and [union]
+  are collectively called "composites".  Each compilation unit
+  comes with a list of top-level definitions of composites. *)
+
+Inductive struct_or_union : Type := Struct | Union.
+
+Definition members : Type := list (ident * type).
+
+Inductive composite_definition : Type :=
+  Composite (id: ident) (su: struct_or_union) (m: members) (a: attr).
+
+(** 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
+  the [composite_definition], such as size and alignment information. *)
+
+Record composite : Type := {
+  co_su: struct_or_union;
+  co_members: members;
+  co_attr: attr;
+  co_sizeof: Z;
+  co_alignof: Z;
+  co_sizeof_pos: co_sizeof >= 0;
+  co_alignof_two_p: exists n, co_alignof = two_power_nat n;
+  co_sizeof_alignof: (co_alignof | co_sizeof)
+}.
+
+Definition composite_env : Type := PTree.t composite.
+
+(** * Operations over types *)
+
+(** ** Conversions *)
+
 Definition type_int32s := Tint I32 Signed noattr.
 Definition type_bool := Tint IBool Signed noattr.
 
@@ -208,15 +206,51 @@ Definition default_argument_conversion (ty: type) : type :=
   | _                   => remove_attributes ty
   end.
 
-(** * Operations over types *)
+(** ** Complete types *)
 
-(** Alignment of a type, in bytes. *)
+(** A type is complete if it fully describes an object.
+  All struct and union names appearing in the type must be defined,
+  unless they occur under a pointer or function type.  [void] and
+  function types are incomplete types. *)
 
-Fixpoint alignof (t: type) : Z :=
-  match attr_alignas (attr_of_type t) with
+Fixpoint complete_type (env: composite_env) (t: type) : bool :=
+  match t with
+  | Tvoid => false
+  | Tint _ _ _ => true
+  | Tlong _ _ => true
+  | Tfloat _ _ => true
+  | Tpointer _ _ => true
+  | Tarray t' _ _ => complete_type env t'
+  | Tfunction _ _ _ => false
+  | Tstruct id _ | Tunion id _ =>
+      match env!id with Some co => true | None => false end
+  end.
+
+Definition complete_or_function_type (env: composite_env) (t: type) : bool :=
+  match t with
+  | Tfunction _ _ _ => true
+  | _ => complete_type env t
+  end.
+
+(** ** Alignment of a type *)
+
+(** Adjust the natural alignment [al] based on the attributes [a] attached
+  to the type.  If an "alignas" attribute is given, use it as alignment
+  in preference to [al]. *)
+
+Definition align_attr (a: attr) (al: Z) : Z :=
+  match attr_alignas a with
   | Some l => two_p (Z.of_N l)
-  | None =>
-      match t with
+  | None => al
+  end.
+
+(** In the ISO C standard, alignment is defined only for complete
+  types.  However, it is convenient that [alignof] is a total
+  function.  For incomplete types, it returns 1. *)
+
+Fixpoint alignof (env: composite_env) (t: type) : Z :=
+  align_attr (attr_of_type t)
+   (match t with
       | Tvoid => 1
       | Tint I8 _ _ => 1
       | Tint I16 _ _ => 2
@@ -226,42 +260,26 @@ Fixpoint alignof (t: type) : Z :=
       | Tfloat F32 _ => 4
       | Tfloat F64 _ => Archi.align_float64
       | Tpointer _ _ => 4
-      | Tarray t' _ _ => alignof t'
+      | Tarray t' _ _ => alignof env t'
       | Tfunction _ _ _ => 1
-      | Tstruct _ fld _ => alignof_fields fld
-      | Tunion _ fld _ => alignof_fields fld
-      | Tcomp_ptr _ _ => 4
-      end
-  end
-
-with alignof_fields (f: fieldlist) : Z :=
-  match f with
-  | Fnil => 1
-  | Fcons id t f' => Zmax (alignof t) (alignof_fields f')
-  end.
-
-Scheme type_ind2 := Induction for type Sort Prop
-  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
+      | Tstruct id _ | Tunion id _ =>
+          match env!id with Some co => co_alignof co | None => 1 end
+    end).
+
+Remark align_attr_two_p:
+  forall al a,
+  (exists n, al = two_power_nat n) ->
+  (exists n, align_attr a al = two_power_nat n).
+Proof.
+  intros. unfold align_attr. destruct (attr_alignas a).   
+  exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto.
+  auto.
+Qed.
 
 Lemma alignof_two_p:
-  forall t, exists n, alignof t = two_power_nat n
-with alignof_fields_two_p:
-  forall f, exists n, alignof_fields f = two_power_nat n.
+  forall env t, exists n, alignof env t = two_power_nat n.
 Proof.
-  assert (X: forall t a,
-    (exists n, a = two_power_nat n) ->
-    exists n,
-    match attr_alignas (attr_of_type t) with
-    | Some l => two_p (Z.of_N l)
-    | None => a
-    end = two_power_nat n).
-  {
-    intros.  
-    destruct (attr_alignas (attr_of_type t)).
-    exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto.
-    auto.
-  }
-  induction t; apply X; simpl; auto.
+  induction t; apply align_attr_two_p; simpl.
   exists 0%nat; auto.
   destruct i.
     exists 0%nat; auto.
@@ -273,28 +291,28 @@ Proof.
     exists 2%nat; auto.
     (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity).
   exists 2%nat; auto.
+  apply IHt.
   exists 0%nat; auto.
-  exists 2%nat; auto.
-  induction f; simpl.
-  exists 0%nat; auto.
-  apply Z.max_case; auto.
+  destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto.
+  destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto.
 Qed.
 
 Lemma alignof_pos:
-  forall t, alignof t > 0.
+  forall env t, alignof env t > 0.
 Proof.
-  intros. destruct (alignof_two_p t) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
+  intros. destruct (alignof_two_p env t) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 Qed.
 
-Lemma alignof_fields_pos:
-  forall f, alignof_fields f > 0.
-Proof.
-  intros. destruct (alignof_fields_two_p f) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
-Qed.
+(** ** Size of a type *)
 
-(** Size of a type, in bytes. *)
+(** In the ISO C standard, size is defined only for complete
+  types.  However, it is convenient that [sizeof] is a total
+  function.  For [void] and function types, we follow GCC and define
+  their size to be 1.  For undefined structures and unions, the size is 
+  arbitrarily taken to be 0.
+*)
 
-Fixpoint sizeof (t: type) : Z :=
+Fixpoint sizeof (env: composite_env) (t: type) : Z :=
   match t with
   | Tvoid => 1
   | Tint I8 _ _ => 1
@@ -305,199 +323,217 @@ Fixpoint sizeof (t: type) : Z :=
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
-  | Tarray t' n _ => sizeof t' * Zmax 0 n
+  | Tarray t' n _ => sizeof env t' * Z.max 0 n
   | Tfunction _ _ _ => 1
-  | Tstruct _ fld _ => align (sizeof_struct fld 0) (alignof t)
-  | Tunion _ fld _ => align (sizeof_union fld) (alignof t)
-  | Tcomp_ptr _ _ => 4
-  end
-
-with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
-  match fld with
-  | Fnil => pos
-  | Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t)
-  end
-
-with sizeof_union (fld: fieldlist) : Z :=
-  match fld with
-  | Fnil => 0
-  | Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld')
+  | Tstruct id _ | Tunion id _ =>
+      match env!id with Some co => co_sizeof co | None => 0 end
   end.
 
 Lemma sizeof_pos:
-  forall t, sizeof t >= 0
-with sizeof_struct_incr:
-  forall fld pos, pos <= sizeof_struct fld pos.
+  forall env t, sizeof env t >= 0.
 Proof.
-- Local Opaque alignof.
-  assert (X: forall n t, n >= 0 -> align n (alignof t) >= 0).
-  {
-    intros. generalize (align_le n (alignof t) (alignof_pos t)). omega.
-  }
-  induction t; simpl; try xomega.
+  induction t; simpl; try omega.
   destruct i; omega.
   destruct f; omega.
-  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. 
-  apply X. apply Zle_ge. apply sizeof_struct_incr. 
-  apply X. induction f; simpl; xomega.
-- induction fld; intros; simpl.
-  omega. 
-  eapply Zle_trans. 2: apply IHfld.
-  apply Zle_trans with (align pos (alignof t)). 
-  apply align_le. apply alignof_pos.
-  generalize (sizeof_pos t); omega.
+  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega.
+  destruct (env!i). apply co_sizeof_pos. omega.
+  destruct (env!i). apply co_sizeof_pos. omega.
 Qed.
 
+(** The size of a type is an integral multiple of its alignment,
+  unless the alignment was artificially increased with the [__Alignas]
+  attribute. *)
+
 Fixpoint naturally_aligned (t: type) : Prop :=
+  attr_alignas (attr_of_type t) = None /\
   match t with
-  | Tint _ _ a | Tlong _ a | Tfloat _ a | Tpointer _ a | Tcomp_ptr _ a =>
-      attr_alignas a = None
-  | Tarray t' _ a =>
-      attr_alignas a = None /\ naturally_aligned t'
-  | Tvoid | Tfunction _ _ _ | Tstruct _ _ _ | Tunion _ _ _ =>
-      True
+  | Tarray t' _ _ => naturally_aligned t'
+  | _ => True
   end.
 
 Lemma sizeof_alignof_compat:
-  forall t, naturally_aligned t -> (alignof t | sizeof t).
+  forall env t, naturally_aligned t -> (alignof env t | sizeof env t).
 Proof.
-Local Transparent alignof.
-  induction t; simpl; intros.
+  induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. 
 - apply Zdivide_refl.
-- rewrite H. destruct i; apply Zdivide_refl.
-- rewrite H. exists (8 / Archi.align_int64); reflexivity. 
-- rewrite H. destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. 
-- rewrite H; apply Zdivide_refl.
-- destruct H. rewrite H. apply Z.divide_mul_l; auto. 
+- destruct i; apply Zdivide_refl.
+- exists (8 / Archi.align_int64); reflexivity. 
+- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. 
 - apply Zdivide_refl.
-- change (alignof (Tstruct i f a) | align (sizeof_struct f 0) (alignof (Tstruct i f a))).
-  apply align_divides. apply alignof_pos.
-- change (alignof (Tunion i f a) | align (sizeof_union f) (alignof (Tunion i f a))).
-  apply align_divides. apply alignof_pos.
-- rewrite H; apply Zdivide_refl.
+- apply Z.divide_mul_l; auto. 
+- apply Zdivide_refl.
+- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. 
+- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. 
 Qed.
 
-(** Byte offset for a field in a struct or union.
-  Field are laid out consecutively, and padding is inserted
-  to align each field to the natural alignment for its type. *)
+(** ** Size and alignment for composite definitions *)
+
+(** The alignment for a structure or union is the max of the alignment
+  of its members. *)
 
-Open Local Scope string_scope.
+Fixpoint alignof_composite (env: composite_env) (m: members) : Z :=
+  match m with
+  | nil => 1
+  | (id, t) :: m' => Z.max (alignof env t) (alignof_composite env m')
+  end.
+
+(** The size of a structure corresponds to its layout: fields are
+  laid out consecutively, and padding is inserted to align
+  each field to the alignment for its type. *)
+
+Fixpoint sizeof_struct (env: composite_env) (cur: Z) (m: members) : Z :=
+  match m with
+  | nil => cur
+  | (id, t) :: m' => sizeof_struct env (align cur (alignof env t) + sizeof env t) m'
+  end.
+
+(** The size of an union is the max of the sizes of its members. *)
 
-Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
-                              {struct fld} : res Z :=
+Fixpoint sizeof_union (env: composite_env) (m: members) : Z :=
+  match m with
+  | nil => 0
+  | (id, t) :: m' => Z.max (sizeof env t) (sizeof_union env m')
+  end.
+
+Lemma alignof_composite_two_p:
+  forall env m, exists n, alignof_composite env m = two_power_nat n.
+Proof.
+  induction m as [|[id t]]; simpl. 
+- exists 0%nat; auto.
+- apply Z.max_case; auto. apply alignof_two_p.
+Qed.
+
+Lemma alignof_composite_pos:
+  forall env m a, align_attr a (alignof_composite env m) > 0.
+Proof.
+  intros.
+  exploit align_attr_two_p. apply (alignof_composite_two_p env m). 
+  instantiate (1 := a). intros [n EQ]. 
+  rewrite EQ; apply two_power_nat_pos.
+Qed.
+
+Lemma sizeof_struct_incr:
+  forall env m cur, cur <= sizeof_struct env cur m.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+- omega.
+- apply Zle_trans with (align cur (alignof env t)). 
+  apply align_le. apply alignof_pos.
+  apply Zle_trans with (align cur (alignof env t) + sizeof env t).
+  generalize (sizeof_pos env t); omega. 
+  apply IHm.
+Qed.
+
+Lemma sizeof_union_pos:
+  forall env m, 0 <= sizeof_union env m.
+Proof.
+  induction m as [|[id t]]; simpl; xomega.
+Qed.
+
+(** ** Byte offset for a field of a structure *)
+
+(** [field_offset env id fld] returns the byte offset for field [id]
+  in a structure whose members are [fld].  Fields are laid out
+  consecutively, and padding is inserted to align each field to the
+  alignment for its type. *)
+
+Fixpoint field_offset_rec (env: composite_env) (id: ident) (fld: members) (pos: Z)
+                          {struct fld} : res Z :=
   match fld with
-  | Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
-  | Fcons id' t fld' =>
+  | nil => Error (MSG "Unknown field " :: CTX id :: nil)
+  | (id', t) :: fld' =>
       if ident_eq id id'
-      then OK (align pos (alignof t))
-      else field_offset_rec id fld' (align pos (alignof t) + sizeof t)
+      then OK (align pos (alignof env t))
+      else field_offset_rec env id fld' (align pos (alignof env t) + sizeof env t)
   end.
 
-Definition field_offset (id: ident) (fld: fieldlist) : res Z :=
-  field_offset_rec id fld 0.
+Definition field_offset (env: composite_env) (id: ident) (fld: members) : res Z :=
+  field_offset_rec env id fld 0.
 
-Fixpoint field_type (id: ident) (fld: fieldlist) {struct fld} : res type :=
+Fixpoint field_type (id: ident) (fld: members) {struct fld} : res type :=
   match fld with
-  | Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
-  | Fcons id' t fld' => if ident_eq id id' then OK t else field_type id fld'
+  | nil => Error (MSG "Unknown field " :: CTX id :: nil)
+  | (id', t) :: fld' => if ident_eq id id' then OK t else field_type id fld'
   end.
 
 (** Some sanity checks about field offsets.  First, field offsets are 
   within the range of acceptable offsets. *)
 
 Remark field_offset_rec_in_range:
-  forall id ofs ty fld pos,
-  field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty ->
-  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
+  forall env id ofs ty fld pos,
+  field_offset_rec env id fld pos = OK ofs -> field_type id fld = OK ty ->
+  pos <= ofs /\ ofs + sizeof env ty <= sizeof_struct env pos fld.
 Proof.
-  intros until ty. induction fld; simpl.
-  congruence.
-  destruct (ident_eq id i); intros.
-  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
+  intros until ty. induction fld as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id i); intros.
+  inv H. inv H0. split.
+  apply align_le. apply alignof_pos. apply sizeof_struct_incr.
   exploit IHfld; eauto. intros [A B]. split; auto. 
-  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
-  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega. 
+  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)).
+  apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. 
 Qed.
 
 Lemma field_offset_in_range:
-  forall sid fld a fid ofs ty,
-  field_offset fid fld = OK ofs -> field_type fid fld = OK ty ->
-  0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a).
+  forall env fld id ofs ty,
+  field_offset env id fld = OK ofs -> field_type id fld = OK ty ->
+  0 <= ofs /\ ofs + sizeof env ty <= sizeof_struct env 0 fld.
 Proof.
-  intros. exploit field_offset_rec_in_range; eauto. intros [A B].
-  split. auto.
-Local Opaque alignof. 
-  simpl. eapply Zle_trans; eauto. 
-  apply align_le. apply alignof_pos. 
+  intros. eapply field_offset_rec_in_range; eauto.
 Qed.
 
 (** Second, two distinct fields do not overlap *)
 
 Lemma field_offset_no_overlap:
-  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
-  field_offset id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
-  field_offset id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
+  forall env id1 ofs1 ty1 id2 ofs2 ty2 fld,
+  field_offset env id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
+  field_offset env id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
   id1 <> id2 ->
-  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
+  ofs1 + sizeof env ty1 <= ofs2 \/ ofs2 + sizeof env ty2 <= ofs1.
 Proof.
-  intros until ty2. intros fld0 A B C D NEQ.
-  assert (forall fld pos,
-  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
-  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
-  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
-  induction fld; intro pos; simpl. congruence.
-  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
-  congruence. 
-  subst i. intros. inv H; inv H0.
+  intros until fld. unfold field_offset. generalize 0 as pos.
+  induction fld as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id1 i); destruct (ident_eq id2 i).
++ congruence. 
++ subst i. inv H; inv H0.
   exploit field_offset_rec_in_range. eexact H1. eauto. tauto.  
-  subst i. intros. inv H1; inv H2.
++ subst i. inv H1; inv H2.
   exploit field_offset_rec_in_range. eexact H. eauto. tauto. 
-  intros. eapply IHfld; eauto.
-
-  apply H with fld0 0; auto.
++ eapply IHfld; eauto.
 Qed.
 
 (** Third, if a struct is a prefix of another, the offsets of common fields
     are the same. *)
 
-Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
-  match fld1 with
-  | Fnil => fld2
-  | Fcons id ty fld => Fcons id ty (fieldlist_app fld fld2)
-  end.
-
 Lemma field_offset_prefix:
-  forall id ofs fld2 fld1,
-  field_offset id fld1 = OK ofs ->
-  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
+  forall env id ofs fld2 fld1,
+  field_offset env id fld1 = OK ofs ->
+  field_offset env id (fld1 ++ fld2) = OK ofs.
 Proof.
-  intros until fld2.
-  assert (forall fld1 pos, 
-    field_offset_rec id fld1 pos = OK ofs ->
-    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
-  induction fld1; intros pos; simpl. congruence.
-  destruct (ident_eq id i); auto.
-  intros. unfold field_offset; auto. 
+  intros until fld1. unfold field_offset. generalize 0 as pos. 
+  induction fld1 as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id i); auto. 
 Qed.
 
 (** Fourth, the position of each field respects its alignment. *)
 
 Lemma field_offset_aligned:
-  forall id fld ofs ty,
-  field_offset id fld = OK ofs -> field_type id fld = OK ty ->
-  (alignof ty | ofs).
+  forall env id fld ofs ty,
+  field_offset env id fld = OK ofs -> field_type id fld = OK ty ->
+  (alignof env ty | ofs).
 Proof.
-  assert (forall id ofs ty fld pos,
-          field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty ->
-          (alignof ty | ofs)).
-  induction fld; simpl; intros.
-  discriminate.
-  destruct (ident_eq id i). inv H; inv H0. 
-  apply align_divides. apply alignof_pos. 
-  eapply IHfld; eauto.
-  intros. eapply H with (pos := 0); eauto.
+  intros until ty. unfold field_offset. generalize 0 as pos. revert fld. 
+  induction fld as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id i).
++ inv H; inv H0. apply align_divides. apply alignof_pos.
++ eauto.
 Qed.
 
+(** ** Access modes *)
+
 (** The [access_mode] function describes how a l-value of the given
 type must be accessed:
 - [By_value ch]: access by value, i.e. by loading from the address
@@ -530,9 +566,8 @@ Definition access_mode (ty: type) : mode :=
   | Tpointer _ _ => By_value Mint32
   | Tarray _ _ _ => By_reference
   | Tfunction _ _ _ => By_reference
-  | Tstruct _ _ _ => By_copy
-  | Tunion _ _ _ => By_copy
-  | Tcomp_ptr _ _ => By_nothing
+  | Tstruct _ _ => By_copy
+  | Tunion _ _ => By_copy
 end.
 
 (** For the purposes of the semantics and the compiler, a type denotes
@@ -545,87 +580,13 @@ Definition type_is_volatile (ty: type) : bool :=
   | _          => false
   end.
 
-(** Unroll the type of a structure or union field, substituting
-    [Tcomp_ptr] by a pointer to the structure. *)
-
-Section UNROLL_COMPOSITE.
-
-Variable cid: ident.
-Variable comp: type.
-
-Fixpoint unroll_composite (ty: type) : type :=
-  match ty with
-  | Tvoid => ty
-  | Tint _ _ _ => ty
-  | Tlong _ _ => ty
-  | Tfloat _ _ => ty
-  | Tpointer t1 a => Tpointer (unroll_composite t1) a
-  | Tarray t1 sz a => Tarray (unroll_composite t1) sz a
-  | Tfunction t1 t2 a => Tfunction (unroll_composite_list t1) (unroll_composite t2) a
-  | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a
-  | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a
-  | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty
-  end
-
-with unroll_composite_list (tl: typelist) : typelist :=
-  match tl with
-  | Tnil => Tnil
-  | Tcons t1 tl' => Tcons (unroll_composite t1) (unroll_composite_list tl')
-  end
-
-with unroll_composite_fields (fld: fieldlist) : fieldlist :=
-  match fld with
-  | Fnil => Fnil
-  | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld')
-  end.
-
-Lemma attr_of_type_unroll_composite:
-  forall ty, attr_of_type (unroll_composite ty) = attr_of_type ty.
-Proof.
-  intros. destruct ty; simpl; auto; destruct (ident_eq i cid); auto.
-Qed.
-
-Lemma alignof_unroll_composite:
-  forall ty, alignof (unroll_composite ty) = alignof ty.
-Proof.
-Local Transparent alignof.
-  apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty)
-                   (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld));
-  simpl; intros; auto.
-  rewrite H; auto.
-  destruct (ident_eq i cid); auto. simpl. rewrite H; auto.
-  destruct (ident_eq i cid); auto. simpl. rewrite H; auto.
-  destruct (ident_eq i cid); auto. congruence.
-Qed.
-
-Lemma sizeof_unroll_composite:
-  forall ty, sizeof (unroll_composite ty) = sizeof ty.
-Proof.
-Local Opaque alignof.
-  apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty)
-                   (fun fld => 
-                      sizeof_union (unroll_composite_fields fld) = sizeof_union fld
-                   /\ forall pos,
-                      sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos));
-  simpl; intros; auto.
-- rewrite H. auto.
-- rewrite <- (alignof_unroll_composite (Tstruct i f a)). simpl.
-  destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H0. auto.
-- rewrite <- (alignof_unroll_composite (Tunion i f a)). simpl.
-  destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H. auto.
-- destruct (ident_eq i cid); auto. 
-- destruct H0. split. 
-  + congruence.
-  + intros. rewrite H1. rewrite H. rewrite alignof_unroll_composite. auto.
-Qed.
-
-End UNROLL_COMPOSITE.
+(** ** Alignment for block copy operations *)
 
 (** A variant of [alignof] for use in block copy operations.
   Block copy operations do not support alignments greater than 8,
   and require the size to be an integral multiple of the alignment. *)
 
-Fixpoint alignof_blockcopy (t: type) : Z :=
+Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z :=
   match t with
   | Tvoid => 1
   | Tint I8 _ _ => 1
@@ -636,20 +597,22 @@ Fixpoint alignof_blockcopy (t: type) : Z :=
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
-  | Tarray t' _ _ => alignof_blockcopy t'
+  | Tarray t' _ _ => alignof_blockcopy env t'
   | Tfunction _ _ _ => 1
-  | Tstruct _ fld _ => Zmin 8 (alignof t)
-  | Tunion _ fld _ => Zmin 8 (alignof t)
-  | Tcomp_ptr _ _ => 4
+  | Tstruct id _ | Tunion id _ =>
+      match env!id with
+      | Some co => Z.min 8 (co_alignof co)
+      | None => 1
+      end
   end.
 
 Lemma alignof_blockcopy_1248:
-  forall ty, let a := alignof_blockcopy ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8.
+  forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8.
 Proof.
-  assert (X: forall ty, let a := Zmin 8 (alignof ty) in
+  assert (X: forall co, let a := Zmin 8 (co_alignof co) in
              a = 1 \/ a = 2 \/ a = 4 \/ a = 8).
   {
-    intros. destruct (alignof_two_p ty) as [n EQ]. unfold a; rewrite EQ. 
+    intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. 
     destruct n; auto.
     destruct n; auto.
     destruct n; auto.
@@ -660,45 +623,47 @@ Proof.
   induction ty; simpl; auto.
   destruct i; auto.
   destruct f; auto.
+  destruct (env!i); auto. 
+  destruct (env!i); auto.
 Qed.
 
 Lemma alignof_blockcopy_pos:
-  forall ty, alignof_blockcopy ty > 0.
+  forall env ty, alignof_blockcopy env ty > 0.
 Proof.
-  intros. generalize (alignof_blockcopy_1248 ty). simpl. intuition omega.
+  intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition omega.
 Qed.
 
 Lemma sizeof_alignof_blockcopy_compat:
-  forall ty, (alignof_blockcopy ty | sizeof ty).
+  forall env ty, (alignof_blockcopy env ty | sizeof env ty).
 Proof.
-  assert (X: forall ty sz, (alignof ty | sz) -> (Zmin 8 (alignof ty) | sz)).
+  assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)).
   {
-    intros. destruct (alignof_two_p ty) as [n EQ]. rewrite EQ in *.
-    destruct n; auto.
-    destruct n; auto.
-    destruct n; auto.
-    eapply Zdivide_trans; eauto. 
+    intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof.
+    destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ.
+    destruct n. apply Zdivide_refl.
+    destruct n. apply Zdivide_refl.
+    destruct n. apply Zdivide_refl.
     apply Z.min_case. 
-    replace (two_power_nat (S(S(S n)))) with (two_p (3 + Z.of_nat n)).
-    rewrite two_p_is_exp by omega. change (two_p 3) with 8.
-    exists (two_p (Z.of_nat n)). ring.
+    exists (two_p (Z.of_nat n)). 
+    change 8 with (two_p 3). 
+    rewrite <- two_p_is_exp by omega.
     rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega.
     apply Zdivide_refl.
   }
-  Local Opaque alignof.
   induction ty; simpl.
   apply Zdivide_refl.
-  destruct i; apply Zdivide_refl.
   apply Zdivide_refl.
-  destruct f; apply Zdivide_refl.
   apply Zdivide_refl.
-  apply Z.divide_mul_l. auto.
   apply Zdivide_refl.
-  apply X. apply align_divides. apply alignof_pos.
-  apply X. apply align_divides. apply alignof_pos.
   apply Zdivide_refl.
+  apply Z.divide_mul_l. auto.
+  apply Zdivide_refl.
+  destruct (env!i). apply X. apply Zdivide_0. 
+  destruct (env!i). apply X. apply Zdivide_0. 
 Qed.
 
+(** ** C types and back-end types *)
+
 (** Extracting a type list from a function parameter declaration. *)
 
 Fixpoint type_of_params (params: list (ident * type)) : typelist :=
@@ -735,3 +700,259 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
 Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
   mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.
 
+(** * Construction of the composite environment *)
+
+Definition sizeof_composite (env: composite_env) (su: struct_or_union) (m: members) : Z :=
+  match su with
+  | Struct => sizeof_struct env 0 m
+  | Union  => sizeof_union env m
+  end.
+
+Lemma sizeof_composite_pos:
+  forall env su m, 0 <= sizeof_composite env su m.
+Proof.
+  intros. destruct su; simpl.
+  apply sizeof_struct_incr.
+  apply sizeof_union_pos.
+Qed.
+
+Fixpoint complete_members (env: composite_env) (m: members) : bool :=
+  match m with
+  | nil => true
+  | (id, t) :: m' => complete_type env t && complete_members env m'
+  end.
+
+(** Convert a composite definition to its internal representation.
+  The size and alignment of the composite are determined at this time.
+  The alignment takes into account the [__Alignas] attributes
+  associated with the definition.  The size is rounded up to a multiple
+  of the alignment.  
+
+  The conversion fails if a type of a member is not complete.  This rules
+  out incorrect recursive definitions such as
+<<
+    struct s { int x; struct s next; }
+>>
+  Here, when we process the definition of [struct s], the identifier [s]
+  is not bound yet in the composite environment, hence field [next]
+  has an incomplete type.  However, recursions that go through a pointer type
+  are correctly handled:
+<<
+    struct s { int x; struct s * next; }
+>>
+  Here, [next] has a pointer type, which is always complete, even though
+  [s] is not yet bound to a composite.
+*)
+
+Program Definition composite_of_def
+     (env: composite_env) (id: ident) (su: struct_or_union) (m: members) (a: attr)
+     : res composite :=
+  match env!id, complete_members env m return _ with
+  | Some _, _ =>
+      Error (MSG "Multiple definitions of struct or union " :: CTX id :: nil)
+  | None, false =>
+      Error (MSG "Incomplete struct or union " :: CTX id :: nil)
+  | None, true =>
+      let al := align_attr a (alignof_composite env m) in
+      OK {| co_su := su;
+            co_members := m;
+            co_attr := a;
+            co_sizeof := align (sizeof_composite env su m) al;
+            co_alignof := al;
+            co_sizeof_pos := _;
+            co_alignof_two_p := _;
+            co_sizeof_alignof := _ |}
+  end.
+Next Obligation.
+  apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. 
+  apply align_le; apply alignof_composite_pos.
+Qed.
+Next Obligation.
+  apply align_attr_two_p. apply alignof_composite_two_p.
+Qed.
+Next Obligation.
+  apply align_divides. apply alignof_composite_pos.
+Qed.
+
+(** The composite environment for a program is obtained by entering
+  its composite definitions in sequence.  The definitions are assumed
+  to be listed in dependency order: the definition of a composite
+  must precede all uses of this composite, unless the use is under
+  a pointer or function type. *)
+
+Local Open Scope error_monad_scope.
+
+Fixpoint add_composite_definitions (env: composite_env) (defs: list composite_definition) : res composite_env :=
+  match defs with
+  | nil => OK env
+  | Composite id su m a :: defs =>
+      do co <- composite_of_def env id su m a;
+      add_composite_definitions (PTree.set id co env) defs
+  end.
+
+Definition build_composite_env (defs: list composite_definition) :=
+  add_composite_definitions (PTree.empty _) defs.
+
+(** Stability properties for alignments and sizes.  If the type is
+  complete in a composite environment [env], its size and alignment
+  are unchanged if we add more definitions to [env]. *)
+
+Section STABILITY.
+
+Variables env env': composite_env.
+Hypothesis extends: forall id co, env!id = Some co -> env'!id = Some co.
+
+Lemma alignof_stable:
+  forall t, complete_type env t = true -> alignof env' t = alignof env t.
+Proof.
+  induction t; simpl; intros; f_equal; auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+Qed.
+
+Lemma sizeof_stable:
+  forall t, complete_type env t = true -> sizeof env' t = sizeof env t.
+Proof.
+  induction t; simpl; intros; auto.
+  rewrite IHt by auto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+Qed.
+
+Lemma complete_type_stable:
+  forall t, complete_type env t = true -> complete_type env' t = true.
+Proof.
+  induction t; simpl; intros; auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+Qed.
+
+Lemma alignof_composite_stable:
+  forall m, complete_members env m = true -> alignof_composite env' m = alignof_composite env m.
+Proof.
+  induction m as [|[id t]]; simpl; intros. 
+  auto.
+  InvBooleans. rewrite alignof_stable by auto. rewrite IHm by auto. auto.
+Qed.
+
+Lemma sizeof_struct_stable:
+  forall m pos, complete_members env m = true -> sizeof_struct env' pos m = sizeof_struct env pos m.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+  auto.
+  InvBooleans. rewrite alignof_stable by auto. rewrite sizeof_stable by auto. 
+  rewrite IHm by auto. auto.
+Qed.
+
+Lemma sizeof_union_stable:
+  forall m, complete_members env m = true -> sizeof_union env' m = sizeof_union env m.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+  auto.
+  InvBooleans. rewrite sizeof_stable by auto. rewrite IHm by auto. auto.
+Qed.
+
+Lemma sizeof_composite_stable:
+  forall su m, complete_members env m = true -> sizeof_composite env' su m = sizeof_composite env su m.
+Proof.
+  intros. destruct su; simpl. 
+  apply sizeof_struct_stable; auto. 
+  apply sizeof_union_stable; auto.
+Qed.
+
+Lemma complete_members_stable:
+  forall m, complete_members env m = true -> complete_members env' m = true.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+  auto.
+  InvBooleans. rewrite complete_type_stable by auto. rewrite IHm by auto. auto.
+Qed.
+
+End STABILITY.
+
+Lemma add_composite_definitions_incr:
+  forall id co defs env1 env2,
+  add_composite_definitions env1 defs = OK env2 ->
+  env1!id = Some co -> env2!id = Some co.
+Proof.
+  induction defs; simpl; intros.
+- inv H; auto.
+- destruct a; monadInv H. 
+  eapply IHdefs; eauto. rewrite PTree.gso; auto.
+  red; intros; subst id0. unfold composite_of_def in EQ. rewrite H0 in EQ; discriminate.
+Qed.
+
+(** It follows that the sizes and alignments contained in the composite
+  environment produced by [build_composite_env] are consistent with
+  the sizes and alignments of the members of the composite types. *)
+
+Definition composite_consistent (env: composite_env) (co: composite) : Prop :=
+     complete_members env (co_members co) = true
+  /\ co_alignof co = align_attr (co_attr co) (alignof_composite env (co_members co))
+  /\ co_sizeof co = align (sizeof_composite env (co_su co) (co_members co)) (co_alignof co).
+
+Definition composite_env_consistent (env: composite_env) : Prop :=
+  forall id co, env!id = Some co -> composite_consistent env co.
+
+Theorem build_composite_env_consistent:
+  forall defs env, build_composite_env defs = OK env -> composite_env_consistent env.
+Proof.
+  cut (forall defs env0 env,
+       add_composite_definitions env0 defs = OK env ->
+       composite_env_consistent env0 ->
+       composite_env_consistent env).
+  intros. eapply H; eauto. red; intros. rewrite PTree.gempty in H1; discriminate.
+  induction defs as [|d1 defs]; simpl; intros.
+- inv H; auto.
+- 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 (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).
++ subst id0. inversion H2; clear H2. subst co. 
+  red; rewrite <- H1; simpl. 
+  assert (A: alignof_composite env1 m = alignof_composite env0 m)
+  by (apply alignof_composite_stable; assumption).
+  rewrite A.
+  split. eapply complete_members_stable; eauto. 
+  split. auto.
+  f_equal. symmetry. apply sizeof_composite_stable; assumption.
++ exploit H0; eauto. intros (P & Q & R).
+  assert (A: alignof_composite env1 (co_members co) = alignof_composite env0 (co_members co))
+  by (apply alignof_composite_stable; assumption).
+  red. rewrite A.
+  split. eapply complete_members_stable; eauto. 
+  split. auto.
+  rewrite R. f_equal. symmetry. apply sizeof_composite_stable; assumption.
+Qed.
+
+(** Moreover, every composite definition is reflected in the composite environment. *)
+
+Theorem build_composite_env_charact:
+  forall id su m a defs env,
+  build_composite_env defs = OK env ->
+  In (Composite id su m a) defs ->
+  exists co, env!id = Some co /\ co_members co = m /\ co_attr co = a /\ co_su co = su.
+Proof.
+  intros until defs. unfold build_composite_env. generalize (PTree.empty composite) as env0. 
+  revert defs. induction defs as [|d1 defs]; simpl; intros.
+- contradiction.
+- destruct d1; monadInv H.
+  destruct H0; [idtac|eapply IHdefs;eauto]. inv H. 
+  unfold composite_of_def in EQ. 
+  destruct (env0!id) eqn:E; try discriminate. 
+  destruct (complete_members env0 m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
+  exists x.
+  split. eapply add_composite_definitions_incr; eauto. apply PTree.gss.
+  subst x; auto.
+Qed.
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 6f193cd9..025960d7 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -13,6 +13,7 @@
 (** Compile-time evaluation of initializers for global C variables. *)
 
 Require Import Coqlib.
+Require Import Maps.
 Require Import Errors.
 Require Import Integers.
 Require Import Floats.
@@ -51,7 +52,13 @@ Definition do_cast (v: val) (t1 t2: type) : res val :=
   | None => Error(msg "undefined cast")
   end.
 
-Fixpoint constval (a: expr) : res val :=
+Definition lookup_composite (ce: composite_env) (id: ident) : res composite :=
+  match ce!id with
+  | Some co => OK co
+  | None => Error (MSG "Undefined struct or union " :: CTX id :: nil)
+  end.
+
+Fixpoint constval (ce: composite_env) (a: expr) : res val :=
   match a with
   | Eval v ty =>
       match v with
@@ -60,74 +67,75 @@ Fixpoint constval (a: expr) : res val :=
       end
   | Evalof l ty =>
       match access_mode ty with
-      | By_reference | By_copy => constval l
+      | By_reference | By_copy => constval ce l
       | _ => Error(msg "dereferencing of an l-value")
       end
   | Eaddrof l ty =>
-      constval l
+      constval ce l
   | Eunop op r1 ty =>
-      do v1 <- constval r1;
+      do v1 <- constval ce r1;
       match sem_unary_operation op v1 (typeof r1) with
       | Some v => OK v
       | None => Error(msg "undefined unary operation")
       end
   | Ebinop op r1 r2 ty =>
-      do v1 <- constval r1;
-      do v2 <- constval r2;
-      match sem_binary_operation op v1 (typeof r1) v2 (typeof r2) Mem.empty with
+      do v1 <- constval ce r1;
+      do v2 <- constval ce r2;
+      match sem_binary_operation ce op v1 (typeof r1) v2 (typeof r2) Mem.empty with
       | Some v => OK v
       | None => Error(msg "undefined binary operation")
       end
   | Ecast r ty =>
-      do v1 <- constval r; do_cast v1 (typeof r) ty
+      do v1 <- constval ce r; do_cast v1 (typeof r) ty
   | Esizeof ty1 ty =>
-      OK (Vint (Int.repr (sizeof ty1)))
+      OK (Vint (Int.repr (sizeof ce ty1)))
   | Ealignof ty1 ty =>
-      OK (Vint (Int.repr (alignof ty1)))
+      OK (Vint (Int.repr (alignof ce ty1)))
   | Eseqand r1 r2 ty =>
-      do v1 <- constval r1;
-      do v2 <- constval r2;
+      do v1 <- constval ce r1;
+      do v2 <- constval ce r2;
       match bool_val v1 (typeof r1) with
       | Some true => do_cast v2 (typeof r2) type_bool
       | Some false => OK (Vint Int.zero)
       | None => Error(msg "undefined && operation")
       end
   | Eseqor r1 r2 ty =>
-      do v1 <- constval r1;
-      do v2 <- constval r2;
+      do v1 <- constval ce r1;
+      do v2 <- constval ce r2;
       match bool_val v1 (typeof r1) with
       | Some false => do_cast v2 (typeof r2) type_bool
       | Some true => OK (Vint Int.one)
       | None => Error(msg "undefined || operation")
       end
   | Econdition r1 r2 r3 ty =>
-      do v1 <- constval r1;
-      do v2 <- constval r2;
-      do v3 <- constval r3;
+      do v1 <- constval ce r1;
+      do v2 <- constval ce r2;
+      do v3 <- constval ce r3;
       match bool_val v1 (typeof r1) with
       | Some true => do_cast v2 (typeof r2) ty
       | Some false => do_cast v3 (typeof r3) ty
       | None => Error(msg "condition is undefined")
       end
   | Ecomma r1 r2 ty =>
-      do v1 <- constval r1; constval r2
+      do v1 <- constval ce r1; constval ce r2
   | Evar x ty =>
       OK(Vptr x Int.zero)
   | Ederef r ty =>
-      constval r
+      constval ce r
   | Efield l f ty =>
       match typeof l with
-      | Tstruct id fList _ =>
-          do delta <- field_offset f fList;
-          do v <- constval l;
+      | Tstruct id _ =>
+          do co <- lookup_composite ce id;
+          do delta <- field_offset ce f (co_members co);
+          do v <- constval ce l;
           OK (Val.add v (Vint (Int.repr delta)))
-      | Tunion id fList _ =>
-          constval l
+      | Tunion id _ =>
+          constval ce l
       | _ =>
           Error(msg "ill-typed field access")
       end
   | Eparen r tycast ty =>
-      do v <- constval r; do_cast v (typeof r) tycast
+      do v <- constval ce r; do_cast v (typeof r) tycast
   | _ =>
     Error(msg "not a compile-time constant")
   end.
@@ -146,21 +154,19 @@ with initializer_list :=
 (** Translate an initializing expression [a] for a scalar variable
   of type [ty].  Return the corresponding initialization datum. *)
 
-Definition transl_init_single (ty: type) (a: expr) : res init_data :=
-  do v1 <- constval a;
+Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res init_data :=
+  do v1 <- constval ce a;
   do v2 <- do_cast v1 (typeof a) ty;
   match v2, ty with
   | Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n)
   | Vint n, Tint I16 sg _ => OK(Init_int16 n)
   | Vint n, Tint I32 sg _ => OK(Init_int32 n)
   | Vint n, Tpointer _ _ => OK(Init_int32 n)
-  | Vint n, Tcomp_ptr _ _ => OK(Init_int32 n)
   | Vlong n, Tlong _ _ => OK(Init_int64 n)
   | Vsingle f, Tfloat F32 _ => OK(Init_float32 f)
   | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
   | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
   | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
-  | Vptr id ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs)
   | Vundef, _ => Error(msg "undefined operation in initializer")
   | _, _ => Error (msg "type mismatch in initializer")
   end.
@@ -171,46 +177,55 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
 Definition padding (frm to: Z) : list init_data :=
   if zlt frm to then Init_space (to - frm) :: nil else nil.
 
-Fixpoint transl_init (ty: type) (i: initializer)
+Fixpoint transl_init (ce: composite_env) (ty: type) (i: initializer)
                      {struct i} : res (list init_data) :=
   match i, ty with
   | Init_single a, _ =>
-      do d <- transl_init_single ty a; OK (d :: nil)
+      do d <- transl_init_single ce ty a; OK (d :: nil)
   | Init_array il, Tarray tyelt nelt _ =>
-      transl_init_array tyelt il (Zmax 0 nelt)
-  | Init_struct il, Tstruct id fl _ =>
-      transl_init_struct id ty fl il 0
-  | Init_union f i1, Tunion id fl _ =>
-      do ty1 <- field_type f fl;
-      do d <- transl_init ty1 i1;
-      OK (d ++ padding (sizeof ty1) (sizeof ty))
+      transl_init_array ce tyelt il (Zmax 0 nelt)
+  | Init_struct il, Tstruct id _ =>
+      do co <- lookup_composite ce id;
+      match co_su co with
+      | Struct => transl_init_struct ce ty (co_members co) il 0
+      | Union  => Error (MSG "struct/union mismatch on " :: CTX id :: nil)
+      end
+  | Init_union f i1, Tunion id _ =>
+      do co <- lookup_composite ce id;
+      match co_su co with
+      | Struct => Error (MSG "union/struct mismatch on " :: CTX id :: nil)
+      | Union =>
+          do ty1 <- field_type f (co_members co);
+          do d <- transl_init ce ty1 i1;
+          OK (d ++ padding (sizeof ce ty1) (sizeof ce ty))
+      end
   | _, _ =>
       Error (msg "wrong type for compound initializer")
   end
 
-with transl_init_array (ty: type) (il: initializer_list) (sz: Z)
+with transl_init_array (ce: composite_env) (ty: type) (il: initializer_list) (sz: Z)
                        {struct il} : res (list init_data) :=
   match il with
   | Init_nil =>
       if zeq sz 0 then OK nil
-      else if zle 0 sz then OK (Init_space (sz * sizeof ty) :: nil)
+      else if zle 0 sz then OK (Init_space (sz * sizeof ce ty) :: nil)
       else Error (msg "wrong number of elements in array initializer")
   | Init_cons i1 il' =>
-      do d1 <- transl_init ty i1;
-      do d2 <- transl_init_array ty il' (sz - 1);
+      do d1 <- transl_init ce ty i1;
+      do d2 <- transl_init_array ce ty il' (sz - 1);
       OK (d1 ++ d2)
   end
 
-with transl_init_struct (id: ident) (ty: type)
-                        (fl: fieldlist) (il: initializer_list) (pos: Z)
+with transl_init_struct (ce: composite_env) (ty: type)
+                        (fl: members) (il: initializer_list) (pos: Z)
                         {struct il} : res (list init_data) :=
   match il, fl with
-  | Init_nil, Fnil =>
-      OK (padding pos (sizeof ty))
-  | Init_cons i1 il', Fcons _ ty1 fl' =>
-      let pos1 := align pos (alignof ty1) in
-      do d1 <- transl_init ty1 i1;
-      do d2 <- transl_init_struct id ty fl' il' (pos1 + sizeof ty1);
+  | Init_nil, nil =>
+      OK (padding pos (sizeof ce ty))
+  | Init_cons i1 il', (_, ty1) :: fl' =>
+      let pos1 := align pos (alignof ce ty1) in
+      do d1 <- transl_init ce ty1 i1;
+      do d2 <- transl_init_struct ce ty fl' il' (pos1 + sizeof ce ty1);
       OK (padding pos pos1 ++ d1 ++ d2)
   | _, _ =>
       Error (msg "wrong number of elements in struct initializer")
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 73fd90b7..225dc23e 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -90,13 +90,13 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
       eval_simple_lvalue (Ederef r ty) b ofs
-  | esl_field_struct: forall r f ty b ofs id fList a delta,
+  | esl_field_struct: forall r f ty b ofs id co a delta,
       eval_simple_rvalue r (Vptr b ofs) ->
-      typeof r = Tstruct id fList a -> field_offset f fList = OK delta ->
+      typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta ->
       eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta))
-  | esl_field_union: forall r f ty b ofs id fList a,
+  | esl_field_union: forall r f ty b ofs id a,
       eval_simple_rvalue r (Vptr b ofs) ->
-      typeof r = Tunion id fList a ->
+      typeof r = Tunion id a ->
       eval_simple_lvalue (Efield r f ty) b ofs
 
 with eval_simple_rvalue: expr -> val -> Prop :=
@@ -116,16 +116,16 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Eunop op r1 ty) v
   | esr_binop: forall op r1 r2 ty v1 v2 v,
       eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 ->
-      sem_binary_operation op v1 (typeof r1) v2 (typeof r2) m = Some v ->
+      sem_binary_operation ge op v1 (typeof r1) v2 (typeof r2) m = Some v ->
       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 ->
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
-      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1)))
+      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
   | esr_alignof: forall ty1 ty,
-      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1)))
+      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1)))
   | esr_seqand_true: forall r1 r2 ty v1 v2 v3,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true ->
       eval_simple_rvalue r2 v2 ->
@@ -372,13 +372,13 @@ Lemma constval_rvalue:
   forall m a v,
   eval_simple_rvalue empty_env m a v ->
   forall v',
-  constval a = OK v' ->
+  constval ge a = OK v' ->
   val_inject inj v' v
 with constval_lvalue:
   forall m a b ofs,
   eval_simple_lvalue empty_env m a b ofs ->
   forall v',
-  constval a = OK v' ->
+  constval ge a = OK v' ->
   val_inject inj v' (Vptr b ofs).
 Proof.
   (* rvalue *)
@@ -394,7 +394,7 @@ Proof.
   exploit sem_unary_operation_inject. eexact E. eauto. 
   intros [v' [A B]]. congruence.
   (* binop *)
-  destruct (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2.
+  destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2.
   exploit (sem_binary_operation_inj inj Mem.empty m).
   intros. rewrite mem_empty_not_valid_pointer in H3; discriminate.
   intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate.
@@ -443,8 +443,9 @@ Proof.
   (* deref *)
   eauto.
   (* field struct *)
-  rewrite H0 in CV. monadInv CV. exploit constval_rvalue; eauto. intro MV. inv MV.
-  simpl. replace x with delta by congruence. econstructor; eauto. 
+  rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. 
+  exploit constval_rvalue; eauto. intro MV. inv MV.
+  simpl. replace x0 with delta by congruence. econstructor; eauto. 
   rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. 
   simpl. auto.
   (* field union *)
@@ -452,7 +453,7 @@ Proof.
 Qed.
 
 Lemma constval_simple:
-  forall a v, constval a = OK v -> simple a.
+  forall a v, constval ge a = OK v -> simple a.
 Proof.
   induction a; simpl; intros vx CV; try (monadInv CV); eauto.
   destruct (typeof a); discriminate || eauto.
@@ -466,7 +467,7 @@ Qed.
 Theorem constval_steps:
   forall f r m v v' ty m',
   star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') ->
-  constval r = OK v ->
+  constval ge r = OK v ->
   m' = m /\ ty = typeof r /\ val_inject inj v v'.
 Proof.
   intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. 
@@ -479,7 +480,7 @@ Qed.
 
 Theorem transl_init_single_steps:
   forall ty a data f m v1 ty1 m' v chunk b ofs m'',
-  transl_init_single ty a = OK data ->
+  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 ->
   access_mode ty = By_value chunk ->
@@ -522,15 +523,14 @@ Qed.
 
 Lemma transl_init_single_size:
   forall ty a data,
-  transl_init_single ty a = OK data ->
-  Genv.init_data_size data = sizeof ty.
+  transl_init_single ge ty a = OK data ->
+  Genv.init_data_size data = sizeof ge ty.
 Proof.
   intros. monadInv H. destruct x0. 
 - monadInv EQ2.
 - destruct ty; try discriminate. 
   destruct i0; inv EQ2; auto.
   inv EQ2; auto.
-  inv EQ2; auto.
 - destruct ty; inv EQ2; auto.
 - destruct ty; try discriminate.
   destruct f0; inv EQ2; auto.
@@ -539,7 +539,6 @@ Proof.
 - destruct ty; try discriminate.
   destruct i0; inv EQ2; auto.
   inv EQ2; auto.
-  inv EQ2; auto.
 Qed.
 
 Notation idlsize := Genv.init_data_list_size.
@@ -561,30 +560,32 @@ Proof.
 Qed.
 
 Remark union_field_size:
-  forall f ty fl, field_type f fl = OK ty -> sizeof ty <= sizeof_union fl.
+  forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl.
 Proof.
-  induction fl; simpl; intros. 
+  induction fl as [|[i t]]; simpl; intros. 
 - inv H.
 - destruct (ident_eq f i). 
   + inv H. xomega. 
   + specialize (IHfl H). xomega. 
 Qed.
 
+Hypothesis ce_consistent: composite_env_consistent ge.
+
 Lemma transl_init_size:
   forall i ty data,
-  transl_init ty i = OK data ->
-  idlsize data = sizeof ty
+  transl_init ge ty i = OK data ->
+  idlsize data = sizeof ge ty
 
 with transl_init_list_size:
   forall il,
   (forall ty sz data,
-   transl_init_array ty il sz = OK data ->
-   idlsize data = sizeof ty * sz)
+   transl_init_array ge ty il sz = OK data ->
+   idlsize data = sizeof ge ty * sz)
   /\
-  (forall id ty fl pos data,
-   transl_init_struct id ty fl il pos = OK data ->
-   sizeof_struct fl pos <= sizeof ty ->
-   idlsize data + pos = sizeof ty).
+  (forall ty fl pos data,
+   transl_init_struct ge ty fl il pos = OK data ->
+   sizeof_struct ge pos fl <= sizeof ge ty ->
+   idlsize data + pos = sizeof ge ty).
 
 Proof.
 - induction i; intros. 
@@ -595,27 +596,35 @@ Proof.
   simpl. eapply (proj1 (transl_init_list_size il)); eauto.
 + (* struct *)
   simpl in H. destruct ty; try discriminate.
+  monadInv H. destruct (co_su x) eqn:?; try discriminate.
   replace (idlsize data) with (idlsize data + 0) by omega.
   eapply (proj2 (transl_init_list_size il)). eauto.
-Local Opaque alignof.
-  simpl. apply align_le. apply alignof_pos.
+  unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i) as [co|] eqn:?; inv EQ.
+  exploit ce_consistent; eauto. intros (A & B & C).
+  rewrite C. unfold sizeof_composite. rewrite Heqs. apply align_le.
+  destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 + (* union *)
   simpl in H. destruct ty; try discriminate.
-  set (sz := sizeof (Tunion i0 f0 a)) in *.
-  monadInv H. rewrite idlsize_app. rewrite (IHi _ _ EQ1). 
-  rewrite padding_size. omega. unfold sz. simpl. 
-  apply Zle_trans with (sizeof_union f0). eapply union_field_size; eauto.
-  apply align_le. apply alignof_pos. 
+  monadInv H. destruct (co_su x) eqn:?; try discriminate.
+  monadInv EQ0. 
+  rewrite idlsize_app. rewrite (IHi _ _ EQ0).
+  unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i0) as [co|] eqn:?; inv EQ.
+  rewrite padding_size. omega.
+  apply Zle_trans with (sizeof_union ge (co_members x)). 
+  eapply union_field_size; eauto.
+  exploit ce_consistent; eauto. intros (A & B & C).
+  rewrite C. unfold sizeof_composite. rewrite Heqs. apply align_le.
+  destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 
 - induction il.
 + (* base cases *)
-  simpl. intuition. 
+  simpl. intuition auto.
 * (* arrays *)
   destruct (zeq sz 0).  inv H.  simpl; ring. 
   destruct (zle 0 sz);  inv H.  simpl. 
   rewrite Z.mul_comm. 
-  assert (0 <= sizeof ty * sz).
-  { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ty); omega. }
+  assert (0 <= sizeof ge ty * sz).
+  { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. }
   zify; omega.
 * (* structs *)
   destruct fl; inv H.
@@ -629,12 +638,12 @@ Local Opaque alignof.
   rewrite (A _ _ _ EQ1).
   ring.
 * (* structs *)
-  intros. simpl in H. destruct fl; monadInv H.
+  intros. simpl in H. destruct fl as [|[i1 t1]]; monadInv H.
   rewrite ! idlsize_app. 
   simpl in H0. 
   rewrite padding_size.
   rewrite (transl_init_size _ _ _ EQ). 
-  rewrite <- (B _ _ _ _ _ EQ1). omega.
+  rewrite <- (B _ _ _ _ EQ1). omega.
   auto. apply align_le. apply alignof_pos. 
 Qed.
 
@@ -642,11 +651,11 @@ Qed.
 
 Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip.
 
-Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list (Z * type) :=
+Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) :=
   match fl with
-  | Fnil => nil
-  | Fcons id1 ty1 fl' =>
-      (align pos (alignof ty1), ty1) :: fields_of_struct id ty fl' (align pos (alignof ty1) + sizeof ty1)
+  | nil => nil
+  | (id1, ty1) :: fl' =>
+      (align pos (alignof ge ty1), ty1) :: fields_of_struct fl' (align pos (alignof ge ty1) + sizeof ge ty1)
   end.
 
 Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
@@ -660,13 +669,15 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
   | exec_init_array_: forall m b ofs ty sz a il m',
       exec_init_array m b ofs ty sz il m' ->
       exec_init m b ofs (Tarray ty sz a) (Init_array il) m'
-  | exec_init_struct: forall m b ofs id fl a il m',
-      exec_init_list m b ofs (fields_of_struct id (Tstruct id fl a) fl 0) il m' ->
-      exec_init m b ofs (Tstruct id fl a) (Init_struct il) m'
-  | exec_init_union: forall m b ofs id fl a f i ty m',
-      field_type f fl = OK ty ->
+  | exec_init_struct: forall m b ofs id a il co m',
+      ge.(genv_cenv)!id = Some co -> co_su co = Struct ->
+      exec_init_list m b ofs (fields_of_struct (co_members co) 0) il m' ->
+      exec_init m b ofs (Tstruct id a) (Init_struct il) m'
+  | exec_init_union: forall m b ofs id a f i ty co m',
+      ge.(genv_cenv)!id = Some co -> co_su co = Union ->
+      field_type f (co_members co) = OK ty ->
       exec_init m b ofs ty i m' ->
-      exec_init m b ofs (Tunion id fl a) (Init_union f i) m'
+      exec_init m b ofs (Tunion id a) (Init_union f i) m'
 
 with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop :=
   | exec_init_array_nil: forall m b ofs ty sz,
@@ -674,7 +685,7 @@ with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem
       exec_init_array m b ofs ty sz Init_nil m
   | exec_init_array_cons: forall m b ofs ty sz i1 il m' m'',
       exec_init m b ofs ty i1 m' ->
-      exec_init_array m' b (ofs + sizeof ty) ty (sz - 1) il m'' ->
+      exec_init_array m' b (ofs + sizeof ge ty) ty (sz - 1) il m'' ->
       exec_init_array m b ofs ty sz (Init_cons i1 il) m''
 
 with exec_init_list: mem -> block -> Z -> list (Z * type) -> initializer_list -> mem -> Prop :=
@@ -718,15 +729,15 @@ Qed.
 
 Lemma transl_init_sound_gen:
   (forall m b ofs ty i m', exec_init m b ofs ty i m' ->
-   forall data, transl_init ty i = OK data ->
+   forall data, transl_init ge ty i = OK data ->
    Genv.store_init_data_list ge m b ofs data = Some m')
 /\(forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' ->
-   forall data, transl_init_array ty il sz = OK data ->
+   forall data, transl_init_array ge ty il sz = OK data ->
    Genv.store_init_data_list ge m b ofs data = Some m')
 /\(forall m b ofs l il m', exec_init_list m b ofs l il m' ->
-   forall id ty fl data pos,
-   l = fields_of_struct id ty fl pos ->
-   transl_init_struct id ty fl il pos = OK data ->
+   forall ty fl data pos,
+   l = fields_of_struct fl pos ->
+   transl_init_struct ge ty fl il pos = OK data ->
    Genv.store_init_data_list ge m b (ofs + pos) data = Some m').
 Proof.
 Local Opaque sizeof.
@@ -737,9 +748,11 @@ Local Opaque sizeof.
   replace (Z.max 0 sz) with sz in H1. eauto.
   assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. 
 - (* struct *)
+  unfold lookup_composite in H3. rewrite H in H3. simpl in H3. rewrite H0 in H3. 
   replace ofs with (ofs + 0) by omega. eauto.
 - (* union *)
-  rewrite H in H2. monadInv H2. inv EQ.  
+  unfold lookup_composite in H4. rewrite H in H4. simpl in H4. rewrite H0 in H4. 
+  monadInv H4. assert (x = ty) by congruence. subst x.  
   eapply store_init_data_list_app. eauto.
   apply store_init_data_list_padding. 
 
@@ -753,15 +766,15 @@ Local Opaque sizeof.
   eauto.
   rewrite (transl_init_size _ _ _ EQ). eauto.
 - (* struct, empty *)
-  destruct fl; simpl in H; inv H. 
-  inv H0. apply store_init_data_list_padding.
+  destruct fl as [|[i t]]; simpl in H0; inv H0. 
+  apply store_init_data_list_padding.
 - (* struct, nonempty *)
-  destruct fl; simpl in H3; inv H3.
-  monadInv H4. 
+  destruct fl as [|[i t]]; simpl in H4; monadInv H4.
+  simpl in H3; inv H3.
   eapply store_init_data_list_app. apply store_init_data_list_padding.
   rewrite padding_size. 
-  replace (ofs + pos0 + (align pos0 (alignof t) - pos0))
-     with (ofs + align pos0 (alignof t)) by omega.
+  replace (ofs + pos0 + (align pos0 (alignof ge t) - pos0))
+     with (ofs + align pos0 (alignof ge t)) by omega.
   eapply store_init_data_list_app.
   eauto.
   rewrite (transl_init_size _ _ _ EQ).
@@ -769,15 +782,18 @@ Local Opaque sizeof.
   apply align_le. apply alignof_pos.
 Qed.
 
+End SOUNDNESS.
+
 Theorem transl_init_sound:
-  forall m b ty i m' data,
-  exec_init m b 0 ty i m' ->
-  transl_init ty i = OK data ->
-  Genv.store_init_data_list ge m b 0 data = Some m'.
+  forall p m b ty i m' data,
+  exec_init (globalenv p) m b 0 ty i m' ->
+  transl_init (prog_comp_env p) ty i = OK data ->
+  Genv.store_init_data_list (globalenv p) m b 0 data = Some m'.
 Proof.
-  intros. eapply (proj1 transl_init_sound_gen); eauto.
+  intros. 
+  set (ge := globalenv p) in *.
+  change (prog_comp_env p) with (genv_cenv ge) in H0.
+  destruct (transl_init_sound_gen ge) as (A & B & C).
+  eapply build_composite_env_consistent. apply prog_comp_env_eq.
+  eapply A; eauto.
 Qed.
-
-End SOUNDNESS.
-
-
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index c5a6e6e1..ebd06c54 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -45,6 +45,8 @@ let rec precedence = function
   | Econst_float _ -> (16, NA)
   | Econst_single _ -> (16, NA)
   | Econst_long _ -> (16, NA)
+  | Esizeof _ -> (15, RtoL)
+  | Ealignof _ -> (15, RtoL)
   | Eunop _ -> (15, RtoL)
   | Eaddrof _ -> (15, RtoL)
   | Ecast _ -> (14, RtoL)
@@ -100,6 +102,10 @@ let rec expr p (prec, e) =
                  expr (prec1, a1) (name_binop op) expr (prec2, a2)
   | Ecast(a1, ty) ->
       fprintf p "(%s) %a" (name_type ty) expr (prec', a1)
+  | Esizeof(ty, _) ->
+      fprintf p "sizeof(%s)" (name_type ty)
+  | Ealignof(ty, _) ->
+      fprintf p "__alignof__(%s)" (name_type ty)
   end;
   if prec' < prec then fprintf p ")@]" else fprintf p "@]"
 
@@ -265,71 +271,10 @@ let print_globdef p (id, gd) =
   | Gfun f -> print_fundef p id f
   | Gvar v -> print_globvar p id v  (* from PrintCsyntax *)
 
-(* Collect struct and union types *)
-
-let rec collect_expr e =
-  collect_type (typeof e);
-  match e with
-  | Econst_int _ -> ()
-  | Econst_float _ -> ()
-  | Econst_single _ -> ()
-  | Econst_long _ -> ()
-  | Evar _ -> ()
-  | Etempvar _ -> ()
-  | Ederef(r, _) -> collect_expr r
-  | Efield(l, _, _) -> collect_expr l
-  | Eaddrof(l, _) -> collect_expr l
-  | Eunop(_, r, _) -> collect_expr r
-  | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2
-  | Ecast(r, _) -> collect_expr r
-
-let rec collect_exprlist = function
-  | [] -> ()
-  | r1 :: rl -> collect_expr r1; collect_exprlist rl
-
-let rec collect_stmt = function
-  | Sskip -> ()
-  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
-  | Sset(id, e2) -> collect_expr e2
-  | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el
-  | Sbuiltin(optid, ef, tyargs, el) -> collect_exprlist el
-  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
-  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
-  | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2
-  | Sbreak -> ()
-  | Scontinue -> ()
-  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
-  | Sreturn None -> ()
-  | Sreturn (Some e) -> collect_expr e
-  | Slabel(lbl, s) -> collect_stmt s
-  | Sgoto lbl -> ()
-
-and collect_cases = function
-  | LSnil -> ()
-  | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem
-
-let collect_function f =
-  collect_type f.fn_return;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_temps;
-  collect_stmt f.fn_body
-
-let collect_globdef (id, gd) =
-  match gd with
-  | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res
-  | Gfun(Internal f) -> collect_function f
-  | Gvar v -> collect_type v.gvar_info
-
-let collect_program p =
-  List.iter collect_globdef p.prog_defs
-
 let print_program p prog =
-  struct_unions := StructUnion.empty;
-  collect_program prog;
   fprintf p "@[<v 0>";
-  StructUnion.iter (declare_struct_or_union p) !struct_unions;
-  StructUnion.iter (print_struct_or_union p) !struct_unions;
+  List.iter (declare_composite p) prog.prog_types;
+  List.iter (define_composite p) prog.prog_types;
   List.iter (print_globdef p) prog.prog_defs;
   fprintf p "@]@."
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index e1b53af8..8a4d60a5 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -70,12 +70,6 @@ let name_longtype sg =
   | Signed -> "long long"
   | Unsigned -> "unsigned long long"
 
-(* Collecting the names and fields of structs and unions *)
-
-module StructUnion = Map.Make(String)
-
-let struct_unions = ref StructUnion.empty
-
 (* Declarator (identifier + type) *)
 
 let attributes a =
@@ -132,12 +126,10 @@ let rec name_cdecl id ty =
       add_args true args;
       Buffer.add_char b ')';
       name_cdecl (Buffer.contents b) res
-  | Tstruct(name, fld, a) ->
-      extern_atom name ^ attributes a ^ name_optid id
-  | Tunion(name, fld, a) ->
-      extern_atom name ^ attributes a ^ name_optid id
-  | Tcomp_ptr(name, a) ->
-      extern_atom name ^ " *" ^ attributes a ^ id
+  | Tstruct(name, a) ->
+      "struct " ^ extern_atom name ^ attributes a ^ name_optid id
+  | Tunion(name, a) ->
+      "union " ^ extern_atom name ^ attributes a ^ name_optid id
 
 (* Type *)
 
@@ -466,7 +458,7 @@ let print_globvar p id v =
       fprintf p "@[<hov 2>%s = "
               (name_cdecl name2 v.gvar_info);
       begin match v.gvar_info, v.gvar_init with
-      | (Tint _ | Tlong _ | Tfloat _ | Tpointer _ | Tfunction _ | Tcomp_ptr _),
+      | (Tint _ | Tlong _ | Tfloat _ | Tpointer _ | Tfunction _),
         [i1] ->
           print_init p i1
       | _, il ->
@@ -482,119 +474,24 @@ let print_globdef p (id, gd) =
   | Gfun f -> print_fundef p id f
   | Gvar v -> print_globvar p id v
 
-(* Collect struct and union types *)
-
-let rec collect_type = function
-  | Tvoid -> ()
-  | Tint _ -> ()
-  | Tfloat _ -> ()
-  | Tlong _ -> ()
-  | Tpointer(t, _) -> collect_type t
-  | Tarray(t, _, _) -> collect_type t
-  | Tfunction(args, res, _) -> collect_type_list args; collect_type res
-  | Tstruct(id, fld, _) | Tunion(id, fld, _) ->
-      let s = extern_atom id in
-      if not (StructUnion.mem s !struct_unions) then begin
-        struct_unions := StructUnion.add s fld !struct_unions;
-        collect_fields fld
-      end
-  | Tcomp_ptr _ -> ()
-
-and collect_type_list = function
-  | Tnil -> ()
-  | Tcons(hd, tl) -> collect_type hd; collect_type_list tl
-
-and collect_fields = function
-  | Fnil -> ()
-  | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl
-
-let rec collect_expr e =
-  collect_type (typeof e);
-  match e with
-  | Eloc _ -> assert false
-  | Evar _ -> ()
-  | Ederef(r, _) -> collect_expr r
-  | Efield(l, _, _) -> collect_expr l
-  | Eval _ -> ()
-  | Evalof(l, _) -> collect_expr l
-  | Eaddrof(l, _) -> collect_expr l
-  | Eunop(_, r, _) -> collect_expr r
-  | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2
-  | Ecast(r, _) -> collect_expr r
-  | Eseqand(r1, r2, _) -> collect_expr r1; collect_expr r2
-  | Eseqor(r1, r2, _) -> collect_expr r1; collect_expr r2
-  | Econdition(r1, r2, r3, _) -> 
-      collect_expr r1; collect_expr r2; collect_expr r3
-  | Esizeof(ty, _) -> collect_type ty
-  | Ealignof(ty, _) -> collect_type ty
-  | Eassign(l, r, _) -> collect_expr l; collect_expr r
-  | Eassignop(_, l, r, _, _) -> collect_expr l; collect_expr r
-  | Epostincr(_, l, _) -> collect_expr l
-  | Ecomma(r1, r2, _) -> collect_expr r1; collect_expr r2
-  | Ecall(r1, rl, _) ->  collect_expr r1; collect_exprlist rl
-  | Ebuiltin(_, _, rl, _) -> collect_exprlist rl
-  | Eparen _ -> assert false
-
-and collect_exprlist = function
-  | Enil -> ()
-  | Econs(r1, rl) ->  collect_expr r1; collect_exprlist rl
-
-let rec collect_stmt = function
-  | Sskip -> ()
-  | Sdo e -> collect_expr e
-  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
-  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
-  | Swhile(e, s) -> collect_expr e; collect_stmt s
-  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
-  | Sfor(s_init, e, s_iter, s_body) ->
-      collect_stmt s_init; collect_expr e;
-      collect_stmt s_iter; collect_stmt s_body
-  | Sbreak -> ()
-  | Scontinue -> ()
-  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
-  | Sreturn None -> ()
-  | Sreturn (Some e) -> collect_expr e
-  | Slabel(lbl, s) -> collect_stmt s
-  | Sgoto lbl -> ()
-
-and collect_cases = function
-  | LSnil -> ()
-  | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem
-
-let collect_function f =
-  collect_type f.fn_return;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
-  collect_stmt f.fn_body
-
-let collect_globdef (id, gd) =
-  match gd with
-  | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res
-  | Gfun(Internal f) -> collect_function f
-  | Gvar v -> collect_type v.gvar_info
-
-let collect_program p =
-  List.iter collect_globdef p.prog_defs
-
-let declare_struct_or_union p name fld =
-  fprintf p "%s;@ @ " name
-
-let print_struct_or_union p name fld =
-  fprintf p "@[<v 2>%s {" name;
-  let rec print_fields = function
-  | Fnil -> ()
-  | Fcons(id, ty, rem) ->
-      fprintf p "@ %s;" (name_cdecl (extern_atom id) ty);
-      print_fields rem in
-  print_fields fld;
+let struct_or_union = function Struct -> "struct" | Union -> "union"
+
+let declare_composite p (Composite(id, su, m, a)) =
+  fprintf p "%s %s;@ " (struct_or_union su) (extern_atom id)
+
+let define_composite p (Composite(id, su, m, a)) =
+  fprintf p "@[<v 2>%s %s%s {"
+          (struct_or_union su) (extern_atom id) (attributes a);
+  List.iter
+    (fun (fid, fty) ->
+      fprintf p "@ %s;" (name_cdecl (extern_atom fid) fty))
+    m;
   fprintf p "@;<0 -2>};@]@ @ "
 
 let print_program p prog =
-  struct_unions := StructUnion.empty;
-  collect_program prog;
   fprintf p "@[<v 0>";
-  StructUnion.iter (declare_struct_or_union p) !struct_unions;
-  StructUnion.iter (print_struct_or_union p) !struct_unions;
+  List.iter (declare_composite p) prog.prog_types;
+  List.iter (define_composite p) prog.prog_types;
   List.iter (print_globdef p) prog.prog_defs;
   fprintf p "@]@."
 
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 089797f2..36fe07ae 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -540,5 +540,10 @@ Fixpoint transl_globdefs
   end.
 
 Definition transl_program (p: Csyntax.program) : res program :=
-  do gl' <- transl_globdefs p.(prog_defs) (initial_generator tt);
-  OK (mkprogram gl' p.(prog_public) p.(prog_main)).
+  do gl' <- transl_globdefs (Csyntax.prog_defs p) (initial_generator tt);
+  OK {| prog_defs := gl';
+        prog_public := Csyntax.prog_public p;
+        prog_main := Csyntax.prog_main p;
+        prog_types := Csyntax.prog_types p;
+        prog_comp_env := Csyntax.prog_comp_env p;
+        prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 6d8b5c86..74019061 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -37,11 +37,17 @@ Variable prog: Csyntax.program.
 Variable tprog: Clight.program.
 Hypothesis TRANSL: transl_program prog = OK tprog.
 
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
+Let ge := Csem.globalenv prog.
+Let tge := Clight.globalenv tprog.
 
 (** Invariance properties. *)
 
+Lemma comp_env_preserved:
+  Clight.genv_cenv tge = Csem.genv_cenv ge.
+Proof.
+  monadInv TRANSL. unfold tge; rewrite <- H0; auto. 
+Qed.
+
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
@@ -87,7 +93,7 @@ Proof.
 - 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. fold ge in A. congruence.
+  intros [v [A B]]. inv B. change (Genv.globalenv prog) with (Csem.genv_genv ge) in A. congruence.
 Qed.
 
 Lemma block_is_volatile_preserved:
@@ -173,7 +179,7 @@ Remark assign_loc_translated:
   forall ty m b ofs v t m',
   Csem.assign_loc ge ty m b ofs v t m' ->
   match chunk_for_volatile_type ty with
-  | None => t = E0 /\ Clight.assign_loc ty m b ofs v m'
+  | None => t = E0 /\ Clight.assign_loc tge ty m b ofs v m'
   | Some chunk => volatile_store tge chunk m b ofs v t m'
   end.
 Proof.
@@ -184,7 +190,8 @@ Proof.
   rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto.
   exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved.
   (* By copy *)
-  rewrite H0. destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto.
+  rewrite H0. rewrite <- comp_env_preserved in *. 
+  destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto.
 Qed.
 
 (** Evaluation of simple expressions and of their translation *)
@@ -241,7 +248,7 @@ Opaque makeif.
   exploit H0; eauto. intros [A [B C]].
   exploit H2; eauto. intros [D [E F]].
   subst sl1 sl2; simpl.
-  assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. congruence.
+  assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. rewrite comp_env_preserved; congruence.
   destruct dst; auto. simpl; econstructor; eauto.
 (* cast *)
   exploit H0; eauto. intros [A [B C]].
@@ -249,11 +256,13 @@ Opaque makeif.
   assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence.
   destruct dst; auto. simpl; econstructor; eauto.
 (* sizeof *)
+  rewrite <- comp_env_preserved. 
   destruct dst.
   split; auto. split; auto. constructor.
   auto.
   exists (Esizeof ty1 ty). split. auto. split. auto. constructor.
 (* alignof *)
+  rewrite <- comp_env_preserved. 
   destruct dst.
   split; auto. split; auto. constructor.
   auto.
@@ -267,9 +276,11 @@ Opaque makeif.
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. constructor; auto.
 (* field struct *)
+  rewrite <- comp_env_preserved in *.
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. rewrite B in H1. eapply eval_Efield_struct; eauto.
 (* field union *)
+  rewrite <- comp_env_preserved in *.
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. rewrite B in H1. eapply eval_Efield_union; eauto.
 Qed.
@@ -1659,7 +1670,7 @@ Proof.
   left. eapply star_plus_trans. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC.
   eapply plus_two. simpl. econstructor. eapply step_make_assign; eauto. 
     econstructor. eexact EV3. eexact EV2. 
-    rewrite TY3; rewrite <- TY1; rewrite <- TY2; eauto.
+    rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; auto.
   reflexivity. traceEq.
   econstructor. auto. change sl2 with (nil ++ sl2). apply S.
   constructor. auto. auto. auto.
@@ -1680,7 +1691,7 @@ Proof.
   eapply star_plus_trans. eexact EXEC.
   simpl. eapply plus_four. econstructor. econstructor.
     econstructor. eexact EV3. eexact EV2. 
-    rewrite TY3; rewrite <- TY1; rewrite <- TY2. eauto.
+    rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; eauto.
   econstructor. eapply step_make_assign; eauto. 
     constructor. apply PTree.gss. 
     reflexivity. traceEq.
@@ -1729,8 +1740,8 @@ Proof.
   eapply plus_two. simpl. constructor.
   eapply step_make_assign; eauto. 
   unfold transl_incrdecr. destruct id; simpl in H2. 
-  econstructor. eauto. constructor. simpl. rewrite TY3; rewrite <- TY1. eauto.
-  econstructor. eauto. constructor. simpl. rewrite TY3; rewrite <- TY1. eauto.
+  econstructor. eauto. constructor. rewrite TY3; rewrite <- TY1; rewrite comp_env_preserved. simpl; eauto.
+  econstructor. eauto. constructor. rewrite TY3; rewrite <- TY1; rewrite comp_env_preserved. simpl; eauto.
   destruct id; auto. 
   reflexivity. traceEq.
   econstructor. auto. change sl2 with (nil ++ sl2). apply S.
@@ -1748,8 +1759,10 @@ Proof.
   constructor.
   eapply step_make_assign; eauto. 
   unfold transl_incrdecr. destruct id; simpl in H2. 
-  econstructor. constructor. apply PTree.gss. constructor. simpl. eauto.
-  econstructor. constructor. apply PTree.gss. constructor. simpl. eauto.
+  econstructor. constructor. apply PTree.gss. constructor.
+  rewrite comp_env_preserved; simpl; eauto.
+  econstructor. constructor. apply PTree.gss. constructor.
+  rewrite comp_env_preserved; simpl; eauto.
   destruct id; auto. 
   traceEq.
   econstructor. auto. apply S.
@@ -1900,24 +1913,31 @@ Qed.
 
 Lemma alloc_variables_preserved:
   forall e m params e' m',
-  Csem.alloc_variables e m params e' m' ->
-  alloc_variables e m params e' m'.
+  Csem.alloc_variables ge e m params e' m' ->
+  alloc_variables tge e m params e' m'.
 Proof.
-  induction 1; econstructor; eauto.
+  induction 1; econstructor; eauto. rewrite comp_env_preserved; auto.
 Qed.
 
 Lemma bind_parameters_preserved:
   forall e m params args m',
   Csem.bind_parameters ge e m params args m' ->
-  bind_parameters e m params args m'.
+  bind_parameters tge e m params args m'.
 Proof.
-  induction 1; econstructor; eauto.
-  inv H0. 
-  eapply assign_loc_value; eauto.
-  inv H4. eapply assign_loc_value; eauto. 
-  eapply assign_loc_copy; eauto.
+  induction 1; econstructor; eauto. inv H0. 
+- eapply assign_loc_value; eauto.
+- inv H4. eapply assign_loc_value; eauto.
+- rewrite <- comp_env_preserved in *. eapply assign_loc_copy; eauto.
 Qed.
 
+Lemma blocks_of_env_preserved:
+  forall e, blocks_of_env tge e = Csem.blocks_of_env ge e.
+Proof.
+  intros; unfold blocks_of_env, Csem.blocks_of_env. 
+  unfold block_of_binding, Csem.block_of_binding. 
+  rewrite comp_env_preserved. auto.
+Qed. 
+
 Lemma sstep_simulation:
   forall S1 t S2, Csem.sstep ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
@@ -2090,9 +2110,10 @@ Proof.
   left. apply plus_one. constructor.
   econstructor; eauto. constructor; auto. 
 
+
 (* return none *)
   inv H7. econstructor; split.
-  left. apply plus_one. econstructor; eauto. 
+  left. apply plus_one. econstructor; eauto. rewrite blocks_of_env_preserved; eauto. 
   constructor. apply match_cont_call; auto. 
 (* return some 1 *)
   inv H6. inv H0. econstructor; split.
@@ -2102,14 +2123,14 @@ Proof.
   inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst.
   econstructor; split.
   left. eapply plus_two. constructor. econstructor. eauto.
-  erewrite function_return_preserved; eauto. 
+  erewrite function_return_preserved; eauto. rewrite blocks_of_env_preserved; eauto. 
   eauto. traceEq.
   constructor. apply match_cont_call; auto.
 (* skip return *)
   inv H8. 
   assert (is_call_cont tk). inv H9; simpl in *; auto.
   econstructor; split.
-  left. apply plus_one. apply step_skip_call; eauto.
+  left. apply plus_one. apply step_skip_call; eauto. rewrite blocks_of_env_preserved; eauto. 
   constructor. auto.
 
 (* switch *)
@@ -2198,14 +2219,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. 
+  intros. inv H. generalize TRANSL; intros TR; monadInv TR. rewrite H4. 
   exploit transl_program_spec; eauto. intros MP.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor.
-  exploit Genv.init_mem_match; eauto.  
-  simpl. fold tge. rewrite symbols_preserved.
-  destruct MP as (A & B & C). rewrite B; eexact H1.
+  exploit Genv.init_mem_match; eauto.
+  change (Genv.globalenv tprog) with (genv_genv tge). rewrite symbols_preserved.
+  rewrite <- H4; simpl; eauto. 
   eexact FIND.
   rewrite <- H3. apply type_of_fundef_preserved. auto.
   constructor. auto. constructor.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 83ddd1f4..9f9fb450 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -1144,10 +1144,10 @@ Qed.
 Theorem transl_program_spec:
   forall p tp,
   transl_program p = OK tp ->
-  match_program tr_fundef (fun v1 v2 => v1 = v2) nil p.(prog_main) p tp.
+  match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp.
 Proof.
   unfold transl_program; intros. 
-  destruct (transl_globdefs (prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H.
+  destruct (transl_globdefs (Csyntax.prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H.
   split; auto. exists l; split. eapply transl_globdefs_spec; eauto. 
   rewrite <- app_nil_end; auto.
 Qed.
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 9c529280..52ee8377 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -48,8 +48,8 @@ Definition make_cast (a: expr) (tto: type) : expr :=
   | cast_case_f2f => a
   | cast_case_s2s => a
   | cast_case_l2l => a
-  | cast_case_struct _ _ _ _ => a
-  | cast_case_union _ _ _ _ => a
+  | cast_case_struct _ _ => a
+  | cast_case_union _ _ => a
   | cast_case_void => a
   | _ => Ecast a tto
   end.
@@ -70,6 +70,8 @@ Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr :=
   | Ebinop op a1 a2 ty => Ebinop op (simpl_expr cenv a1) (simpl_expr cenv a2) ty
   | Ecast a1 ty => Ecast (simpl_expr cenv a1) ty
   | Efield a1 fld ty => Efield (simpl_expr cenv a1) fld ty
+  | Esizeof _ _ => a
+  | Ealignof _ _ => a
   end.
 
 Definition simpl_exprlist (cenv: compilenv) (al: list expr) : list expr :=
@@ -170,6 +172,8 @@ Fixpoint addr_taken_expr (a: expr): VSet.t :=
   | Ebinop op a1 a2 ty => VSet.union (addr_taken_expr a1) (addr_taken_expr a2)
   | Ecast a1 ty => addr_taken_expr a1
   | Efield a1 fld ty => addr_taken_expr a1
+  | Esizeof _ _ => VSet.empty
+  | Ealignof _ _ => VSet.empty
   end.
 
 Fixpoint addr_taken_exprlist (l: list expr) : VSet.t :=
@@ -247,6 +251,10 @@ Definition transf_fundef (fd: fundef) : res fundef :=
   end.
 
 Definition transf_program (p: program) : res program :=
-  AST.transform_partial_program transf_fundef p.
-
-
+  do p1 <- AST.transform_partial_program transf_fundef p;
+  OK {| prog_defs := AST.prog_defs p1;
+        prog_public := AST.prog_public p1;
+        prog_main := AST.prog_main p1;
+        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/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 15d0af06..5cf59d94 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -39,25 +39,37 @@ Section PRESERVATION.
 Variable prog: program.
 Variable tprog: program.
 Hypothesis TRANSF: transf_program prog = OK tprog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv 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. 
+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).
+  exact (Genv.find_symbol_transf_partial _ _ transf_programs).
 Qed.
 
 Lemma public_preserved:
   forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
 Proof.
-  exact (Genv.public_symbol_transf_partial _ _ TRANSF).
+  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).
+  exact (Genv.find_var_info_transf_partial _ _ transf_programs).
 Qed.
 
 Lemma functions_translated:
@@ -65,7 +77,7 @@ Lemma functions_translated:
   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).
+  exact (Genv.find_funct_transf_partial _ _ transf_programs).
 Qed.
 
 Lemma function_ptr_translated:
@@ -73,7 +85,7 @@ Lemma function_ptr_translated:
   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).
+  exact (Genv.find_funct_ptr_transf_partial _ _ transf_programs).
 Qed.
 
 Lemma type_of_fundef_preserved:
@@ -207,14 +219,10 @@ Inductive val_casted: val -> type -> Prop :=
       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_ptr_cptr: forall b ofs id attr,
-      val_casted (Vptr b ofs) (Tcomp_ptr id attr)
-  | val_casted_int_cptr: forall n id attr,
-      val_casted (Vint n) (Tcomp_ptr id attr)
-  | val_casted_struct: forall id fld attr b ofs,
-      val_casted (Vptr b ofs) (Tstruct id fld attr)
-  | val_casted_union: forall id fld attr b ofs,
-      val_casted (Vptr b ofs) (Tunion id fld 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.
 
@@ -254,8 +262,6 @@ Proof.
   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.
@@ -266,8 +272,6 @@ Proof.
   constructor; auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
   constructor; auto.
-  constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
-  constructor; auto.
 (* long *)
   destruct ty; try (destruct f); try discriminate.
   destruct v; inv H. constructor.
@@ -277,7 +281,6 @@ Proof.
   destruct v; 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 *)
@@ -287,12 +290,10 @@ Proof.
   discriminate.
 (* structs *)
   destruct ty; try discriminate; destruct v; try discriminate.
-  destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor.
+  destruct (ident_eq i0 i); inv H; constructor.
 (* unions *)
   destruct ty; try discriminate; destruct v; try discriminate.
-  destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor.
-(* comp_ptr *)
-  destruct ty; simpl in H; try discriminate; destruct v; inv H; constructor.
+  destruct (ident_eq i0 i); inv H; constructor.
 Qed.
 
 Lemma val_casted_load_result:
@@ -316,8 +317,6 @@ Proof.
   discriminate.
   discriminate.
   discriminate.
-  discriminate.
-  discriminate.
 Qed.
 
 Lemma cast_val_casted:
@@ -374,9 +373,9 @@ Proof.
   destruct v1; inv H0; auto.
   destruct v1; inv H0; auto.
   destruct v1; try discriminate.
-  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto.
+  destruct (ident_eq id1 id2); inv H0; auto.
   destruct v1; try discriminate.
-  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto.
+  destruct (ident_eq id1 id2); inv H0; auto.
   inv H0; auto.
 Qed.
 
@@ -388,7 +387,7 @@ Lemma match_envs_assign_lifted:
   e!id = Some(b, ty) ->
   val_casted v ty ->
   val_inject f v tv ->
-  assign_loc ty m b Int.zero v m' ->
+  assign_loc ge ty m b Int.zero v m' ->
   VSet.mem id cenv = true ->
   match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi.
 Proof.
@@ -582,8 +581,8 @@ Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat.
 (** Allocation and initialization of parameters *)
 
 Lemma alloc_variables_nextblock:
-  forall e m vars e' m',
-  alloc_variables e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m').
+  forall ge e m vars e' m',
+  alloc_variables ge e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m').
 Proof.
   induction 1.
   apply Ple_refl.
@@ -591,8 +590,8 @@ Proof.
 Qed.
 
 Lemma alloc_variables_range:
-  forall id b ty e m vars e' m',
-  alloc_variables e m vars e' m' ->
+  forall ge id b ty e m vars e' m',
+  alloc_variables ge e m vars e' m' ->
   e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Ple (Mem.nextblock m) b /\ Plt b (Mem.nextblock m').
 Proof.
   induction 1; intros.
@@ -600,15 +599,15 @@ Proof.
   exploit IHalloc_variables; eauto. rewrite PTree.gsspec. intros [A|A].
   destruct (peq id id0). inv A. 
   right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto.
-  generalize (alloc_variables_nextblock _ _ _ _ _ H0). intros A B C. 
+  generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C. 
   subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ. 
   auto.
   right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. 
 Qed.
 
 Lemma alloc_variables_injective:
-  forall id1 b1 ty1 id2 b2 ty2 e m vars e' m',
-  alloc_variables e m vars e' m' ->
+  forall ge id1 b1 ty1 id2 b2 ty2 e m vars e' m',
+  alloc_variables ge e m vars e' m' ->
   (e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2) ->
   (forall id b ty, e!id = Some(b, ty) -> Plt b (Mem.nextblock m)) ->
   (e'!id1 = Some(b1, ty1) -> e'!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2).
@@ -629,12 +628,12 @@ Qed.
 
 Lemma match_alloc_variables:
   forall cenv e m vars e' m',
-  alloc_variables e m vars e' m' ->
+  alloc_variables ge e m vars e' m' ->
   forall j tm te,
   list_norepet (var_names vars) ->
   Mem.inject j m tm ->
   exists j', exists te', exists tm',
-      alloc_variables te tm (remove_lifted cenv vars) te' tm'
+      alloc_variables tge te tm (remove_lifted cenv vars) te' tm'
   /\ Mem.inject j' m' tm'
   /\ inject_incr j j'
   /\ (forall b, Mem.valid_block m b -> j' b = j b)
@@ -698,7 +697,7 @@ Proof.
   exploit IHalloc_variables; eauto. instantiate (1 := PTree.set id (tb1, ty) te). 
   intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]].
   exists j'; exists te'; exists tm'.
-  split. simpl. econstructor; eauto.
+  split. simpl. econstructor; eauto. rewrite comp_env_preserved; auto. 
   split. auto.
   split. eapply inject_incr_trans; eauto. 
   split. intros. transitivity (j1 b). apply M. eapply Mem.valid_block_alloc; eauto. 
@@ -737,7 +736,7 @@ Qed.
 
 Lemma alloc_variables_load:
   forall e m vars e' m',
-  alloc_variables e m vars e' m' ->
+  alloc_variables ge e m vars e' m' ->
   forall chunk b ofs v,
   Mem.load chunk m b ofs = Some v ->
   Mem.load chunk m' b ofs = Some v.
@@ -749,10 +748,10 @@ Qed.
 
 Lemma sizeof_by_value:
   forall ty chunk,
-  access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty.
+  access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ge ty.
 Proof.
   unfold access_mode; intros.
-  assert (size_chunk chunk = sizeof ty).
+  assert (size_chunk chunk = sizeof ge ty).
   {
     destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto.
   }
@@ -765,7 +764,7 @@ Definition env_initial_value (e: env) (m: mem) :=
  
 Lemma alloc_variables_initial_value:
   forall e m vars e' m',
-  alloc_variables e m vars e' m' ->
+  alloc_variables ge e m vars e' m' ->
   env_initial_value e m ->
   env_initial_value e' m'.
 Proof.
@@ -900,14 +899,14 @@ Qed.
 
 Theorem match_envs_alloc_variables:
   forall cenv m vars e m' temps j tm,
-  alloc_variables empty_env m vars e m' ->
+  alloc_variables ge empty_env m vars e m' ->
   list_norepet (var_names vars) ->
   Mem.inject j m tm ->
   (forall id ty, In (id, ty) vars -> VSet.mem id cenv = true ->
                      exists chunk, access_mode ty = By_value chunk) ->
   (forall id, VSet.mem id cenv = true -> In id (var_names vars)) ->
   exists j', exists te, exists tm',
-     alloc_variables empty_env tm (remove_lifted cenv vars) te tm'
+     alloc_variables tge empty_env tm (remove_lifted cenv vars) te tm'
   /\ match_envs j' cenv e (create_undef_temps temps) m' (Mem.nextblock m) (Mem.nextblock m')
                         te (create_undef_temps (add_lifted cenv vars temps)) (Mem.nextblock tm) (Mem.nextblock tm')
   /\ Mem.inject j' m' tm'
@@ -996,12 +995,12 @@ Qed.
 
 Lemma assign_loc_inject:
   forall f ty m loc ofs v m' tm loc' ofs' v',
-  assign_loc ty m loc ofs v m' ->
+  assign_loc ge ty m loc ofs v m' ->
   val_inject f (Vptr loc ofs) (Vptr loc' ofs') ->
   val_inject f v v' ->
   Mem.inject f m tm ->
   exists tm',
-     assign_loc ty tm loc' ofs' v' tm'
+     assign_loc tge ty tm loc' ofs' v' tm'
   /\ Mem.inject f m' tm'
   /\ (forall b chunk v,
       f b = None -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v).
@@ -1018,10 +1017,11 @@ Proof.
   rename b' into bsrc. rename ofs'0 into osrc. 
   rename loc into bdst. rename ofs into odst.
   rename loc' into bdst'. rename b2 into bsrc'.
-  destruct (zeq (sizeof ty) 0).
+  rewrite <- comp_env_preserved in *.
+  destruct (zeq (sizeof tge ty) 0).
 + (* special case size = 0 *)
   assert (bytes = nil).
-  { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof ty)).
+  { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof tge ty)).
     omega. congruence. }
   subst.
   destruct (Mem.range_perm_storebytes tm bdst' (Int.unsigned (Int.add odst (Int.repr delta))) nil)
@@ -1038,12 +1038,12 @@ Proof.
   left. congruence.
 + (* general case size > 0 *)
   exploit Mem.loadbytes_length; eauto. intros LEN.
-  assert (SZPOS: sizeof ty > 0).
-  { generalize (sizeof_pos ty); omega. }
-  assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof ty) Cur Nonempty).
+  assert (SZPOS: sizeof tge ty > 0).
+  { generalize (sizeof_pos tge ty); omega. }
+  assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof tge ty) Cur Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
-  assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof ty) Cur Nonempty).
-    replace (sizeof ty) with (Z_of_nat (length bytes)).
+  assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof tge ty) Cur Nonempty).
+    replace (sizeof tge ty) with (Z_of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
     rewrite LEN. apply nat_of_Z_eq. omega.
   assert (PSRC: Mem.perm m bsrc (Int.unsigned osrc) Cur Nonempty).
@@ -1084,8 +1084,8 @@ Proof.
 Qed.
 
 Lemma assign_loc_nextblock:
-  forall ty m b ofs v m',
-  assign_loc ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m.
+  forall ge ty m b ofs v m',
+  assign_loc ge ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m.
 Proof.
   induction 1. 
   simpl in H0. eapply Mem.nextblock_store; eauto.
@@ -1094,7 +1094,7 @@ Qed.
 
 Theorem store_params_correct:
   forall j f k cenv le lo hi te tlo thi e m params args m',
-  bind_parameters e m params args m' ->
+  bind_parameters ge e m params args m' ->
   forall s tm tle1 tle2 targs,
   list_norepet (var_names params) ->
   list_forall2 val_casted args (map snd params) ->
@@ -1105,7 +1105,7 @@ Theorem store_params_correct:
   (forall id, In id (var_names params) -> le!id = None) ->
   exists tle, exists tm',
   star step2 tge (State f (store_params cenv params s) k te tle tm)
-             E0 (State f s k te tle tm')
+              E0 (State f s k te tle tm')
   /\ bind_parameter_temps params targs tle2 = Some tle
   /\ Mem.inject j m' tm'
   /\ match_envs j cenv e le m' lo hi te tle tlo thi
@@ -1157,12 +1157,12 @@ Proof.
   reflexivity. reflexivity. 
   eexact U. 
   traceEq.
-  rewrite (assign_loc_nextblock _ _ _ _ _ _ A) in Z. auto. 
+  rewrite (assign_loc_nextblock _ _ _ _ _ _ _ A) in Z. auto. 
 Qed.
 
 Lemma bind_parameters_nextblock:
-  forall e m params args m',
-  bind_parameters e m params args m' -> Mem.nextblock m' = Mem.nextblock m.
+  forall ge e m params args m',
+  bind_parameters ge e m params args m' -> Mem.nextblock m' = Mem.nextblock m.
 Proof.
   induction 1.
   auto.
@@ -1170,10 +1170,10 @@ Proof.
 Qed.
 
 Lemma bind_parameters_load:
-  forall e chunk b ofs,
+  forall ge e chunk b ofs,
   (forall id b' ty, e!id = Some(b', ty) -> b <> b') ->
   forall m params args m',
-  bind_parameters e m params args m' ->
+  bind_parameters ge e m params args m' ->
   Mem.load chunk m' b ofs = Mem.load chunk m b ofs.
 Proof.
   induction 2.
@@ -1188,16 +1188,16 @@ Qed.
 (** Freeing of local variables *)
 
 Lemma free_blocks_of_env_perm_1:
-  forall m e m' id b ty ofs k p,
-  Mem.free_list m (blocks_of_env e) = Some m' ->
+  forall ce m e m' id b ty ofs k p,
+  Mem.free_list m (blocks_of_env ce e) = Some m' ->
   e!id = Some(b, ty) ->
   Mem.perm m' b ofs k p ->
-  0 <= ofs < sizeof ty ->
+  0 <= ofs < sizeof ce ty ->
   False.
 Proof.
   intros. exploit Mem.perm_free_list; eauto. intros [A B].
-  apply B with 0 (sizeof ty); auto.
-  unfold blocks_of_env. change (b, 0, sizeof ty) with (block_of_binding (id, (b, ty))).
+  apply B with 0 (sizeof ce ty); auto.
+  unfold blocks_of_env. change (b, 0, sizeof ce ty) with (block_of_binding ce (id, (b, ty))).
   apply in_map. apply PTree.elements_correct. auto.
 Qed.
 
@@ -1216,13 +1216,13 @@ Proof.
 Qed.
 
 Lemma free_blocks_of_env_perm_2:
-  forall m e m' id b ty,
-  Mem.free_list m (blocks_of_env e) = Some m' ->
+  forall ce m e m' id b ty,
+  Mem.free_list m (blocks_of_env ce e) = Some m' ->
   e!id = Some(b, ty) ->
-  Mem.range_perm m b 0 (sizeof ty) Cur Freeable.
+  Mem.range_perm m b 0 (sizeof ce ty) Cur Freeable.
 Proof.
   intros. eapply free_list_perm'; eauto. 
-  unfold blocks_of_env. change (b, 0, sizeof ty) with (block_of_binding (id, (b, ty))).
+  unfold blocks_of_env. change (b, 0, sizeof ce ty) with (block_of_binding ce (id, (b, ty))).
   apply in_map. apply PTree.elements_correct. auto.
 Qed.
 
@@ -1252,15 +1252,15 @@ Proof.
 Qed.
 
 Lemma blocks_of_env_no_overlap:
-  forall j cenv e le m lo hi te tle tlo thi tm,
+  forall (ge: genv) j cenv e le m lo hi te tle tlo thi tm,
   match_envs j cenv e le m lo hi te tle tlo thi ->
   Mem.inject j m tm ->
   (forall id b ty, 
-   e!id = Some(b, ty) -> Mem.range_perm m b 0 (sizeof ty) Cur Freeable) ->
+   e!id = Some(b, ty) -> Mem.range_perm m b 0 (sizeof ge ty) Cur Freeable) ->
   forall l,
   list_norepet (List.map fst l) ->
   (forall id bty, In (id, bty) l -> te!id = Some bty) ->
-  freelist_no_overlap (List.map block_of_binding l).
+  freelist_no_overlap (List.map (block_of_binding ge) l).
 Proof.
   intros until tm; intros ME MINJ PERMS. induction l; simpl; intros.
 - auto.
@@ -1272,8 +1272,8 @@ Proof.
     assert (TE': te!id' = Some(b', ty')) by eauto. 
     exploit me_mapped. eauto. eexact TE. intros [b0 [INJ E]]. 
     exploit me_mapped. eauto. eexact TE'. intros [b0' [INJ' E']]. 
-    destruct (zle (sizeof ty) 0); auto. 
-    destruct (zle (sizeof ty') 0); auto. 
+    destruct (zle (sizeof ge0 ty) 0); auto. 
+    destruct (zle (sizeof ge0 ty') 0); auto. 
     assert (b0 <> b0').
     { eapply me_inj; eauto. red; intros; subst; elim H3.
       change id' with (fst (id', (b', ty'))). apply List.in_map; auto. }
@@ -1302,26 +1302,34 @@ Proof.
   eapply Mem.free_right_inject; eauto. 
 Qed.
 
+Lemma blocks_of_env_translated:
+  forall e, blocks_of_env tge e = blocks_of_env ge e.
+Proof.
+  intros. unfold blocks_of_env, block_of_binding. 
+  rewrite comp_env_preserved; auto. 
+Qed.
+
 Theorem match_envs_free_blocks:
   forall j cenv e le m lo hi te tle tlo thi m' tm,
   match_envs j cenv e le m lo hi te tle tlo thi ->
   Mem.inject j m tm ->
-  Mem.free_list m (blocks_of_env e) = Some m' ->
+  Mem.free_list m (blocks_of_env ge e) = Some m' ->
   exists tm',
-     Mem.free_list tm (blocks_of_env te) = Some tm'
+     Mem.free_list tm (blocks_of_env tge te) = Some tm'
   /\ Mem.inject j m' tm'.
 Proof.
   intros. 
-  assert (X: exists tm', Mem.free_list tm (blocks_of_env te) = Some tm').
+Local Opaque ge tge.
+  assert (X: exists tm', Mem.free_list tm (blocks_of_env tge te) = Some tm').
   {
-    apply can_free_list.
+    rewrite blocks_of_env_translated. apply can_free_list.
   - (* permissions *)
     intros. unfold blocks_of_env in H2.
     exploit list_in_map_inv; eauto. intros [[id [b' ty]] [EQ IN]].
-    simpl in EQ; inv EQ. 
+    unfold block_of_binding in EQ; inv EQ.
     exploit me_mapped; eauto. eapply PTree.elements_complete; eauto. 
     intros [b [A B]]. 
-    change 0 with (0 + 0). replace (sizeof ty) with (sizeof ty + 0) by omega.
+    change 0 with (0 + 0). replace (sizeof ge ty) with (sizeof ge ty + 0) by omega.
     eapply Mem.range_perm_inject; eauto. 
     eapply free_blocks_of_env_perm_2; eauto.
   - (* no overlap *)
@@ -1335,10 +1343,10 @@ Proof.
   eapply free_list_right_inject; eauto. 
   eapply Mem.free_list_left_inject; eauto. 
   intros. unfold blocks_of_env in H3. exploit list_in_map_inv; eauto. 
-  intros [[id [b' ty]] [EQ IN]]. simpl in EQ. inv EQ.
+  intros [[id [b' ty]] [EQ IN]]. unfold block_of_binding in EQ. inv EQ.
   exploit me_flat; eauto. apply PTree.elements_complete; eauto. 
   intros [P Q]. subst delta. eapply free_blocks_of_env_perm_1 with (m := m); eauto.
-  omega. 
+  rewrite <- comp_env_preserved. omega. 
 Qed.
 
 (** Matching global environments *)
@@ -1434,11 +1442,16 @@ Proof.
   exploit eval_simpl_expr. eexact H. eauto with compat. intros [tv1 [A B]].
   exploit eval_simpl_expr. eexact H0. eauto with compat. intros [tv2 [C D]].
   exploit sem_binary_operation_inject; eauto. intros [tv [E F]].
-  exists tv; split; auto. econstructor; eauto. repeat rewrite typeof_simpl_expr; auto.
+  exists tv; split; auto. econstructor; eauto.
+  repeat rewrite typeof_simpl_expr; rewrite comp_env_preserved; auto. 
 (* cast *)
   exploit eval_simpl_expr; eauto. intros [tv1 [A B]].
   exploit sem_cast_inject; eauto. intros [tv2 [C D]].
-  exists tv2; split; auto. econstructor. eauto. rewrite typeof_simpl_expr; auto. 
+  exists tv2; split; auto. econstructor. eauto. rewrite typeof_simpl_expr; auto.
+(* sizeof *)
+  econstructor; split. constructor. rewrite comp_env_preserved; auto.
+(* alignof *)
+  econstructor; split. constructor. rewrite comp_env_preserved; auto.
 (* rval *)
   assert (EITHER: (exists id, exists ty, a = Evar id ty /\ VSet.mem id cenv = true)
                \/ (match a with Evar id _ => VSet.mem id cenv = false | _ => True end)).
@@ -1481,12 +1494,14 @@ Proof.
   inversion B. subst. 
   econstructor; econstructor; split; eauto. econstructor; eauto. 
 (* field struct *)
+  rewrite <- comp_env_preserved in *.
   exploit eval_simpl_expr; eauto. intros [tv [A B]]. 
   inversion B. subst. 
   econstructor; econstructor; split. 
   eapply eval_Efield_struct; eauto. rewrite typeof_simpl_expr; eauto. 
   econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
 (* field union *)
+  rewrite <- comp_env_preserved in *.
   exploit eval_simpl_expr; eauto. intros [tv [A B]]. 
   inversion B. subst. 
   econstructor; econstructor; split. 
@@ -1583,7 +1598,7 @@ Qed.
 Lemma match_cont_assign_loc:
   forall f cenv k tk m bound tbound ty loc ofs v m',
   match_cont f cenv k tk m bound tbound ->
-  assign_loc ty m loc ofs v m' ->
+  assign_loc ge ty m loc ofs v m' ->
   Ple bound loc ->
   match_cont f cenv k tk m' bound tbound.
 Proof.
@@ -1687,8 +1702,8 @@ Lemma match_cont_free_env:
   match_cont f cenv k tk m lo tlo ->
   Ple hi (Mem.nextblock m) ->
   Ple thi (Mem.nextblock tm) ->
-  Mem.free_list m (blocks_of_env e) = Some m' ->
-  Mem.free_list tm (blocks_of_env te) = Some tm' ->
+  Mem.free_list m (blocks_of_env ge e) = Some m' ->
+  Mem.free_list tm (blocks_of_env tge te) = Some tm' ->
   match_cont f cenv k tk m' (Mem.nextblock m') (Mem.nextblock tm').
 Proof.
   intros. apply match_cont_incr_bounds with lo tlo.
@@ -2183,7 +2198,7 @@ Proof.
   red; intros; subst b'. xomega. 
   eapply alloc_variables_load; eauto.
   apply compat_cenv_for. 
-  rewrite (bind_parameters_nextblock _ _ _ _ _ H2). xomega.
+  rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). xomega.
   rewrite T; xomega.
 
 (* external function *)
@@ -2216,8 +2231,9 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [A B]]. 
   econstructor; split.
   econstructor.
-  eapply Genv.init_mem_transf_partial; eauto.
-  rewrite (transform_partial_program_main _ _ TRANSF).
+  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).
   instantiate (1 := b). rewrite <- H1. apply symbols_preserved.
   eauto.
   rewrite <- H3; apply type_of_fundef_preserved; auto.