Deactivate warning 27 and added back removed code.

The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349

14 files changed, 139 insertions, 139 deletions

diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 6e325ff2..d55a6d36 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -513,7 +513,7 @@ let transf_decl env (sto, id, ty, init_opt) =
 
 let transf_stmt env s =
   Transform.stmt
-     ~expr:(fun _ env ctx e -> transf_exp env ctx e)
+     ~expr:(fun loc env ctx e -> transf_exp env ctx e)
      ~decl:transf_decl
      env s
 
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 7a706da2..c3d7eeeb 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -80,10 +80,10 @@ let boolean_value v =
 
 let constant = function
   | CInt(v, ik, _) -> I (normalize_int v ik)
-  | CFloat _ -> raise Notconst
+  | CFloat(v, fk) -> raise Notconst
   | CStr s -> S s
   | CWStr s -> WS s
-  | CEnum(_, v) -> I v
+  | CEnum(id, v) -> I v
 
 let is_signed env ty =
   match unroll env ty with
@@ -101,11 +101,11 @@ let cast env ty_to v =
       if sizeof_ikind ik >= !config.sizeof_ptr
       then v
       else raise Notconst
-  | TPtr _, I n ->
+  | TPtr(ty, _), I n ->
       I (normalize_int n (ptr_t_ikind ()))
-  | TPtr _, (S _ | WS _) ->
+  | TPtr(ty, _), (S _ | WS _) ->
       v
-  | TEnum _, I n ->
+  | TEnum(_, _), I n ->
       I (normalize_int n enum_ikind)
   | _, _ ->
       raise Notconst
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 845232aa..fe674d9b 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -51,18 +51,18 @@ let rec add_typ = function
   | _ -> ()
 
 and add_vars vl =
-  List.iter (fun (_, ty) -> add_typ ty) vl
+  List.iter (fun (id, ty) -> add_typ ty) vl
 
 let rec add_exp e =
   add_typ e.etyp; (* perhaps not necessary but play it safe *)
   match e.edesc with
-  | EConst (CEnum(id, _)) -> addref id
+  | EConst (CEnum(id, v)) -> addref id
   | EConst _ -> ()
   | ESizeof ty -> add_typ ty
   | EAlignof ty -> add_typ ty
   | EVar id -> addref id
-  | EUnop(_, e1) -> add_exp e1
-  | EBinop(_, e1, e2, _) -> add_exp e1; add_exp e2
+  | EUnop(op, e1) -> add_exp e1
+  | EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
   | EConditional(e1, e2, e3) -> add_exp e1; add_exp e2; add_exp e3
   | ECast(ty, e1) -> add_typ ty; add_exp e1
   | ECompound(ty, ie) -> add_typ ty; add_init ie
@@ -74,11 +74,11 @@ and add_init = function
   | Init_struct(id, il) -> addref id; List.iter (fun (_, i) -> add_init i) il
   | Init_union(id, _, i) -> addref id; add_init i
 
-let add_decl (_, _, ty, init) =
+let add_decl (sto, id, ty, init) =
   add_typ ty;
   match init with None -> () | Some i -> add_init i
 
-let add_asm_operand (_, _, e) = add_exp e
+let add_asm_operand (lbl, cstr, e) = add_exp e
 
 let rec add_stmt s =
   match s.sdesc with
@@ -95,12 +95,12 @@ let rec add_stmt s =
   | Slabeled(lbl, s) ->
       begin match lbl with Scase e -> add_exp e | _ -> () end;
       add_stmt s
-  | Sgoto _ -> ()
+  | Sgoto lbl -> ()
   | Sreturn None -> ()
   | Sreturn(Some e) -> add_exp e
   | Sblock sl -> List.iter add_stmt sl
   | Sdecl d -> add_decl d
-  | Sasm(_, _, outputs, inputs, _) ->
+  | Sasm(attr, template, outputs, inputs, flags) ->
       List.iter add_asm_operand outputs;
       List.iter add_asm_operand inputs
 
@@ -114,13 +114,13 @@ let add_field f = add_typ f.fld_typ
 
 let add_enum e =
   List.iter
