Clean-up pass on C types:

- Ctypes: add useful functions on attributes; remove attrs in typeconv
    (because attributes are meaningless on r-values)
- C2C: fixed missing or redundant Evalof
- Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values);
    add sanity check between typeconv/classify_binarith and the C99 standard.
- cparser: fixed several cases where incorrect type annotations were put
    on expressions.


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

9 files changed, 381 insertions, 135 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f767372..8799bc0 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -200,9 +200,10 @@ a constant)"; Integers.Int.one in
 (** ** Translation of [va_arg] for variadic functions. *)
 
 let va_list_ptr e =
-  if CBuiltins.va_list_scalar
-  then Eaddrof(e, Tpointer(typeof e, noattr))
-  else e
+  if not CBuiltins.va_list_scalar then e else
+    match e with
+    | Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr))
+    | _             -> error "bad use of a va_list object"; e
 
 let make_builtin_va_arg env ty e =
   let (helper, ty_ret) =
@@ -215,15 +216,14 @@ let make_builtin_va_arg env ty e =
         ("__compcert_va_float64", Tfloat(F64, noattr))
     | _ ->
         unsupported "va_arg at this type";
-        ("", Tvoid)
-  in
-    Ecast 
-      (Ecall(Evar (intern_string helper, 
-                   Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, 
-                             cc_default)),
-             Econs(va_list_ptr e, Enil),
-             ty_ret),
-       ty)
+        ("", Tvoid) in
+  let ty_fun =
+    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in
+  Ecast 
+    (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
+           Econs(va_list_ptr e, Enil),
+           ty_ret),
+     ty)
 
 (** ** Translation functions *)
 
@@ -338,7 +338,7 @@ let convertTyp env t =
     | C.TStruct(id, a) ->
         let a' = convertAttr a in
         begin try
-          mergeTypAttr (Hashtbl.find compositeCache id) a'
+          merge_attributes (Hashtbl.find compositeCache id) a'
         with Not_found ->
           let flds =
             try
@@ -350,7 +350,7 @@ let convertTyp env t =
     | C.TUnion(id, a) ->
         let a' = convertAttr a in
         begin try
-          mergeTypAttr (Hashtbl.find compositeCache id) a'
+          merge_attributes (Hashtbl.find compositeCache id) a'
         with Not_found ->
           let flds =
             try
@@ -379,12 +379,6 @@ let convertTyp env t =
 
   in convertTyp [] t
 
-(*
-let rec convertTypList env = function
-  | [] -> Tnil
-  | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl)
-*)
-
 let rec convertTypArgs env tl el =
   match tl, el with
   | _, [] -> Tnil
@@ -1062,10 +1056,11 @@ let convertProgram p =
   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_main = intern_string "main" } in
     if !numErrors > 0
     then None
-    else Some { AST.prog_defs = gl2;
-                AST.prog_main = intern_string "main" }
+    else Some p'
   with Env.Error msg ->
     error (Env.error_message msg); None
 
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index f2550ef..83fe772 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -115,7 +115,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   end.
 
 (** Semantics of casts.  [sem_cast v1 t1 t2 = Some v2] if value [v1],
-  viewed with static type [t1], can be cast to type [t2],
+  viewed with static type [t1], can be converted  to type [t2],
   resulting in value [v2].  *)
 
 Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
@@ -266,7 +266,8 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
 
 (** The following describes types that can be interpreted as a boolean:
   integers, floats, pointers.  It is used for the semantics of 
-  the [!] and [?] operators, as well as the [if], [while], [for] statements. *)
+  the [!] and [?] operators, as well as the [if], [while], 
+  and [for] statements. *)
 
 Inductive classify_bool_cases : Type :=
   | bool_case_i                           (**r integer *)
@@ -315,34 +316,6 @@ Definition bool_val (v: val) (t: type) : option bool :=
   | bool_default => None
   end.
 
-(** Common-sense relation between Boolean value and casting to [_Bool] type. *)
-
-Lemma cast_bool_bool_val:
-  forall v t,
-  sem_cast v t (Tint IBool Signed noattr) =
-  match bool_val v t with None => None | Some b => Some(Val.of_bool b) end.
-Proof.
-  intros.
-  assert (A: classify_bool t =
-    match t with
-    | Tint _ _ _ => bool_case_i
-    | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
-    | Tfloat _ _ => bool_case_f
-    | Tlong _ _ => bool_case_l
-    | _ => bool_default
-    end).
-  {
-    unfold classify_bool; destruct t; simpl; auto. destruct i; auto.
-  }
-  unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto.
-  destruct (Int.eq i0 Int.zero); auto.
-  destruct (Int64.eq i Int64.zero); auto.
-  destruct (Float.cmp Ceq f0 Float.zero); auto.
-  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.
 
 (** ** Unary operators *)
 
@@ -374,17 +347,6 @@ Definition sem_notbool (v: val) (ty: type) : option val :=
   | bool_default => None
   end.
 
-(** Common-sense relation between Boolean value and Boolean negation. *)
-
-Lemma notbool_bool_val:
-  forall v t,
-  sem_notbool v t =
-  match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end.
-Proof.
-  intros. unfold sem_notbool, bool_val. 
-  destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto.
-Qed.
-
 (** *** Opposite and absolute value *)
 
 Inductive classify_neg_cases : Type :=
@@ -503,6 +465,16 @@ Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
   | _, _ => bin_default
   end.
 
+(** The static type of the result. *)
+
+Definition binarith_result_type (c: binarith_cases) : option type :=
+  match c with
+  | bin_case_i sg => Some(Tint I32 sg noattr)
+  | bin_case_l sg => Some(Tlong sg noattr)
+  | bin_case_f sz => Some(Tfloat sz noattr)
+  | bin_default   => None
+  end.
+
 (** The type at which the computation is done.  Both arguments are
   converted to this type before the actual computation.  *)
 
@@ -549,43 +521,43 @@ Definition sem_binarith
 (** *** Addition *)
 
 Inductive classify_add_cases : Type :=
-  | add_case_pi(ty: type)(a: attr)     (**r pointer, int *)
-  | add_case_ip(ty: type)(a: attr)     (**r int, pointer *)
-  | add_case_pl(ty: type)(a: attr)     (**r pointer, long *)
-  | add_case_lp(ty: type)(a: attr)     (**r long, pointer *)
+  | add_case_pi(ty: type)     (**r pointer, int *)
+  | add_case_ip(ty: type)     (**r int, pointer *)
+  | add_case_pl(ty: type)     (**r pointer, long *)
+  | add_case_lp(ty: type)     (**r long, pointer *)
   | add_default.                       (**r numerical type, numerical type *)
 
 Definition classify_add (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with
-  | Tpointer ty a, Tint _ _ _ => add_case_pi ty a
-  | Tint _ _ _, Tpointer ty a => add_case_ip ty a
-  | Tpointer ty a, Tlong _ _ => add_case_pl ty a
-  | Tlong _ _, Tpointer ty a => add_case_lp ty a
+  | Tpointer ty _, Tint _ _ _ => add_case_pi ty
+  | Tint _ _ _, Tpointer ty _ => add_case_ip ty
+  | Tpointer ty _, Tlong _ _ => add_case_pl ty
+  | Tlong _ _, Tpointer ty _ => add_case_lp ty
   | _, _ => add_default
   end.
 
 Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_add t1 t2 with 
-  | add_case_pi ty _ =>                 (**r pointer plus integer *)
+  | 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)))
       | _,  _ => None
       end   
-  | add_case_ip ty _ =>                 (**r integer plus pointer *)
+  | 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)))
       | _,  _ => None
       end   