-    (fun (_, _, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
+    (fun (id, v, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
     e
 
 (* Saturate the set of referenced identifiers, starting with externally
    visible global declarations *)
 
-let visible_decl (sto, _, ty, _) =
+let visible_decl (sto, id, ty, init) =
   sto = Storage_default &&
   match ty with TFun _ -> false | _ -> true
 
@@ -150,7 +150,7 @@ let rec add_needed_globdecls accu = function
   | [] -> accu
   | g :: rem ->
       match g.gdesc with
-      | Gdecl((_, id, _, _) as decl) ->
+      | Gdecl((sto, id, ty, init) as decl) ->
           if needed id
           then (add_decl decl; add_needed_globdecls accu rem)
           else add_needed_globdecls (g :: accu) rem
@@ -194,14 +194,14 @@ let rec simpl_globdecls accu = function
   | g :: rem ->
       let need =
         match g.gdesc with
-        | Gdecl((_, id, _, _) as decl) -> visible_decl decl || needed id
+        | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
         | Gfundef f -> visible_fundef f || needed f.fd_name
         | Gcompositedecl(_, id, _) -> needed id
-        | Gcompositedef(_, id, _, _) -> needed id
-        | Gtypedef(id, _) -> needed id
+        | Gcompositedef(_, id, _, flds) -> needed id
+        | Gtypedef(id, ty) -> needed id
         | Genumdef(id, _, enu) ->
             needed id || List.exists (fun (id, _, _) -> needed id) enu
-        | Gpragma _ -> true in
+        | Gpragma s -> true in
       if need
       then simpl_globdecls (g :: accu) rem
       else begin remove_unused_debug g.gdesc; simpl_globdecls accu rem end
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 61441aeb..e80a4c8e 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -83,7 +83,7 @@ let const pp = function
           else fprintf pp "\" \"\\x%02Lx\" \"" c)
         l;
       fprintf pp "\""
-  | CEnum(id, _) ->
+  | CEnum(id, v) ->
       ident pp id
 
 let attr_arg pp = function
@@ -343,11 +343,11 @@ and init pp = function
       fprintf pp "@[<hov 1>{";
       List.iter (fun i -> fprintf pp "%a,@ " init i) il;
       fprintf pp "}@]"
-  | Init_struct(_, il) ->
+  | Init_struct(id, il) ->
       fprintf pp "@[<hov 1>{";
-      List.iter (fun (_, i) -> fprintf pp "%a,@ " init i) il;
+      List.iter (fun (fld, i) -> fprintf pp "%a,@ " init i) il;
       fprintf pp "}@]"
-  | Init_union(_, fld, i) ->
+  | Init_union(id, fld, i) ->
       fprintf pp "@[<hov 2>{.%s =@ %a}@]" fld.fld_name init i
 
 let simple_decl pp (id, ty) =
@@ -450,7 +450,7 @@ let rec stmt pp s =
       fprintf pp "return;"
   | Sreturn (Some e) ->
       fprintf pp "return %a;" exp (0, e)
-  | Sblock _ ->
+  | Sblock sl ->
       fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s
   | Sdecl d ->
       full_decl pp d
@@ -535,7 +535,7 @@ let globdecl pp g =
   | Genumdef(id, attrs, vals) ->
       fprintf pp "@[<v 2>enum%a %a {" attributes attrs ident id;
       List.iter
-        (fun (name, _, opt_e) ->
+        (fun (name, v, opt_e) ->
            fprintf pp "@ %a" ident name;
            begin match opt_e with
            | None -> ()
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 19f6d29a..1bbb8e98 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -73,7 +73,7 @@ let rec find_custom_attributes (names: string list)  (al: attributes) =
 let rec remove_custom_attributes (names: string list)  (al: attributes) =
   match al with
   | [] -> []
-  | Attr(name, _) :: tl when List.mem name names ->
+  | Attr(name, args) :: tl when List.mem name names ->
       remove_custom_attributes names tl
   | a :: tl ->
       a :: remove_custom_attributes names tl
@@ -137,12 +137,12 @@ let rec unroll env t =
 let rec attributes_of_type env t =
   match t with
   | TVoid a -> a
-  | TInt(_, a) -> a
-  | TFloat(_, a) -> a
-  | TPtr(_, a) -> a
-  | TArray(ty, _, a) -> add_attributes a (attributes_of_type env ty)
-  | TFun(_, _,_, a) -> a
-  | TNamed(_, _) -> attributes_of_type env (unroll env t)
+  | TInt(ik, a) -> a
+  | TFloat(fk, a) -> a
+  | TPtr(ty, a) -> a
+  | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty)
+  | TFun(ty, params, vararg, a) -> a
+  | TNamed(s, a) -> attributes_of_type env (unroll env t)
   | TStruct(s, a) ->
       let ci = Env.find_struct env s in add_attributes ci.ci_attr a
   | TUnion(s, a) ->
@@ -162,7 +162,7 @@ let rec change_attributes_type env (f: attributes -> attributes) t =
   | TArray(ty, sz, a) ->
       TArray(change_attributes_type env f ty, sz, f a)
   | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
-  | TNamed(_, _) ->
+  | TNamed(s, a) ->
       let t1 = unroll env t in
       let t2 = change_attributes_type env f t1 in
       if t2 = t1 then t else t2         (* avoid useless expansion *)
@@ -174,7 +174,7 @@ let remove_attributes_type env attr t =
   change_attributes_type env (fun a -> remove_attributes a attr) t
 
 let erase_attributes_type env t =
-  change_attributes_type env (fun _ -> []) t
+  change_attributes_type env (fun a -> []) t
 
 (* Remove all attributes from type that are not contained in attr *)
 let strip_attributes_type t attr =
@@ -224,7 +224,7 @@ let alignas_attribute al =
   let rec alignas_attr accu = function
   | [] -> accu
   | AAlignas n :: al -> alignas_attr (max n accu) al
-  | _ :: al -> alignas_attr accu al
+  | a :: al -> alignas_attr accu al
   in alignas_attr 0 al
 
 (* Type compatibility *)
@@ -260,14 +260,14 @@ let combine_types mode env t1 t2 =
     | None, _ -> sz2
     | _, None -> sz1
     | Some n1, Some n2 -> if n1 = n2 then Some n2 else raise Incompat
-  and comp_conv (_, ty) =
+  and comp_conv (id, ty) =
     match unroll env ty with
-    | TInt(kind, _) ->
+    | TInt(kind, attr) ->
         begin match kind with
         | IBool | IChar | ISChar | IUChar | IShort | IUShort -> raise Incompat
         | _ -> ()
         end
-    | TFloat(kind, _) ->
+    | TFloat(kind, attr) ->
         begin match kind with
         | FFloat -> raise Incompat
         | _ -> ()
@@ -295,7 +295,7 @@ let combine_types mode env t1 t2 =
           | Some l1, None -> List.iter comp_conv l1; (params1, vararg1)
           | Some l1, Some l2 ->
               if List.length l1 <> List.length l2 then raise Incompat;
-              let comp_param (_, ty1) (id2, ty2) =
+              let comp_param (id1, ty1) (id2, ty2) =
                 (id2, comp AttrIgnoreTop ty1 ty2) in
               (Some(List.map2 comp_param l1 l2), comp_base vararg1 vararg2)
         in
@@ -309,8 +309,8 @@ let combine_types mode env t1 t2 =
         TUnion(comp_base s1 s2, comp_attr m a1 a2)
     | TEnum(s1, a1), TEnum(s2, a2) ->
         TEnum(comp_base s1 s2, comp_attr m a1 a2)
-    | TEnum(s,a1), TInt(_,a2)
-    | TInt(_,a2), TEnum (s,a1) ->
+    | TEnum(s,a1), TInt(enum_ikind,a2)
+    | TInt(enum_ikind,a2), TEnum (s,a1) ->
         TEnum(s,comp_attr m a1 a2)
     | _, _ ->
         raise Incompat
@@ -432,7 +432,7 @@ let alignof_struct_union env members =
         | None -> None
         | Some a -> align_rec (max a al) rem
       end else begin
-        let (_, a, ml') = pack_bitfields ml in
+        let (s, a, ml') = pack_bitfields ml in
         align_rec (max a al) ml'
       end
   in align_rec 1 members
@@ -471,7 +471,7 @@ let rec sizeof env t =
   | TInt(ik, _) -> Some(sizeof_ikind ik)
   | TFloat(fk, _) -> Some(sizeof_fkind fk)
   | TPtr(_, _) -> Some(!config.sizeof_ptr)
-  | TArray(_, None, _) -> None
+  | TArray(ty, None, _) -> None
   | TArray(ty, Some n, _) as t' ->
       begin match sizeof env ty with
       | None -> None
@@ -721,7 +721,7 @@ let pointer_decay env t =
 let unary_conversion env t =
   match unroll env t with
   (* Promotion of small integer types *)
-  | TInt(kind, _) ->
+  | TInt(kind, attr) ->
       begin match kind with
       | IBool | IChar | ISChar | IUChar | IShort | IUShort ->
           TInt(IInt, [])
@@ -729,13 +729,13 @@ let unary_conversion env t =
           TInt(kind, [])
       end
   (* Enums are like signed ints *)
-  | TEnum(_, _) -> TInt(enum_ikind, [])
+  | TEnum(id, attr) -> TInt(enum_ikind, [])
   (* Arrays and functions decay automatically to pointers *)
   | TArray(ty, _, _) -> TPtr(ty, [])
   | TFun _ as ty -> TPtr(ty, [])
   (* Float types and pointer types lose their attributes *)
-  | TFloat(kind, _) -> TFloat(kind, [])
-  | TPtr(ty, _) -> TPtr(ty, [])
+  | TFloat(kind, attr) -> TFloat(kind, [])
+  | TPtr(ty, attr) -> TPtr(ty, [])
   (* Other types should not occur, but in doubt... *)
   | _ -> t
 
@@ -859,7 +859,7 @@ let type_of_constant = function
 
 let rec is_lvalue e =
   match e.edesc with
-  | EVar _ -> true
+  | EVar id -> true
   | EUnop((Oderef | Oarrow _), _) -> true
   | EUnop(Odot _, e') -> is_lvalue e'
   | EBinop(Oindex, _, _, _) -> true
@@ -905,8 +905,8 @@ let is_debug_stmt s =
    Custom attributes can safely be dropped or added. *)
 
 let valid_assignment_attr afrom ato =
-  let (afromstd, _) = List.partition attr_is_standard afrom
-  and (atostd,_) = List.partition attr_is_standard ato in
+  let (afromstd, afromcustom) = List.partition attr_is_standard afrom
+  and (atostd, atocustom) = List.partition attr_is_standard ato in
   incl_attributes afromstd atostd
 
 (* Check that an assignment is allowed *)
@@ -1031,11 +1031,11 @@ let rec default_init env ty =
   match unroll env ty with
   | TInt _ | TEnum _ ->
       Init_single (intconst 0L IInt)
-  | TFloat(_, _) ->
+  | TFloat(fk, _) ->
       Init_single floatconst0
-  | TPtr(_, _) ->
+  | TPtr(ty, _) ->
       Init_single nullconst
-  | TArray(_, _, _) ->
+  | TArray(ty, sz, _) ->
       Init_array []
   | TStruct(id, _) ->
       let rec default_init_fields = function
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index fb75c687..130f37cd 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -90,7 +90,7 @@ let previous_def fn env arg =
 let redef fn env arg =
   match previous_def fn env arg with
   | None -> false
-  | Some(id, _) -> Env.in_current_scope env id
+  | Some(id, info) -> Env.in_current_scope env id
 
 (* Forward declarations *)
 
@@ -289,8 +289,8 @@ let elab_attr_arg loc env a =
   | VARIABLE s ->
       begin try
         match Env.lookup_ident env s with
-        | (_, II_ident _) ->  AIdent s
-        | (_, II_enum v) -> AInt v
+        | (id, II_ident(sto, ty)) ->  AIdent s
+        | (id, II_enum v) -> AInt v
       with Env.Error _ ->
         AIdent s
       end
@@ -477,7 +477,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
     (* Now the other type specifiers *)
 
     | [Cabs.Tnamed id] ->
-        let (id', _) = wrap Env.lookup_typedef loc env id in
+        let (id', info) = wrap Env.lookup_typedef loc env id in
         simple (TNamed(id', []))
 
     | [Cabs.Tstruct_union(STRUCT, id, optmembers, a)] ->
@@ -702,7 +702,7 @@ and elab_struct_or_union_info kind loc env members attrs =
   (* Check for incomplete types *)
   let rec check_incomplete = function
   | [] -> ()
-  | [ { fld_typ = TArray(_, None, _) } ] when kind = Struct -> ()
+  | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> ()
         (* C99: ty[] allowed as last field of a struct *)
   | fld :: rem ->
       if wrap incomplete_type loc env' fld.fld_typ then
@@ -726,7 +726,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
           Env.lookup_composite env s, s
   in
   match optbinding, optmembers with
-  | Some(tag', _), None
+  | Some(tag', ci), None
     when (not only) || Env.in_current_scope env tag' ->
       (* Reference to an already declared struct or union.
          Special case: if this is an "only" declaration (without variable names)
@@ -808,7 +808,7 @@ and elab_enum only loc tag optmembers attrs env =
     if only then
       fatal_error loc
          "forward declaration of 'enum %s' is not allowed in ISO C" tag;
-      let (tag', _) = wrap Env.lookup_enum loc env tag in (tag', env)
+      let (tag', info) = wrap Env.lookup_enum loc env tag in (tag', env)
   | Some members ->
       if tag <> "" && redef Env.lookup_enum env tag then
         error loc "redefinition of 'enum %s'" tag;
@@ -904,12 +904,12 @@ module I = struct
   let top env name ty = (Ztop(name, ty), default_init env ty)
 
   (* Change the initializer for the current point *)
-  let set (z, _) i' = (z, i')
+  let set (z, i) i' = (z, i')
 
   (* Put the current point back to the top *)
   let rec to_top = function
-    | Ztop _, _ as zi -> zi
-    | Zarray(z, _, _,_, before, _, after), i ->
+    | Ztop(name, ty), i as zi -> zi
+    | Zarray(z, ty, sz, dfl, before, idx, after), i ->
         to_top (z, Init_array (List.rev_append before (i :: after)))
     | Zstruct(z, id, before, fld, after), i ->
         to_top (z, Init_struct(id, List.rev_append before ((fld, i) :: after)))
@@ -921,34 +921,34 @@ module I = struct
 
   (* The type of the current point *)
   let typeof = function
-    | Ztop(_, ty), _ -> ty
-    | Zarray(_, ty, _, _, _, _, _), _ -> ty
-    | Zstruct(_, _, _, fld, _), _ -> fld.fld_typ
-    | Zunion(_, _, fld), _ -> fld.fld_typ
+    | Ztop(name, ty), i -> ty
+    | Zarray(z, ty, sz, dfl, before, idx, after), i -> ty
+    | Zstruct(z, id, before, fld, after), i -> fld.fld_typ
+    | Zunion(z, id, fld), i -> fld.fld_typ
 
   (* The name of the path leading to the current point, for error reporting *)
   let rec zipname = function
-    | Ztop(name, _) -> name
-    | Zarray(z, _, _, _, _, idx, _) ->
+    | Ztop(name, ty) -> name
+    | Zarray(z, ty, sz, dfl, before, idx, after) ->
         sprintf "%s[%Ld]" (zipname z) idx
-    | Zstruct(z, _, _, fld, _) ->
+    | Zstruct(z, id, before, fld, after) ->
         sprintf "%s.%s" (zipname z) fld.fld_name
-    | Zunion(z, _, fld) ->
+    | Zunion(z, id, fld) ->
         sprintf "%s.%s" (zipname z) fld.fld_name
 
-  let name (z, _) = zipname z
+  let name (z, i) = zipname z
 
   (* Auxiliary functions to deal with arrays *)
   let index_below (idx: int64) (sz: int64 option) =
     match sz with None -> true | Some sz -> idx < sz
 
-  let il_head dfl = function [] -> dfl | ih :: _ -> ih
-  let il_tail = function [] -> [] | _ :: il -> il
+  let il_head dfl = function [] -> dfl | i1 :: il -> i1
+  let il_tail = function [] -> [] | i1 :: il -> il
 
   (* Advance the current point to the next point in right-up order.
      Return None if no next point, i.e. we are at top *)
   let rec next = function
-    | Ztop _, _ -> None
+    | Ztop(name, ty), i -> None
     | Zarray(z, ty, sz, dfl, before, idx, after), i ->
         let idx' = Int64.succ idx in
         if index_below idx' sz
@@ -973,11 +973,11 @@ module I = struct
           Some(Zarray(z, ty, sz, dfl, [], 0L, il_tail il), il_head dfl il)
         end
         else None
-    | TStruct _, Init_struct(_, []) ->
+    | TStruct(id, _), Init_struct(id', []) ->
         None
-    | TStruct(id, _), Init_struct(_, (fld1, i1) :: flds) ->
+    | TStruct(id, _), Init_struct(id', (fld1, i1) :: flds) ->
         Some(Zstruct(z, id, [], fld1, flds), i1)
-    | TUnion(id, _), Init_union(_, fld, i) ->
+    | TUnion(id, _), Init_union(id', fld, i) ->
         begin match (Env.find_union env id).ci_members with
         | [] -> None
         | fld1 :: _ ->
@@ -986,7 +986,7 @@ module I = struct
                  then i
                  else default_init env fld1.fld_typ)
         end
-    | (TStruct _ | TUnion _), Init_single _ ->
+    | (TStruct _ | TUnion _), Init_single a ->
         (* This is a previous whole-struct initialization that we
            are going to overwrite.  Revert to the default initializer. *)
         first env (z, default_init env ty)
@@ -1019,7 +1019,7 @@ module I = struct
   let rec member env (z, i as zi) name =
     let ty = typeof zi in
     match unroll env ty, i with
-    | TStruct(id, _), Init_struct(_, flds) ->
+    | TStruct(id, _), Init_struct(id', flds) ->
         let rec find before = function
           | [] -> None
           | (fld, i as f_i) :: after ->
@@ -1028,7 +1028,7 @@ module I = struct
               else
                 find (f_i :: before) after
         in find [] flds
-    | TUnion(id, _), Init_union(_, fld, i) ->
+    | TUnion(id, _), Init_union(id', fld, i) ->
         if fld.fld_name = name then
           Some(Zunion(z, id, fld), i)
         else begin
@@ -1041,7 +1041,7 @@ module I = struct
                   find rem
            in find (Env.find_union env id).ci_members
          end
-    | (TStruct _ | TUnion _), Init_single _ ->
+    | (TStruct _ | TUnion _), Init_single a ->
         member env (z, default_init env ty) name
     | _, _ ->
         None
@@ -1126,7 +1126,7 @@ and elab_item zi item il =
       | CStr _, _ ->
           error loc "initialization of an array of non-char elements with a string literal";
           elab_list zi il false
-      | CWStr s, TInt _ ->
+      | CWStr s, TInt(ik, _) ->
           if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then
             warning loc "initializer string for array of wide chars %s is too long"
                         (I.name zi);
@@ -1229,7 +1229,7 @@ let elab_expr loc env a =
 
   | VARIABLE s ->
       begin match wrap Env.lookup_ident loc env s with
-      | (id, II_ident(_, ty)) ->
+      | (id, II_ident(sto, ty)) ->
           { edesc = EVar id; etyp = ty }
       | (id, II_enum v) ->
           { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) }
@@ -1247,7 +1247,7 @@ let elab_expr loc env a =
         match (unroll env b1.etyp, unroll env b2.etyp) with
         | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t
         | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t
-        | _, _ -> error "incorrect types for array subscripting" in
+        | t1, t2 -> error "incorrect types for array subscripting" in
       { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres }
 
   | MEMBEROF(a1, fieldname) ->
@@ -1300,7 +1300,7 @@ let elab_expr loc env a =
   | BUILTIN_VA_ARG (a2, a3) ->
       let ident =
         match wrap Env.lookup_ident loc env "__builtin_va_arg" with
-          | (id, II_ident(_, ty)) -> { edesc = EVar id; etyp = ty }
+          | (id, II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty }
           | _ -> assert false
       in
       let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in
@@ -1329,10 +1329,10 @@ let elab_expr loc env a =
       (* Extract type information *)
       let (res, args, vararg) =
         match unroll env b1.etyp with
-        | TFun(res, args, vararg, _) -> (res, args, vararg)
-        | TPtr(ty, _) ->
+        | TFun(res, args, vararg, a) -> (res, args, vararg)
+        | TPtr(ty, a) ->
             begin match unroll env ty with
-            | TFun(res, args, vararg, _) -> (res, args, vararg)
+            | TFun(res, args, vararg, a) -> (res, args, vararg)
             | _ -> error "the function part of a call does not have a function type"
             end
         | _ -> error "the function part of a call does not have a function type"
@@ -1364,7 +1364,7 @@ let elab_expr loc env a =
       let (ty, _) = elab_type loc env spec dcl in
       begin match elab_initializer loc env "<compound literal>" ty ie with
       | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' }
-      | (_, None)   -> error "ill-formed compound literal"
+      | (ty', None)   -> error "ill-formed compound literal"
       end
 
 (* 6.5.3 Unary expressions *)
@@ -1487,8 +1487,8 @@ let elab_expr loc env a =
         else begin
           let ty =
             match unroll env b1.etyp, unroll env b2.etyp with
-            | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) -> ty
-            | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(ty, _, _)) -> ty
+            | (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 '+'";
@@ -1505,16 +1505,16 @@ let elab_expr loc env a =
           (tyres, tyres)
         end else begin
           match unroll env b1.etyp, unroll env b2.etyp with
-          | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) ->
+          | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
               (TPtr(ty, []), TPtr(ty, []))
-          | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(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, []), TPtr(ty, []))
-          | (TPtr(ty1, _) | TArray(ty1, _, _)),
-            (TPtr(ty2, _) | TArray(ty2, _, _)) ->
+          | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
+            (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
               if not (compatible_types AttrIgnoreAll env ty1 ty2) then
                 err "mismatch between pointer types in binary '-'";
               if not (pointer_arithmetic_ok env ty1) then
@@ -1585,9 +1585,9 @@ let elab_expr loc env a =
               | Some ty -> ty
             in
           { edesc = EConditional(b1, b2, b3); etyp = tyres }
-      | TPtr(ty1, _), TInt _ when is_literal_0 b3 ->
+      | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
           { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) }
-      | TInt _, TPtr(ty2, _) when is_literal_0 b2 ->
+      | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
           { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) }
       | ty1, ty2 ->
           match combine_types AttrIgnoreAll env ty1 ty2 with
@@ -1795,7 +1795,7 @@ let enter_typedefs loc env sto dl =
     if init <> NO_INIT then
       error loc "initializer in typedef";
     match previous_def Env.lookup_typedef env s with
-    | Some (_ ,ty') ->
+    | Some (s',ty') ->
         if equal_types env ty ty' then begin
           warning loc "redefinition of typedef '%s'" s;
           env
@@ -1846,7 +1846,7 @@ let enter_or_refine_ident local loc env s sto ty =
 	| Storage_register,_ -> Storage_register
       in
       (id, new_sto, Env.add_ident env id new_sto new_ty,new_ty)
-  | Some(id, II_enum _) when Env.in_current_scope env id ->
+  | Some(id, II_enum v) when Env.in_current_scope env id ->
       error loc "redefinition of enumerator '%s'" s;
       (id, sto, Env.add_ident env id sto ty,ty)
   | _ ->
@@ -1913,7 +1913,7 @@ let elab_fundef env spec name defs body loc =
           fatal_error loc "Parameter '%s' appears more than once in function declaration" id)
         params;
       (* Check that the declarations only declare parameters *)
-      let extract_name (Init_name(Name(s, _, _, loc') as name, ie)) =
+      let extract_name (Init_name(Name(s, dty, attrs, loc') as name, ie)) =
         if not (List.mem s params) then
           error loc' "Declaration of '%s' which is not a function parameter" s;
         if ie <> NO_INIT then
@@ -1947,7 +1947,7 @@ let elab_fundef env spec name defs body loc =
       in
       let params' = List.map search_param_type params in
       (TFun(ty_ret, Some params', false, attr), env1)
-    | _, Some _ -> assert false
+    | _, Some params -> assert false
   in
   (* Extract info from type *)
   let (ty_ret, params, vararg, attr) =
@@ -2093,7 +2093,7 @@ let rec elab_stmt env ctx s =
       begin match Ceval.integer_expr env a' with
         | None ->
             error loc "argument of 'case' must be an integer compile-time constant"
-        | Some _ -> ()
+        | Some n -> ()
       end;
       { sdesc = Slabeled(Scase a', elab_stmt env ctx s1); sloc = elab_loc loc }
 
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 9ab5e657..dae79ef2 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -120,7 +120,7 @@ let lookup_ident env s =
 
 let lookup_struct env s =
   try
-    let (_, ci as res) = IdentMap.lookup s env.env_tag in
+    let (id, ci as res) = IdentMap.lookup s env.env_tag in
     if ci.ci_kind <> Struct then
       raise(Error(Tag_mismatch(s, "struct", "union")));
     res
@@ -129,7 +129,7 @@ let lookup_struct env s =
 
 let lookup_union env s =
   try
-    let (_, ci as res) = IdentMap.lookup s env.env_tag in
+    let (id, ci as res) = IdentMap.lookup s env.env_tag in
     if ci.ci_kind <> Union then
       raise(Error(Tag_mismatch(s, "union", "struct")));
     res
@@ -245,7 +245,7 @@ let add_typedef env id info =
   { env with env_typedef = IdentMap.add id info env.env_typedef }
 
 let add_enum env id info =
-  let add_enum_item env (id, v, _) =
+  let add_enum_item env (id, v, exp) =
     { env with env_ident = IdentMap.add id (II_enum v) env.env_ident } in
   List.fold_left add_enum_item
     { env with env_enum = IdentMap.add id info env.env_enum }
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 5183df9b..c3d80272 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -150,7 +150,7 @@ let transf_outputs loc env = function
          when substituting the text *)
       let rec bind_outputs pos subst = function
       | [] -> (None, [], subst, pos, pos)
-      | (lbl, _, _) :: outputs ->
+      | (lbl, cstr, e) :: outputs ->
           bind_outputs (pos + 1) (set_label_reg lbl pos pos subst) outputs
       in bind_outputs 0 StringMap.empty outputs
 
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index b2b00e8c..871f2bf9 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -577,7 +577,7 @@ and singleline_comment = parse
           let rec doConcat wide str =
             try
               match Queue.peek tokens with
-              | STRING_LITERAL (wide', str', _) ->
+              | STRING_LITERAL (wide', str', loc) ->
                   ignore (Queue.pop tokens);
                   let (wide'', str'') = doConcat wide' str' in
                   if str'' <> []
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 6a60dfb8..aafa1caa 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -129,8 +129,8 @@ let transf_composite loc env su id attrs ml =
 
 let lookup_function env name =
   match Env.lookup_ident env name with
-  | (id, II_ident(_, ty)) -> (id, ty)
-  | (_, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
+  | (id, II_ident(sto, ty)) -> (id, ty)
+  | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
 
 (* Type for the access *)
 
@@ -387,7 +387,7 @@ let rec transf_globdecls env accu = function
   | [] -> List.rev accu
   | g :: gl ->
       match g.gdesc with
-      | Gdecl((sto, id, ty, _) as d) ->
+      | Gdecl((sto, id, ty, init) as d) ->
           transf_globdecls
             (Env.add_ident env id sto ty)
             ({g with gdesc = Gdecl(transf_decl g.gloc env d)} :: accu)
@@ -422,7 +422,7 @@ let rec transf_globdecls env accu = function
             (Env.add_enum env id {ei_members =  el; ei_attr = attr})
             (g :: accu)
             gl
-      | Gpragma _ ->
+      | Gpragma p ->
           transf_globdecls env (g :: accu) gl
 
 (* Program *)
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 0d92c514..664f6a28 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -182,7 +182,7 @@ and stmt_desc env = function
   | Sgoto lbl -> Sgoto lbl
   | Sreturn a -> Sreturn (optexp env a)
   | Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl'
-  | Sdecl _ -> assert false
+  | Sdecl d -> assert false
   | Sasm(attr, txt, outputs, inputs, flags) ->
        Sasm(attr, txt,
             List.map (asm_operand env) outputs,
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 95f133bd..04f0021a 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -217,7 +217,7 @@ let rec transf_type env t =
           TFun(tres', None, vararg, attr)
       | Ret_ref ->
           TFun(TVoid [], None, vararg, add_attributes attr attr_structret)
-      | Ret_value(ty, _, _) ->
+      | Ret_value(ty, sz, al) ->
           TFun(ty, None, vararg, attr)
       end
   | TFun(tres, Some args, vararg, attr) ->
@@ -230,7 +230,7 @@ let rec transf_type env t =
           let res = Env.fresh_ident "_res" in
           TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg,
                add_attributes attr attr_structret)
-      | Ret_value(ty, _, _) ->
+      | Ret_value(ty, sz, al) ->
           TFun(ty, Some args', vararg, attr)
       end
   | TPtr(t1, attr) ->
@@ -251,7 +251,7 @@ and transf_funargs env = function
           (id, t') :: args'
       | Param_ref_caller ->
           (id, TPtr(t', [])) :: args'
-      | Param_flattened(n, _, _) ->
+      | Param_flattened(n, sz, al) ->
           list_map_n (fun _ -> (Env.fresh_ident id.name, uint)) n
           @ args'
 
@@ -261,7 +261,7 @@ let rec translates_to_extended_lvalue arg =
   is_lvalue arg ||
   (match arg.edesc with
    | ECall _ -> true
-   | EBinop(Ocomma, _, b, _) -> translates_to_extended_lvalue b
+   | EBinop(Ocomma, a, b, _) -> translates_to_extended_lvalue b
    | _ -> false)
 
 let rec transf_expr env ctx e =
@@ -279,7 +279,7 @@ let rec transf_expr env ctx e =
       {edesc = EUnop(op, transf_expr env Val e1); etyp = newty}
   | EBinop(Oassign, lhs, {edesc = ECall(fn, args); etyp = ty}, _) ->
       transf_call env ctx (Some (transf_expr env Val lhs)) fn args ty
-  | EBinop(Ocomma, e1, e2, _) ->
+  | EBinop(Ocomma, e1, e2, ty) ->
       ecomma (transf_expr env Effects e1) (transf_expr env ctx e2)
   | EBinop(op, e1, e2, ty) ->
       {edesc = EBinop(op, transf_expr env Val e1,
@@ -349,7 +349,7 @@ and transf_call env ctx opt_lhs fn args ty =
               ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
                      (eassign lhs tmp)
           end
-      | Ret_value(ty_ret, _, _) ->
+      | Ret_value(ty_ret, sz, al) ->
           let ecall = {edesc = ECall(fn', args'); etyp = ty_ret} in
           begin match ctx, opt_lhs with
           | Effects, None ->
@@ -461,7 +461,7 @@ let rec transf_stmt s =
       {s with sdesc = Sswitch(transf_expr Val e, transf_stmt s1)}
   | Slabeled(lbl, s1) ->
       {s with sdesc = Slabeled(lbl, transf_stmt s1)}
-  | Sgoto _ -> s
+  | Sgoto lbl -> s
   | Sreturn None -> s
   | Sreturn(Some e) ->
       let e' = transf_expr Val e in
@@ -524,7 +524,7 @@ let rec transf_funparams loc env params =
           ((x, tpx) :: params',
            actions,
            IdentMap.add x estarx subst)
-      | Param_flattened(n, _, _) ->
+      | Param_flattened(n, sz, al) ->
           let y = new_temp ~name:x.name (ty_buffer n) in
           let yparts = list_map_n (fun _ -> Env.fresh_ident x.name) n in
           let assign_part e p act =
@@ -559,7 +559,7 @@ let transf_fundef env f =
          TVoid [],
          (vres, tres) :: params,
          transf_funbody env (subst_stmt subst f.fd_body) (Some eeres))
-    | Ret_value(ty, _, _) ->
+    | Ret_value(ty, sz, al) ->
         (f.fd_attrib,
          ty,
          params,
@@ -573,7 +573,7 @@ let transf_fundef env f =
 
 (* Composites *)
 
-let transf_composite env _ _ attr fl =
+let transf_composite env su id attr fl =
   (attr, List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl)
 
 (* Entry point *)
@@ -591,5 +591,5 @@ let program p =
     ~decl:transf_decl
     ~fundef:transf_fundef
     ~composite:transf_composite
-    ~typedef:(fun env _ ty -> transf_type env ty)
+    ~typedef:(fun env id ty -> transf_type env ty)
     p
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 685ef7e1..0a2ce3bb 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -141,7 +141,7 @@ let expand_postincrdecr ~read ~write env ctx op l =
    and preserving the statement structure.
    If [decl] is not given, it applies only to unblocked code. *)
 
-let stmt ~expr ?(decl = fun _ _ -> assert false) env s =
+let stmt ~expr ?(decl = fun env decl -> assert false) env s =
   let rec stm s =
   match s.sdesc with
   | Sskip -> s
@@ -163,7 +163,7 @@ let stmt ~expr ?(decl = fun _ _ -> assert false) env s =
       {s with sdesc = Sswitch(expr s.sloc env Val e, stm s1)}
   | Slabeled(lbl, s) ->
       {s with sdesc = Slabeled(lbl, stm s)}
-  | Sgoto _ -> s
+  | Sgoto lbl -> s
   | Sreturn None -> s
   | Sreturn (Some e) ->
       {s with sdesc = Sreturn(Some(expr s.sloc env Val e))}
@@ -191,12 +191,12 @@ let fundef trstmt env f =
 (* Generic transformation of a program *)
 
 let program
-    ?(decl = fun _ d -> d)
-    ?(fundef = fun _ fd -> fd)
-    ?(composite = fun _ _ _ attr fl -> (attr, fl))
-    ?(typedef = fun _ _ ty -> ty)
-    ?(enum = fun _ _ attr members -> (attr, members))
-    ?(pragma = fun _ s -> s)
+    ?(decl = fun env d -> d)
+    ?(fundef = fun env fd -> fd)
+    ?(composite = fun env su id attr fl -> (attr, fl))
+    ?(typedef = fun env id ty -> ty)
+    ?(enum = fun env id attr members -> (attr, members))
+    ?(pragma = fun env s -> s)
     p =
 
   let rec transf_globdecls env accu = function
@@ -204,7 +204,7 @@ let program
   | g :: gl ->
       let (desc', env') =
         match g.gdesc with
-        | Gdecl((sto, id, ty, _) as d) ->
+        | Gdecl((sto, id, ty, init) as d) ->
            (Gdecl(decl env d), Env.add_ident env id sto ty)
         | Gfundef f ->
            (Gfundef(fundef env f),
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index eaf49164..0669be6e 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -46,13 +46,13 @@ let rec local_initializer env path init k =
             (array_init (Int64.succ pos) il')
         end in
       array_init 0L il
-  | Init_struct(_, fil) ->
+  | Init_struct(id, fil) ->
       let field_init (fld, i) k =
         local_initializer env
           { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
           i k in
       List.fold_right field_init fil k
-  | Init_union(_, fld, i) ->
+  | Init_union(id, fld, i) ->
       local_initializer env
         { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
         i k
@@ -293,7 +293,7 @@ let rec unblock_stmt env ctx ploc s =
   | Slabeled(lbl, s1) ->
       add_lineno ctx ploc s.sloc
         {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
-  | Sgoto _ ->
+  | Sgoto lbl ->
       add_lineno ctx ploc s.sloc s
   | Sreturn None ->
       add_lineno ctx ploc s.sloc s
@@ -311,7 +311,7 @@ let rec unblock_stmt env ctx ploc s =
           id:: ctx
         else ctx in
       unblock_block env ctx' ploc sl
-  | Sdecl _ ->
+  | Sdecl d ->
       assert false
   | Sasm(attr, template, outputs, inputs, clob) ->
       let expand_asm_operand (lbl, cstr, e) =