-  | add_case_pl ty _ =>                 (**r pointer plus long *)
+  | 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)))
       | _,  _ => None
       end   
-  | add_case_lp ty _ =>                 (**r long plus pointer *)
+  | 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
@@ -603,28 +575,28 @@ Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
 (** *** Subtraction *)
 
 Inductive classify_sub_cases : Type :=
-  | sub_case_pi(ty: type)(a: attr)      (**r pointer, int *)
+  | sub_case_pi(ty: type)               (**r pointer, int *)
   | sub_case_pp(ty: type)               (**r pointer, pointer *)
-  | sub_case_pl(ty: type)(a: attr)      (**r pointer, long *)
+  | sub_case_pl(ty: type)               (**r pointer, long *)
   | sub_default.                        (**r numerical type, numerical type *)
 
 Definition classify_sub (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with
-  | Tpointer ty a, Tint _ _ _ => sub_case_pi ty a
+  | Tpointer ty _, Tint _ _ _ => sub_case_pi ty
   | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty
-  | Tpointer ty a, Tlong _ _ => sub_case_pl ty a
+  | Tpointer ty _, Tlong _ _ => sub_case_pl ty
   | _, _ => sub_default
   end.
 
 Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_sub t1 t2 with
-  | sub_case_pi ty attr =>            (**r pointer minus integer *)
+  | 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)))
       | _,  _ => None
       end
-  | sub_case_pl ty attr =>            (**r pointer minus long *)
+  | 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
@@ -1177,5 +1149,234 @@ Proof.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
+(** * Some properties of operator semantics *)
+
+(** This section collects some common-sense properties about the type
+  classification and semantic functions above.  These properties are
+  not used in the CompCert semantics preservation proofs, but increase
+  confidence in the specification and its relation with the ISO C99 standard. *)
+
+(** Relation between Boolean value and casting to [_Bool] type. *)
+
+Lemma cast_bool_bool_val:
+  forall v t,
+  sem_cast v t (Tint IBool Signed noattr) =
+  match bool_val v t with None => None | Some b => Some(Val.of_bool b) end.
+Proof.
+  intros.
+  assert (A: classify_bool t =
+    match t with
+    | Tint _ _ _ => bool_case_i
+    | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
+    | Tfloat _ _ => bool_case_f
+    | Tlong _ _ => bool_case_l
+    | _ => bool_default
+    end).
+  {
+    unfold classify_bool; destruct t; simpl; auto. destruct i; auto.
+  }
+  unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto.
+  destruct (Int.eq i0 Int.zero); auto.
+  destruct (Int64.eq i Int64.zero); auto.
+  destruct (Float.cmp Ceq f0 Float.zero); auto.
+  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. *)
 
+Lemma notbool_bool_val:
+  forall v t,
+  sem_notbool v t =
+  match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end.
+Proof.
+  intros. unfold sem_notbool, bool_val. 
+  destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto.
+Qed.
 
+(** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *)
+
+Module ArithConv.
+
+(** This is the ISO C algebra of arithmetic types, without qualifiers.
+    [S] stands for "signed" and [U] for "unsigned".  *)
+
+Inductive int_type : Type :=
+  | _Bool
+  | Char | SChar | UChar
+  | Short | UShort
+  | Int | UInt
+  | Long | ULong
+  | Longlong | ULonglong.
+
+Inductive arith_type : Type :=
+  | I (it: int_type)
+  | Float
+  | Double
+  | Longdouble.
+
+Definition eq_int_type: forall (x y: int_type), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+Definition is_unsigned (t: int_type) : bool :=
+  match t with
+  | _Bool => true
+  | Char => false    (**r as in most of CompCert's target ABIs *)
+  | SChar => false
+  | UChar => true
+  | Short => false
+  | UShort => true
+  | Int => false
+  | UInt => true
+  | Long => false
+  | ULong => true
+  | Longlong => false
+  | ULonglong => true
+  end.
+
+Definition unsigned_type (t: int_type) : int_type :=
+  match t with
+  | Char => UChar
+  | SChar => UChar
+  | Short => UShort
+  | Int => UInt
+  | Long => ULong
+  | Longlong => ULonglong
+  | _ => t
+  end.
+
+Definition int_sizeof (t: int_type) : Z :=
+  match t with
+  | _Bool | Char | SChar | UChar => 1
+  | Short | UShort => 2
+  | Int | UInt | Long | ULong => 4
+  | Longlong | ULonglong => 8
+  end.
+
+(** 6.3.1.1 para 1: integer conversion rank *)
+
+Definition rank (t: int_type) : Z :=
+  match t with
+  | _Bool => 1
+  | Char | SChar | UChar => 2
+  | Short | UShort => 3
+  | Int | UInt => 4
+  | Long | ULong => 5
+  | Longlong | ULonglong => 6
+  end.
+
+(** 6.3.1.1 para 2: integer promotions, a.k.a. usual unary conversions *)
+
+Definition integer_promotion (t: int_type) : int_type :=
+  if zlt (rank t) (rank Int) then Int else t.
+
+(** 6.3.1.8: Usual arithmetic conversions, a.k.a. binary conversions.
+  This function returns the type to which the two operands must be
+  converted. *)
+
+Definition usual_arithmetic_conversion (t1 t2: arith_type) : arith_type :=
+  match t1, t2 with
+  (* First, if the corresponding real type of either operand is long
+     double, the other operand is converted, without change of type domain,
+     to a type whose corresponding real type is long double. *)
+  | Longdouble, _ | _, Longdouble => Longdouble
+  (* Otherwise, if the corresponding real type of either operand is
+     double, the other operand is converted, without change of type domain,
+     to a type whose corresponding real type is double. *)
+  | Double, _ | _, Double => Double
+  (* Otherwise, if the corresponding real type of either operand is
+     float, the other operand is converted, without change of type domain,
+     to a type whose corresponding real type is float. *)
+  | Float, _ | _, Float => Float
+  (* Otherwise, the integer promotions are performed on both operands. *)
+  | I i1, I i2 =>
+    let j1 := integer_promotion i1 in
+    let j2 := integer_promotion i2 in
+    (* Then the following rules are applied to the promoted operands:
+       If both operands have the same type, then no further conversion
+       is needed. *)
+    if eq_int_type j1 j2 then I j1 else
+    match is_unsigned j1, is_unsigned j2 with
+    (* Otherwise, if both operands have signed integer types or both
+       have unsigned integer types, the operand with the type of lesser
+       integer conversion rank is converted to the type of the operand with
+       greater rank. *)
+    | true, true | false, false =>
+        if zlt (rank j1) (rank j2) then I j2 else I j1
+    | true, false =>
+    (* Otherwise, if the operand that has unsigned integer type has
+       rank greater or equal to the rank of the type of the other operand,
+       then the operand with signed integer type is converted to the type of
+       the operand with unsigned integer type. *)
+        if zle (rank j2) (rank j1) then I j1 else
+    (* Otherwise, if the type of the operand with signed integer type
+       can represent all of the values of the type of the operand with
+       unsigned integer type, then the operand with unsigned integer type is
+       converted to the type of the operand with signed integer type. *)
+        if zlt (int_sizeof j1) (int_sizeof j2) then I j2 else
+    (* Otherwise, both operands are converted to the unsigned integer type
+       corresponding to the type of the operand with signed integer type. *)
+        I (unsigned_type j2)
+    | false, true =>
+    (* Same logic as above, swapping the roles of j1 and j2 *)
+        if zle (rank j1) (rank j2) then I j2 else
+        if zlt (int_sizeof j2) (int_sizeof j1) then I j1 else
+        I (unsigned_type j1)
+    end
+  end.
+
+(** Mapping ISO arithmetic types to CompCert types *)
+
+Definition proj_type (t: arith_type) : type :=
+  match t with
+  | I _Bool => Tint IBool Unsigned noattr
+  | I Char => Tint I8 Unsigned noattr
+  | I SChar => Tint I8 Signed noattr
+  | I UChar => Tint I8 Unsigned noattr
+  | I Short => Tint I16 Signed noattr
+  | I UShort => Tint I16 Unsigned noattr
+  | I Int => Tint I32 Signed noattr
+  | I UInt => Tint I32 Unsigned noattr
+  | I Long => Tint I32 Signed noattr
+  | I ULong => Tint I32 Unsigned noattr
+  | I Longlong => Tlong Signed noattr
+  | I ULonglong => Tlong Unsigned noattr
+  | Float => Tfloat F32 noattr
+  | Double => Tfloat F64 noattr
+  | Longdouble => Tfloat F64 noattr
+  end.
+
+(** Relation between [typeconv] and integer promotion. *)
+
+Lemma typeconv_integer_promotion:
+  forall i, typeconv (proj_type (I i)) = proj_type (I (integer_promotion i)).
+Proof.
+  destruct i; reflexivity.
+Qed.
+
+(** Relation between [classify_binarith] and arithmetic conversion. *)
+
+Lemma classify_binarith_arithmetic_conversion:
+  forall t1 t2,
+  binarith_result_type (classify_binarith (proj_type t1) (proj_type t2)) =
+  Some (proj_type (usual_arithmetic_conversion t1 t2)).
+Proof.
+  destruct t1; destruct t2; try reflexivity.
+- destruct it; destruct it0; reflexivity.
+- destruct it; reflexivity.
+- destruct it; reflexivity.
+- destruct it; reflexivity.
+- destruct it; reflexivity.
+- destruct it; reflexivity.
+- destruct it; reflexivity.
+Qed.
+
+End ArithConv.
+
+
+
+
+
+ 
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index c97e881..685fa71 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -203,16 +203,16 @@ Definition make_binarith (iop iopu fop lop lopu: binary_operation)
 
 Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
-  | add_case_pi ty _ =>
+  | add_case_pi ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Oadd e1 (Ebinop Omul n e2))
-  | add_case_ip ty _ =>
+  | add_case_ip ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Oadd e2 (Ebinop Omul n e1))
-  | add_case_pl ty _ =>
+  | add_case_pl ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
-  | add_case_lp ty _ =>
+  | add_case_lp ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1)))
   | add_default =>
@@ -221,13 +221,13 @@ Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 
 Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_sub ty1 ty2 with
-  | sub_case_pi ty _ =>
+  | sub_case_pi ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Odivu (Ebinop Osub e1 e2) n)
-  | sub_case_pl ty _ =>
+  | sub_case_pl ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | sub_default =>
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 5cd032d..41d0dcb 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -145,18 +145,55 @@ Definition attr_of_type (ty: type) :=
   | Tcomp_ptr id a => a
   end.
 
+(** Change the top-level attributes of a type *)
+
+Definition change_attributes (f: attr -> attr) (ty: type) : type :=
+  match ty with
+  | Tvoid => ty
+  | Tint sz si a => Tint sz si (f a)
+  | Tlong si a => Tlong si (f a)
+  | Tfloat sz a => Tfloat sz (f a)
+  | 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)
+  end.
+
+(** Erase the top-level attributes of a type *)
+
+Definition remove_attributes (ty: type) : type :=
+  change_attributes (fun _ => noattr) ty.
+
+(** Add extra attributes to the top-level attributes of a type *)
+
+Definition attr_union (a1 a2: attr) : attr :=
+  {| attr_volatile := a1.(attr_volatile) || a2.(attr_volatile);
+     attr_alignas :=
+       match a1.(attr_alignas), a2.(attr_alignas) with
+       | None, al => al
+       | al, None => al
+       | Some n1, Some n2 => Some (N.max n1 n2)
+       end 
+  |}.
+
+Definition merge_attributes (ty: type) (a: attr) : type :=
+  change_attributes (attr_union a) ty.
+
 Definition type_int32s := Tint I32 Signed noattr.
 Definition type_bool := Tint IBool Signed noattr.
 
 (** The usual unary conversion.  Promotes small integer types to [signed int32]
-  and degrades array types and function types to pointer types. *)
+  and degrades array types and function types to pointer types. 
+  Attributes are erased. *)
 
 Definition typeconv (ty: type) : type :=
   match ty with
-  | Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a
-  | Tarray t sz a       => Tpointer t a
+  | Tint (I8 | I16 | IBool) _ _ => Tint I32 Signed noattr
+  | Tarray t sz a       => Tpointer t noattr
   | Tfunction _ _ _     => Tpointer ty noattr
-  | _                   => ty
+  | _                   => remove_attributes ty
   end.
 
 (** * Operations over types *)
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 71404b2..14c9314 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -161,6 +161,14 @@ let insertion_mask bf =
   (* Give the mask an hexadecimal string representation, nicer to read *)
   {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}
 
+let eshift env op a b =
+  let ty = unary_conversion env a.etyp in
+  { edesc = EBinop(op, a, b, ty); etyp = ty }
+
+let ebinint env op a b =
+  let ty = binary_conversion env a.etyp b.etyp in
+  { edesc = EBinop(op, a, b, ty); etyp = ty }
+
 (* Extract the value of a bitfield *)
 
 (* Reference C code:
@@ -178,15 +186,11 @@ signed int bitfield_signed_extract(unsigned int x, int ofs, int sz)
 
 *)
 
-let bitfield_extract bf carrier =
-  let e1 =
-    {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
-     etyp = carrier.etyp} in
+let bitfield_extract env bf carrier =
+  let e1 = eshift env Oshl carrier (left_shift_count bf) in
   let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
   let e2 = ecast ty e1 in
-  let e3 =
-    {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
-     etyp = ty} in
+  let e3 = eshift env Oshr e2 (right_shift_count bf) in
   if bf.bf_signed_res = bf.bf_signed
   then e3
   else ecast (TInt((if bf.bf_signed_res then IInt else IUInt), [])) e3
@@ -203,23 +207,16 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
 
 *)
 
-let bitfield_assign bf carrier newval =
+let bitfield_assign env bf carrier newval =
   let msk = insertion_mask bf in
   let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
   let newval_casted =
     ecast (TInt(IUInt,[])) newval in
   let newval_shifted =
-    {edesc = EBinop(Oshl, newval_casted, intconst (Int64.of_int bf.bf_pos) IUInt,
-                    TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])} in
-  let newval_masked =
-    {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])}
-  and oldval_masked =
-    {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])} in
-  {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
-   etyp =  TInt(IUInt,[])}
+    eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in
+  let newval_masked = ebinint env Oand newval_shifted msk
+  and oldval_masked = ebinint env Oand carrier notmsk in
+  ebinint env Oor oldval_masked newval_masked
 
 (* Check whether a field access (e.f or e->f) is a bitfield access.
    If so, return carrier expression (e and *e, respectively)
@@ -322,7 +319,7 @@ let transf_expr env ctx e =
         {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp}
 
   and transf_read e bf =
-    bitfield_extract bf
+    bitfield_extract env bf
       {edesc = EUnop(Odot bf.bf_carrier, texp Val e); etyp = bf.bf_carrier_typ}
 
   and transf_assign ctx e1 bf e2 =
@@ -330,19 +327,19 @@ let transf_expr env ctx e =
       let carrier =
         {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
       let asg =
-        eassign carrier (bitfield_assign bf carrier (texp Val e2)) in
-      if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg)
+        eassign carrier (bitfield_assign env bf carrier (texp Val e2)) in
+      if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg)
 
   and transf_assignop ctx op e1 bf e2 tyres =
     bind_lvalue env (texp Val e1) (fun base ->
       let carrier =
         {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
       let rhs =
-        {edesc = EBinop(op, bitfield_extract bf carrier, texp Val e2, tyres);
+        {edesc = EBinop(op, bitfield_extract env bf carrier, texp Val e2, tyres);
          etyp = tyres} in
       let asg =
-        eassign carrier (bitfield_assign bf carrier rhs) in
-      if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg)
+        eassign carrier (bitfield_assign env bf carrier rhs) in
+      if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg)
 
   and transf_pre ctx op e1 bf tyfield =
     transf_assignop ctx op e1 bf (intconst 1L IInt)
@@ -357,11 +354,11 @@ let transf_expr env ctx e =
           {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
         let temp = mk_temp env tyfield in
         let tyres = unary_conversion env tyfield in
-        let settemp = eassign temp (bitfield_extract bf carrier) in
+        let settemp = eassign temp (bitfield_extract env bf carrier) in
         let rhs =
           {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in
         let asg =
-          eassign carrier (bitfield_assign bf carrier rhs) in
+          eassign carrier (bitfield_assign env bf carrier rhs) in
         ecomma (ecomma settemp asg) temp)
     end
 
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 22ef187..1169346 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -92,6 +92,13 @@ let attr_array_applicable = function
   | AConst | AVolatile | ARestrict | AAlignas _ -> false
   | Attr _ -> true
 
+(* Is an attribute of a composite type applicable to members of this type
+  when they are accessed? *)
+
+let attr_inherited_by_members = function
+  | AConst | AVolatile | ARestrict -> true
+  | AAlignas _ | Attr _ -> false
+
 (* Adding top-level attributes to a type.  Doesn't need to unroll defns. *)
 (* For array types, standard attrs are pushed to the element type. *)
 
@@ -574,17 +581,20 @@ let unary_conversion env t =
   | TInt(kind, attr) ->
       begin match kind with
       | IBool | IChar | ISChar | IUChar | IShort | IUShort ->
-          TInt(IInt, attr)
+          TInt(IInt, [])
       | IInt | IUInt | ILong | IULong | ILongLong | IULongLong ->
-          TInt(kind, attr)
+          TInt(kind, [])
       end
   (* Enums are like signed ints *)
-  | TEnum(id, attr) -> TInt(enum_ikind, attr)
+  | TEnum(id, attr) -> TInt(enum_ikind, [])
   (* Arrays and functions decay automatically to pointers *)
   | TArray(ty, _, _) -> TPtr(ty, [])
   | TFun _ as ty -> TPtr(ty, [])
-  (* Other types are not changed *)
-  | t -> t
+  (* Float types and pointer types lose their attributes *)
+  | TFloat(kind, attr) -> TFloat(kind, [])
+  | TPtr(ty, attr) -> TPtr(ty, [])
+  (* Other types should not occur, but in doubt... *)
+  | _ -> t
 
 (* The usual binary conversions  (H&S 6.3.4).
    Applies only to arithmetic types.
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 9f59a76..0de0c82 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -54,6 +54,8 @@ val change_attributes_type : Env.t -> (attributes -> attributes) -> typ -> typ
   (* Apply the given function to the top-level attributes of the given type *)
 val attr_is_type_related: attribute -> bool
   (* Is an attribute type-related (true) or variable-related (false)? *)
+val attr_inherited_by_members: attribute -> bool
+  (* Is an attribute of a composite inherited by members of the composite? *)
 
 (* Type compatibility *)
 val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 0d2cb89..ecc97a7 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -805,7 +805,8 @@ let elab_expr loc env a =
             error "left-hand side of '.' is not a struct or union" in
       (* A field of a const/volatile struct or union is itself const/volatile *)
       { edesc = EUnop(Odot fieldname, b1);
-        etyp = add_attributes_type attrs (type_of_member env fld) }
+        etyp = add_attributes_type (List.filter attr_inherited_by_members attrs)
+                                   (type_of_member env fld) }
 
   | MEMBEROFPTR(a1, fieldname) ->
       let b1 = elab a1 in
@@ -823,7 +824,8 @@ let elab_expr loc env a =
         | _ ->
             error "left-hand side of '->' is not a pointer " in
       { edesc = EUnop(Oarrow fieldname, b1);
-        etyp = add_attributes_type attrs (type_of_member env fld) }
+        etyp = add_attributes_type (List.filter attr_inherited_by_members attrs)
+                                   (type_of_member env fld) }
 
 (* Hack to treat vararg.h functions the GCC way.  Helps with testing.
     va_start(ap,n)
@@ -996,14 +998,14 @@ let elab_expr loc env a =
         if is_arith_type env b1.etyp && is_arith_type env b2.etyp then
           binary_conversion env b1.etyp b2.etyp
         else begin
-          let (ty, attr) =
+          let ty =
             match unroll env b1.etyp, unroll env b2.etyp with
-            | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> (ty, a)
-            | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a)
+            | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty
+            | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty
             | _, _ -> error "type error in binary '+'" in
           if not (pointer_arithmetic_ok env ty) then
             err "illegal pointer arithmetic in binary '+'";
-          TPtr(ty, attr)
+          TPtr(ty, [])
         end in
       { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres }
 
@@ -1019,11 +1021,11 @@ let elab_expr loc env a =
           | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
-              (TPtr(ty, a), TPtr(ty, a))
+              (TPtr(ty, []), TPtr(ty, []))
           | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
-              (TPtr(ty, a), TPtr(ty, a))
+              (TPtr(ty, []), TPtr(ty, []))
           | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
             (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
               if not (compatible_types ~noattrs:true env ty1 ty2) then
@@ -1084,7 +1086,7 @@ let elab_expr loc env a =
       | TPtr(ty1, a1), TPtr(ty2, a2) ->
           let tyres =
             if is_void_type env ty1 || is_void_type env ty2 then
-              TPtr(TVoid [], add_attributes a1 a2)
+              TPtr(TVoid (add_attributes a1 a2), [])
             else
               match combine_types ~noattrs:true env
                                   (TPtr(ty1, a1)) (TPtr(ty2, a2)) with
@@ -1095,9 +1097,9 @@ let elab_expr loc env a =
             in
           { edesc = EConditional(b1, b2, b3); etyp = tyres }
       | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
-          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, a1) }
+          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) }
       | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
-          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) }
+          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) }
       | ty1, ty2 ->
           match combine_types ~noattrs:true env ty1 ty2 with
           | None ->
@@ -1312,7 +1314,7 @@ let init_char_array_string opt_size s =
     if i < 0L then init else begin
       let c =
         if i < len then Int64.of_int (Char.code s.[Int64.to_int i]) else 0L in
-      add_chars (Int64.pred i) (Init_single (intconst c IChar) :: init)
+      add_chars (Int64.pred i) (Init_single (intconst c IInt) :: init)
     end in
   Init_array (add_chars (Int64.pred size) [])
 
diff --git a/extraction/extraction.v b/extraction/extraction.v
index b9f684e..344a00f 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -21,6 +21,7 @@ Require Inlining.
 Require ValueDomain.
 Require Tailcall.
 Require Allocation.
+Require Ctypes.
 Require Compiler.
 
 (* Standard lib *)
@@ -125,6 +126,7 @@ Cd "extraction".
 Separate Extraction
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
+   Ctypes.merge_attributes Ctypes.remove_attributes
    Initializers.transl_init Initializers.constval
    Csyntax.Eindex Csyntax.Epreincr
    Conventions1.dummy_int_reg Conventions1.dummy_float_reg