Code cleanup.

Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.

16 files changed, 194 insertions, 230 deletions

diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index bbc39456..6e325ff2 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -19,7 +19,7 @@
 
 open Printf
 open Machine
-open C
+open !C
 open Cutil
 open Transform
 
@@ -60,12 +60,6 @@ let unsigned_ikind_for_carrier nbits =
   if nbits <= 8 * !config.sizeof_longlong then IULongLong else
   assert false
 
-let fits_unsigned v n =
-  v >= 0L && v < Int64.shift_left 1L n
-
-let fits_signed v n =
-  let p =  Int64.shift_left 1L (n-1) in v >= Int64.neg p && v < p
-
 let is_signed_enum_bitfield env sid fld eid n =
   let info = Env.find_enum env eid in
   if List.for_all (fun (_, v, _) -> int_representable v n false) info.Env.ei_members
@@ -73,7 +67,7 @@ let is_signed_enum_bitfield env sid fld eid n =
   else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members
   then true
   else begin
-    Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.name n;
+    Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n;
     false
   end
 
@@ -519,7 +513,7 @@ let transf_decl env (sto, id, ty, init_opt) =
 
 let transf_stmt env s =
   Transform.stmt
-     ~expr:(fun loc env ctx e -> transf_exp env ctx e)
+     ~expr:(fun _ env ctx e -> transf_exp env ctx e)
      ~decl:transf_decl
      env s
 
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 74b535d4..7a706da2 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(v, fk) -> raise Notconst
+  | CFloat _ -> raise Notconst
   | CStr s -> S s
   | CWStr s -> WS s
-  | CEnum(id, v) -> I v
+  | CEnum(_, v) -> I v
 
 let is_signed env ty =
   match unroll env ty with
@@ -91,7 +91,7 @@ let is_signed env ty =
   | TEnum(_, _) -> is_signed_ikind enum_ikind
   | _ -> false
 
-let cast env ty_to ty_from v =
+let cast env ty_to v =
   match unroll env ty_to, v with
   | TInt(IBool, _), _ ->
       if boolean_value v then I 1L else I 0L
@@ -101,11 +101,11 @@ let cast env ty_to ty_from v =
       if sizeof_ikind ik >= !config.sizeof_ptr
       then v
       else raise Notconst
-  | TPtr(ty, _), I n ->
+  | TPtr _, I n ->
       I (normalize_int n (ptr_t_ikind ()))
-  | TPtr(ty, _), (S _ | WS _) ->
+  | TPtr _, (S _ | WS _) ->
       v
-  | TEnum(_, _), I n ->
+  | TEnum _, I n ->
       I (normalize_int n enum_ikind)
   | _, _ ->
       raise Notconst
@@ -118,12 +118,12 @@ let unop env op tyres ty v =
    | Olognot, _, _ -> if boolean_value v then I 0L else I 1L
    | Onot, _, I n -> I (Int64.lognot n)
    | _ -> raise Notconst
-  in cast env ty tyres res
+  in cast env ty res
 
-let comparison env direction ptraction tyop ty1 v1 ty2 v2 =
+let comparison env direction ptraction tyop v1 v2 =
   (* tyop = type at which the comparison is done *)
   let b =
-    match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+    match cast env tyop v1, cast env tyop v2 with
     | I n1, I n2 ->
         if is_signed env tyop
         then direction (compare n1 n2) 0
@@ -143,25 +143,25 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
     match op with
     | Oadd ->
         if is_arith_type env ty1 && is_arith_type env ty2 then begin
-          match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+          match cast env tyop v1, cast env tyop v2 with
           | I n1, I n2 -> I (Int64.add n1 n2)
           | _, _ -> raise Notconst
         end else
           raise Notconst
     | Osub ->
         if is_arith_type env ty1 && is_arith_type env ty2 then begin
-          match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+          match cast env tyop v1, cast env tyop v2 with
           | I n1, I n2 -> I (Int64.sub n1 n2)
           | _, _ -> raise Notconst
         end else
           raise Notconst
     | Omul ->
-        begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+        begin match cast env tyop v1, cast env tyop v2 with
           | I n1, I n2 -> I (Int64.mul n1 n2)
           | _, _ -> raise Notconst
         end
     | Odiv ->
-        begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+        begin match cast env tyop v1, cast env tyop v2 with
           | I n1, I n2 ->
               if n2 = 0L then raise Notconst else
               if is_signed env tyop then I (Int64.div n1 n2)
@@ -206,17 +206,17 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
           | _, _ -> raise Notconst
         end
     | Oeq ->
-        comparison env (=) (Some false) tyop ty1 v1 ty2 v2
+        comparison env (=) (Some false) tyop v1 v2
     | One ->
-        comparison env (<>) (Some true) tyop ty1 v1 ty2 v2
+        comparison env (<>) (Some true) tyop v1 v2
     | Olt ->
-        comparison env (<) None tyop ty1 v1 ty2 v2
+        comparison env (<) None tyop v1 v2
     | Ogt ->
-        comparison env (>) None tyop ty1 v1 ty2 v2
+        comparison env (>) None tyop v1 v2
     | Ole ->
-        comparison env (<=) None tyop ty1 v1 ty2 v2
+        comparison env (<=) None tyop v1 v2
     | Oge ->
-        comparison env (>=) None tyop ty1 v1 ty2 v2
+        comparison env (>=) None tyop v1 v2
     | Ocomma ->
         v2
     | Ologand ->
@@ -229,7 +229,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
         else if boolean_value v2 then I 1L else I 0L
     | _ -> raise Notconst
   (* force normalization of result, e.g. of double to float *)
-  in cast env tyres tyres res
+  in cast env tyres res
 
 let rec expr env e =
   match e.edesc with
@@ -253,11 +253,10 @@ let rec expr env e =
       binop env op ty e.etyp e1.etyp (expr env e1) e2.etyp (expr env e2)
   | EConditional(e1, e2, e3) ->
       if boolean_value (expr env e1)
-      then cast env e.etyp e2.etyp (expr env e2)
-      else cast env e.etyp e3.etyp (expr env e3)
-  (* | ECast(TInt (_, _), EConst (CFloat (_, _))) -> TODO *)
+      then cast env e.etyp (expr env e2)
+      else cast env e.etyp (expr env e3)
   | ECast(ty, e1) ->
-      cast env ty e1.etyp (expr env e1)
+      cast env ty (expr env e1)
   | ECompound _ ->
       raise Notconst
   | ECall _ ->
@@ -265,14 +264,14 @@ let rec expr env e =
 
 let integer_expr env e =
   try
-    match cast env (TInt(ILongLong, [])) e.etyp (expr env e) with
+    match cast env (TInt(ILongLong, [])) (expr env e) with
     | I n -> Some n
     | _   -> None
   with Notconst -> None
 
 let constant_expr env ty e =
   try
-    match unroll env ty, cast env ty e.etyp (expr env e) with
+    match unroll env ty, cast env ty (expr env e) with
     | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
     | TPtr(_, _), I n -> Some(CInt(n, IInt, ""))
     | TPtr(_, _), S s -> Some(CStr s)
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index fe674d9b..845232aa 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 (id, ty) -> add_typ ty) vl
+  List.iter (fun (_, 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, v)) -> addref id
+  | EConst (CEnum(id, _)) -> addref id
   | EConst _ -> ()
   | ESizeof ty -> add_typ ty
   | EAlignof ty -> add_typ ty
   | EVar id -> addref id
-  | EUnop(op, e1) -> add_exp e1
-  | EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
+  | EUnop(_, e1) -> add_exp e1
+  | EBinop(_, e1, e2, _) -> 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 (sto, id, ty, init) =
+let add_decl (_, _, ty, init) =
   add_typ ty;
   match init with None -> () | Some i -> add_init i
 
-let add_asm_operand (lbl, cstr, e) = add_exp e
+let add_asm_operand (_, _, 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 lbl -> ()
+  | Sgoto _ -> ()
   | Sreturn None -> ()
   | Sreturn(Some e) -> add_exp e
   | Sblock sl -> List.iter add_stmt sl
   | Sdecl d -> add_decl d
-  | Sasm(attr, template, outputs, inputs, flags) ->
+  | Sasm(_, _, outputs, inputs, _) ->
       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 (id, v, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
+    (fun (_, _, 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, id, ty, init) =
+let visible_decl (sto, _, ty, _) =
   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((sto, id, ty, init) as decl) ->
+      | Gdecl((_, id, _, _) 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((sto, id, ty, init) as decl) -> visible_decl decl || needed id
+        | Gdecl((_, id, _, _) as decl) -> visible_decl decl || needed id
         | Gfundef f -> visible_fundef f || needed f.fd_name
         | Gcompositedecl(_, id, _) -> needed id
-        | Gcompositedef(_, id, _, flds) -> needed id
-        | Gtypedef(id, ty) -> needed id
+        | Gcompositedef(_, id, _, _) -> needed id
+        | Gtypedef(id, _) -> needed id
         | Genumdef(id, _, enu) ->
             needed id || List.exists (fun (id, _, _) -> needed id) enu
-        | Gpragma s -> true in
+        | Gpragma _ -> 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 e80a4c8e..61441aeb 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, v) ->
+  | CEnum(id, _) ->
       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(id, il) ->
+  | Init_struct(_, il) ->
       fprintf pp "@[<hov 1>{";
-      List.iter (fun (fld, i) -> fprintf pp "%a,@ " init i) il;
+      List.iter (fun (_, i) -> fprintf pp "%a,@ " init i) il;
       fprintf pp "}@]"
-  | Init_union(id, fld, i) ->
+  | Init_union(_, 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 sl ->
+  | Sblock _ ->
       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, v, opt_e) ->
+        (fun (name, _, opt_e) ->
            fprintf pp "@ %a" ident name;
            begin match opt_e with
            | None -> ()
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index c15a7adf..19f6d29a 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -15,7 +15,6 @@
 
 (* Operations on C types and abstract syntax *)
 
-open Printf
 open Cerrors
 open C
 open Env
@@ -74,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, args) :: tl when List.mem name names ->
+  | Attr(name, _) :: tl when List.mem name names ->
       remove_custom_attributes names tl
   | a :: tl ->
       a :: remove_custom_attributes names tl
@@ -138,12 +137,12 @@ let rec unroll env t =
 let rec attributes_of_type env t =
   match t with
   | TVoid a -> a
-  | 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)
+  | 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)
   | TStruct(s, a) ->
       let ci = Env.find_struct env s in add_attributes ci.ci_attr a
   | TUnion(s, a) ->
@@ -163,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(s, a) ->
+  | TNamed(_, _) ->
       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 *)
@@ -175,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 a -> []) t
+  change_attributes_type env (fun _ -> []) t
 
 (* Remove all attributes from type that are not contained in attr *)
 let strip_attributes_type t attr =
@@ -194,7 +193,7 @@ let strip_attributes_type t attr =
 
 (* Remove the last attribute from the toplevel and return the changed type *)
 let strip_last_attribute typ  =
-  let rec hd_opt l = match l with
+  let hd_opt l = match l with
     [] -> None,[]
   | a::rest -> Some a,rest in
   match typ with
@@ -225,7 +224,7 @@ let alignas_attribute al =
   let rec alignas_attr accu = function
   | [] -> accu
   | AAlignas n :: al -> alignas_attr (max n accu) al
-  | a :: al -> alignas_attr accu al
+  | _ :: al -> alignas_attr accu al
   in alignas_attr 0 al
 
 (* Type compatibility *)
@@ -261,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 (id, ty) =
+  and comp_conv (_, ty) =
     match unroll env ty with
-    | TInt(kind, attr) ->
+    | TInt(kind, _) ->
         begin match kind with
         | IBool | IChar | ISChar | IUChar | IShort | IUShort -> raise Incompat
         | _ -> ()
         end
-    | TFloat(kind, attr) ->
+    | TFloat(kind, _) ->
         begin match kind with
         | FFloat -> raise Incompat
         | _ -> ()
@@ -296,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 (id1, ty1) (id2, ty2) =
+              let comp_param (_, ty1) (id2, ty2) =
                 (id2, comp AttrIgnoreTop ty1 ty2) in
               (Some(List.map2 comp_param l1 l2), comp_base vararg1 vararg2)
         in
@@ -310,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(enum_ikind,a2)
-    | TInt(enum_ikind,a2), TEnum (s,a1) ->
+    | TEnum(s,a1), TInt(_,a2)
+    | TInt(_,a2), TEnum (s,a1) ->
         TEnum(s,comp_attr m a1 a2)
     | _, _ ->
         raise Incompat
@@ -433,7 +432,7 @@ let alignof_struct_union env members =
         | None -> None
         | Some a -> align_rec (max a al) rem
       end else begin
-        let (s, a, ml') = pack_bitfields ml in
+        let (_, a, ml') = pack_bitfields ml in
         align_rec (max a al) ml'
       end
   in align_rec 1 members
@@ -472,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(ty, None, _) -> None
+  | TArray(_, None, _) -> None
   | TArray(ty, Some n, _) as t' ->
       begin match sizeof env ty with
       | None -> None
@@ -561,7 +560,7 @@ let incomplete_type env t =
 
 (* Computing composite_info records *)
 
-let composite_info_decl env su attr =
+let composite_info_decl su attr =
   { ci_kind = su; ci_members = [];
     ci_alignof = None; ci_sizeof = None;
     ci_attr = attr }
@@ -722,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, attr) ->
+  | TInt(kind, _) ->
       begin match kind with
       | IBool | IChar | ISChar | IUChar | IShort | IUShort ->
           TInt(IInt, [])
@@ -730,13 +729,13 @@ let unary_conversion env t =
           TInt(kind, [])
       end
   (* Enums are like signed ints *)
-  | TEnum(id, attr) -> TInt(enum_ikind, [])
+  | TEnum(_, _) -> 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, attr) -> TFloat(kind, [])
-  | TPtr(ty, attr) -> TPtr(ty, [])
+  | TFloat(kind, _) -> TFloat(kind, [])
+  | TPtr(ty, _) -> TPtr(ty, [])
   (* Other types should not occur, but in doubt... *)
   | _ -> t
 
@@ -860,7 +859,7 @@ let type_of_constant = function
 
 let rec is_lvalue e =
   match e.edesc with
-  | EVar id -> true
+  | EVar _ -> true
   | EUnop((Oderef | Oarrow _), _) -> true
   | EUnop(Odot _, e') -> is_lvalue e'
   | EBinop(Oindex, _, _, _) -> true
@@ -892,7 +891,7 @@ let is_literal_0 e =
 
 let is_debug_stmt s =
   let is_debug_call = function
-    | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug"
+    | (ECall ({edesc = EVar id; _},_)) -> id.C.name = "__builtin_debug"
     | _ -> false in
   match s.sdesc with
   | Sdo {edesc = e;_} ->
@@ -906,8 +905,8 @@ let is_debug_stmt s =
    Custom attributes can safely be dropped or added. *)
 
 let valid_assignment_attr afrom ato =
-  let (afromstd, afromcustom) = List.partition attr_is_standard afrom
-  and (atostd, atocustom) = List.partition attr_is_standard ato in
+  let (afromstd, _) = List.partition attr_is_standard afrom
+  and (atostd,_) = List.partition attr_is_standard ato in
   incl_attributes afromstd atostd
 
 (* Check that an assignment is allowed *)
@@ -1032,11 +1031,11 @@ let rec default_init env ty =
   match unroll env ty with
   | TInt _ | TEnum _ ->
       Init_single (intconst 0L IInt)
-  | TFloat(fk, _) ->
+  | TFloat(_, _) ->
       Init_single floatconst0
-  | TPtr(ty, _) ->
+  | TPtr(_, _) ->
       Init_single nullconst
-  | TArray(ty, sz, _) ->
+  | TArray(_, _, _) ->
       Init_array []
   | TStruct(id, _) ->
       let rec default_init_fields = function
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b353cba3..3dcfe4aa 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -102,13 +102,11 @@ val sizeof_ikind: ikind -> int
   (* Return the size of the given integer kind. *)
 val sizeof_fkind: fkind -> int
   (* Return the size of the given float kind. *)
-val is_signed_ikind: ikind -> bool
-  (* Return true if the given integer kind is signed, false if unsigned. *)
 
 (* Computing composite_info records *)
 
 val composite_info_decl:
-  Env.t -> struct_or_union -> attributes -> Env.composite_info
+  struct_or_union -> attributes -> Env.composite_info
 val composite_info_def:
   Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
 val struct_layout:
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index d7a1212a..ceab0aa5 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -19,9 +19,9 @@
 
 open Format
 open Machine
-open Cabs
+open !Cabs
 open Cabshelper
-open C
+open !C
 open Cutil
 open Env
 
@@ -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, info) -> Env.in_current_scope env id
+  | Some(id, _) -> Env.in_current_scope env id
 
 (* Forward declarations *)
 
@@ -203,7 +203,7 @@ let elab_int_constant loc s0 =
   in
   (v, ty)
 
-let elab_float_constant loc f =
+let elab_float_constant f =
   let ty = match f.suffix_FI with
     | Some ("l"|"L") -> FLongDouble
     | Some ("f"|"F") -> FFloat
@@ -265,7 +265,7 @@ let elab_constant loc = function
       let (v, ik) = elab_int_constant loc s in
       CInt(v, ik, s)
   | CONST_FLOAT f ->
-      let (v, fk) = elab_float_constant loc f in
+      let (v, fk) = elab_float_constant f in
       CFloat(v, fk)
   | CONST_CHAR(wide, s) ->
       CInt(elab_char_constant loc wide s, IInt, "")
@@ -289,8 +289,8 @@ let elab_attr_arg loc env a =
   | VARIABLE s ->
       begin try
         match Env.lookup_ident env s with
-        | (id, II_ident(sto, ty)) ->  AIdent s
-        | (id, II_enum v) -> AInt v
+        | (_, II_ident _) ->  AIdent s
+        | (_, II_enum v) -> AInt v
       with Env.Error _ ->
         AIdent s
       end
@@ -319,7 +319,7 @@ let elab_gcc_attr loc env = function
         warning loc "cannot parse '%s' attribute, ignored" v; []
       end
 
-let is_power_of_two n = n > 0L && Int64.(logand n (pred n)) = 0L
+let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L
 
 let extract_alignas loc a =
   match a with
@@ -477,7 +477,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
     (* Now the other type specifiers *)
 
     | [Cabs.Tnamed id] ->
-        let (id', info) = wrap Env.lookup_typedef loc env id in
+        let (id', _) = wrap Env.lookup_typedef loc env id in
         simple (TNamed(id', []))
 
     | [Cabs.Tstruct_union(STRUCT, id, optmembers, a)] ->
@@ -569,7 +569,7 @@ and elab_parameters env params =
   let (vars, _) = mmap elab_parameter (Env.new_scope env) params in
   (* Catch special case f(t) where t is void or a typedef to void *)
   match vars with
-    | [ ( {name=""}, t) ] when is_void_type env t -> []
+    | [ ( {C.name=""}, t) ] when is_void_type env t -> []
     | _ -> vars
 
 (* Elaboration of a function parameter *)
@@ -578,7 +578,7 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) =
   let (sto, inl, tydef, bty, env1) = elab_specifier loc env spec in
   if tydef then
     error loc "'typedef' used in function parameter";
-  let ((ty, _), env2) = elab_type_declarator loc env1 bty false decl in
+  let ((ty, _), _) = elab_type_declarator loc env1 bty false decl in
   let ty = add_attributes_type (elab_attributes env attr) ty in
   if sto <> Storage_default && sto <> Storage_register then
     error loc
@@ -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(ty_elt, None, _) } ] when kind = Struct -> ()
+  | [ { fld_typ = TArray(_, 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', ci), None
+  | Some(tag', _), 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)
@@ -753,7 +753,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (* declaration of an incomplete struct or union *)
       if tag = "" then
         error loc "anonymous, incomplete struct or union";
-      let ci = composite_info_decl env kind attrs in
+      let ci = composite_info_decl kind attrs in
       (* enter it with a new name *)
       let (tag', env') = Env.enter_composite env tag ci in
       (* emit it *)
@@ -761,7 +761,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (tag', env')
   | _, Some members ->
       (* definition of a complete struct or union *)
-      let ci1 = composite_info_decl env kind attrs in
+      let ci1 = composite_info_decl kind attrs in
       (* enter it, incomplete, with a new name *)
       let (tag', env') = Env.enter_composite env tag ci1 in
       (* emit a declaration so that inner structs and unions can refer to it *)
@@ -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', info) = wrap Env.lookup_enum loc env tag in (tag', env)
+      let (tag', _) = 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;
@@ -900,18 +900,16 @@ module I = struct
               * ident                   (* union type *)
               * field                   (* current member *)
 
-  type state = zipinit * init        (* current point & init for this point *)
-
   (* The initial state: default initialization, current point at top *)
   let top env name ty = (Ztop(name, ty), default_init env ty)
 
   (* Change the initializer for the current point *)
-  let set (z, i) i' = (z, i')
+  let set (z, _) i' = (z, i')
 
   (* Put the current point back to the top *)
   let rec to_top = function
-    | Ztop(name, ty), i as zi -> zi
-    | Zarray(z, ty, sz, dfl, before, idx, after), i ->
+    | Ztop _, _ as zi -> zi
+    | Zarray(z, _, _,_, before, _, 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)))
@@ -923,34 +921,34 @@ module I = struct
 
   (* The type of the current point *)
   let typeof = function
-    | 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
+    | Ztop(_, ty), _ -> ty
+    | Zarray(_, ty, _, _, _, _, _), _ -> ty
+    | Zstruct(_, _, _, fld, _), _ -> fld.fld_typ
+    | Zunion(_, _, fld), _ -> fld.fld_typ
 
   (* The name of the path leading to the current point, for error reporting *)
   let rec zipname = function
-    | Ztop(name, ty) -> name
-    | Zarray(z, ty, sz, dfl, before, idx, after) ->
+    | Ztop(name, _) -> name
+    | Zarray(z, _, _, _, _, idx, _) ->
         sprintf "%s[%Ld]" (zipname z) idx
-    | Zstruct(z, id, before, fld, after) ->
+    | Zstruct(z, _, _, fld, _) ->
         sprintf "%s.%s" (zipname z) fld.fld_name
-    | Zunion(z, id, fld) ->
+    | Zunion(z, _, fld) ->
         sprintf "%s.%s" (zipname z) fld.fld_name
 
-  let name (z, i) = zipname z
+  let name (z, _) = 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 | i1 :: il -> i1
-  let il_tail = function [] -> [] | i1 :: il -> il
+  let il_head dfl = function [] -> dfl | ih :: _ -> ih
+  let il_tail = function [] -> [] | _ :: 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(name, ty), i -> None
+    | Ztop _, _ -> None
     | Zarray(z, ty, sz, dfl, before, idx, after), i ->
         let idx' = Int64.succ idx in
         if index_below idx' sz
@@ -975,11 +973,11 @@ module I = struct
           Some(Zarray(z, ty, sz, dfl, [], 0L, il_tail il), il_head dfl il)
         end
         else None
-    | TStruct(id, _), Init_struct(id', []) ->
+    | TStruct _, Init_struct(_, []) ->
         None
-    | TStruct(id, _), Init_struct(id', (fld1, i1) :: flds) ->
+    | TStruct(id, _), Init_struct(_, (fld1, i1) :: flds) ->
         Some(Zstruct(z, id, [], fld1, flds), i1)
-    | TUnion(id, _), Init_union(id', fld, i) ->
+    | TUnion(id, _), Init_union(_, fld, i) ->
         begin match (Env.find_union env id).ci_members with
         | [] -> None
         | fld1 :: _ ->
@@ -988,7 +986,7 @@ module I = struct
                  then i
                  else default_init env fld1.fld_typ)
         end
-    | (TStruct _ | TUnion _), Init_single a ->
+    | (TStruct _ | TUnion _), Init_single _ ->
         (* 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)
@@ -1021,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(id', flds) ->
+    | TStruct(id, _), Init_struct(_, flds) ->
         let rec find before = function
           | [] -> None
           | (fld, i as f_i) :: after ->
@@ -1030,7 +1028,7 @@ module I = struct
               else
                 find (f_i :: before) after
         in find [] flds
-    | TUnion(id, _), Init_union(id', fld, i) ->
+    | TUnion(id, _), Init_union(_, fld, i) ->
         if fld.fld_name = name then
           Some(Zunion(z, id, fld), i)
         else begin
@@ -1043,7 +1041,7 @@ module I = struct
                   find rem
            in find (Env.find_union env id).ci_members
          end
-    | (TStruct _ | TUnion _), Init_single a ->
+    | (TStruct _ | TUnion _), Init_single _ ->
         member env (z, default_init env ty) name
     | _, _ ->
         None
@@ -1128,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(ik, _) ->
+      | CWStr s, TInt _ ->
           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);
@@ -1231,7 +1229,7 @@ let elab_expr loc env a =
 
   | VARIABLE s ->
       begin match wrap Env.lookup_ident loc env s with
-      | (id, II_ident(sto, ty)) ->
+      | (id, II_ident(_, ty)) ->
           { edesc = EVar id; etyp = ty }
       | (id, II_enum v) ->
           { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) }
@@ -1249,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
-        | t1, t2 -> error "incorrect types for array subscripting" in
+        | _, _ -> error "incorrect types for array subscripting" in
       { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres }
 
   | MEMBEROF(a1, fieldname) ->
@@ -1302,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(sto, ty)) -> { edesc = EVar id; etyp = ty }
+          | (id, II_ident(_, ty)) -> { edesc = EVar id; etyp = ty }
           | _ -> assert false
       in
       let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in
@@ -1331,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, a) -> (res, args, vararg)
-        | TPtr(ty, a) ->
+        | TFun(res, args, vararg, _) -> (res, args, vararg)
+        | TPtr(ty, _) ->
             begin match unroll env ty with
-            | TFun(res, args, vararg, a) -> (res, args, vararg)
+            | TFun(res, args, vararg, _) -> (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"
@@ -1366,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' }
-      | (ty', None)   -> error "ill-formed compound literal"
+      | (_, None)   -> error "ill-formed compound literal"
       end
 
 (* 6.5.3 Unary expressions *)
@@ -1489,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, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty
-            | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty
+            | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) -> ty
+            | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(ty, _, _)) -> ty
             | _, _ -> error "type error in binary '+'" in
           if not (pointer_arithmetic_ok env ty) then
             err "illegal pointer arithmetic in binary '+'";
@@ -1507,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, a) | TArray(ty, _, a)), (TInt _ | TEnum _) ->
+          | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
               (TPtr(ty, []), TPtr(ty, []))
-          | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) ->
+          | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(ty, _, _)) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
               (TPtr(ty, []), TPtr(ty, []))
-          | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
-            (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
+          | (TPtr(ty1, _) | TArray(ty1, _, _)),
+            (TPtr(ty2, _) | TArray(ty2, _, _)) ->
               if not (compatible_types AttrIgnoreAll env ty1 ty2) then
                 err "mismatch between pointer types in binary '-'";
               if not (pointer_arithmetic_ok env ty1) then
@@ -1587,9 +1585,9 @@ let elab_expr loc env a =
               | Some ty -> ty
             in
           { edesc = EConditional(b1, b2, b3); etyp = tyres }
-      | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
+      | TPtr(ty1, _), TInt _ when is_literal_0 b3 ->
           { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) }
-      | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
+      | TInt _, TPtr(ty2, _) when is_literal_0 b2 ->
           { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) }
       | ty1, ty2 ->
           match combine_types AttrIgnoreAll env ty1 ty2 with
@@ -1727,7 +1725,7 @@ let elab_expr loc env a =
         | (TInt _ | TEnum _), TPtr _ ->
             warning "comparison between integer and pointer";
             EBinop(op, b1, b2, TPtr(TVoid [], []))
-        | ty1, ty2 ->
+        | _, _ ->
             error "illegal comparison between types@ %a@ and %a"
                   Cprint.typ b1.etyp Cprint.typ b2.etyp in
       { edesc = resdesc; etyp = TInt(IInt, []) }
@@ -1797,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 (s',ty') ->
+    | Some (_ ,ty') ->
         if equal_types env ty ty' then begin
           warning loc "redefinition of typedef '%s'" s;
           env
@@ -1848,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 v) when Env.in_current_scope env id ->
+  | Some(id, II_enum _) when Env.in_current_scope env id ->
       error loc "redefinition of enumerator '%s'" s;
       (id, sto, Env.add_ident env id sto ty,ty)
   | _ ->
@@ -1860,7 +1858,7 @@ let enter_decdefs local loc env sto dl =
     fatal_error loc "'register' on global declaration";
   if sto <> Storage_default && dl = [] then
     warning loc "Storage class specifier on empty declaration";
-  let rec enter_decdef (decls, env) (s, ty, init) =
+  let enter_decdef (decls, env) (s, ty, init) =
     let isfun = is_function_type env ty in
     if sto = Storage_extern && init <> NO_INIT then
       error loc "'extern' declaration cannot have an initializer";
@@ -1915,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, dty, attrs, loc') as name, ie)) =
+      let extract_name (Init_name(Name(s, _, _, 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
@@ -1936,7 +1934,7 @@ let elab_fundef env spec name defs body loc =
                       "Illegal declaration of function parameter" in
       let (kr_params_defs, env1) = mmap elab_kr_param_def env1 defs in
       let kr_params_defs = List.concat kr_params_defs in
-      let rec search_param_type param =
+      let search_param_type param =
         match List.filter (fun (p, _) -> p = param) kr_params_defs with
         | [] ->
           (* Parameter is not declared, defaults to "int" in ISO C90,
@@ -1949,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 params -> assert false
+    | _, Some _ -> assert false
   in
   (* Extract info from type *)
   let (ty_ret, params, vararg, attr) =
@@ -1960,7 +1958,7 @@ let elab_fundef env spec name defs body loc =
         (ty_ret, params, vararg, attr)
     | _ -> fatal_error loc "wrong type for function definition" in
   (* Enter function in the environment, for recursive references *)
-  let (fun_id, sto1, env1,ty) = enter_or_refine_ident false loc env1 s sto ty in
+  let (fun_id, sto1, env1, _) = enter_or_refine_ident false loc env1 s sto ty in
   (* Enter parameters in the environment *)
   let env2 =
     List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty)
@@ -2095,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 n -> ()
+        | Some _ -> ()
       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 65df6cb9..9ab5e657 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -118,15 +118,9 @@ let lookup_ident env s =
   with Not_found ->
     raise(Error(Unbound_identifier s))
 
-let lookup_tag env s =
-  try
-    IdentMap.lookup s env.env_tag
-  with Not_found ->
-    raise(Error(Unbound_tag(s, "tag")))
-
 let lookup_struct env s =
   try
-    let (id, ci as res) = IdentMap.lookup s env.env_tag in
+    let (_, ci as res) = IdentMap.lookup s env.env_tag in
     if ci.ci_kind <> Struct then
       raise(Error(Tag_mismatch(s, "struct", "union")));
     res
@@ -135,7 +129,7 @@ let lookup_struct env s =
 
 let lookup_union env s =
   try
-    let (id, ci as res) = IdentMap.lookup s env.env_tag in
+    let (_, ci as res) = IdentMap.lookup s env.env_tag in
     if ci.ci_kind <> Union then
       raise(Error(Tag_mismatch(s, "union", "struct")));
     res
@@ -169,11 +163,6 @@ let find_ident env id =
   with Not_found ->
     raise(Error(Unbound_identifier(id.name)))
 
-let find_tag env id =
-  try IdentMap.find id env.env_tag
-  with Not_found ->
-    raise(Error(Unbound_tag(id.name, "tag")))
-
 let find_struct env id =
   try
     let ci = IdentMap.find id env.env_tag in
@@ -256,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, exp) =
+  let add_enum_item env (id, v, _) =
     { 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 94fcda31..5183df9b 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -33,7 +33,6 @@ open Printf
 open Machine
 open C
 open Cutil
-open Env
 open Cerrors
 
 (* Renaming of labeled and numbered operands *)
@@ -151,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, cstr, e) :: outputs ->
+      | (lbl, _, _) :: 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 bcf2ada0..b2b00e8c 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -17,8 +17,7 @@
 open Lexing
 open Pre_parser
 open Pre_parser_aux
-open Cabshelper
-open Camlcoq
+open !Cabshelper
 
 module SSet = Set.Make(String)
 
@@ -430,7 +429,7 @@ and singleline_comment = parse
   open Streams
   open Specif
   open Parser
-  open Aut.GramDefs
+  open !Aut.GramDefs
 
   (* This is the main entry point to the lexer. *)
 
@@ -578,7 +577,7 @@ and singleline_comment = parse
           let rec doConcat wide str =
             try
               match Queue.peek tokens with
-              | STRING_LITERAL (wide', str', loc) ->
+              | STRING_LITERAL (wide', str', _) ->
                   ignore (Queue.pop tokens);
                   let (wide'', str'') = doConcat wide' str' in
                   if str'' <> []
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 6ea5d121..6a60dfb8 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -127,10 +127,10 @@ let transf_composite loc env su id attrs ml =
 
 (* Accessor functions *)
 
-let lookup_function loc env name =
+let lookup_function env name =
   match Env.lookup_ident env name with
-  | (id, II_ident(sto, ty)) -> (id, ty)
-  | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
+  | (id, II_ident(_, ty)) -> (id, ty)
+  | (_, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
 
 (* Type for the access *)
 
@@ -161,14 +161,14 @@ let bswap_read loc env lval =
   try
     if !use_reversed then begin
       let (id, fty) =
-        lookup_function loc env (sprintf "__builtin_read%d_reversed" bsize) in
+        lookup_function env (sprintf "__builtin_read%d_reversed" bsize) in
       let fn = {edesc = EVar id; etyp = fty} in
       let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lval)] in
       let call = {edesc = ECall(fn, args); etyp = aty} in
       ecast_opt env ty call
     end else begin
       let (id, fty) =
-        lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
+        lookup_function env (sprintf "__builtin_bswap%d" bsize) in
       let fn = {edesc = EVar id; etyp = fty} in
       let args = [ecast_opt env aty lval] in
       let call = {edesc = ECall(fn, args); etyp = aty} in
@@ -188,14 +188,14 @@ let bswap_write loc env lhs rhs =
   try
     if !use_reversed then begin
       let (id, fty) =
-        lookup_function loc env (sprintf "__builtin_write%d_reversed" bsize) in
+        lookup_function env (sprintf "__builtin_write%d_reversed" bsize) in
       let fn = {edesc = EVar id; etyp = fty} in
       let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs);
                   ecast_opt env aty rhs] in
       {edesc = ECall(fn, args); etyp = TVoid[]}
     end else begin
       let (id, fty) =
-        lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
+        lookup_function env (sprintf "__builtin_bswap%d" bsize) in
       let fn = {edesc = EVar id; etyp = fty} in
       let args = [ecast_opt env aty rhs] in
       let call = {edesc = ECall(fn, args); etyp = aty} in
@@ -387,7 +387,7 @@ let rec transf_globdecls env accu = function
   | [] -> List.rev accu
   | g :: gl ->
       match g.gdesc with
-      | Gdecl((sto, id, ty, init) as d) ->
+      | Gdecl((sto, id, ty, _) as d) ->
           transf_globdecls
             (Env.add_ident env id sto ty)
             ({g with gdesc = Gdecl(transf_decl g.gloc env d)} :: accu)
@@ -403,7 +403,7 @@ let rec transf_globdecls env accu = function
             | Union -> attr
             | Struct -> remove_custom_attributes  ["packed";"__packed__"] attr in
           transf_globdecls
-            (Env.add_composite env id (composite_info_decl env su attr'))
+            (Env.add_composite env id (composite_info_decl su attr'))
             ({g with gdesc = Gcompositedecl(su, id, attr')} :: accu)
             gl
       | Gcompositedef(su, id, attr, fl) ->
@@ -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 p ->
+      | Gpragma _ ->
           transf_globdecls env (g :: accu) gl
 
 (* Program *)
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 664f6a28..0d92c514 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 d -> assert false
+  | Sdecl _ -> 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 4e019380..95f133bd 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -19,7 +19,7 @@
 
 open Machine
 open Configuration
-open C
+open !C
 open Cutil
 open Transform
 
@@ -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, sz, al) ->
+      | Ret_value(ty, _, _) ->
           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, sz, al) ->
+      | Ret_value(ty, _, _) ->
           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, sz, al) ->
+      | Param_flattened(n, _, _) ->
           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, a, b, _) -> translates_to_extended_lvalue b
+   | EBinop(Ocomma, _, 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, ty) ->
+  | EBinop(Ocomma, e1, e2, _) ->
       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, sz, al) ->
+      | Ret_value(ty_ret, _, _) ->
           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 lbl -> s
+  | Sgoto _ -> 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, sz, al) ->
+      | Param_flattened(n, _, _) ->
           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, sz, al) ->
+    | Ret_value(ty, _, _) ->
         (f.fd_attrib,
          ty,
          params,
@@ -573,7 +573,7 @@ let transf_fundef env f =
 
 (* Composites *)
 
-let transf_composite env su id attr fl =
+let transf_composite env _ _ 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 id ty -> transf_type env ty)
+    ~typedef:(fun env _ ty -> transf_type env ty)
     p
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 840234b8..685ef7e1 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -45,7 +45,7 @@ let new_temp ?(name = "t") ty =
 
 let attributes_to_remove_from_temp = add_attributes [AConst] [AVolatile]
 
-let mk_temp env ?(name = "t") ty =
+let mk_temp env ty =
   new_temp (remove_attributes_type env attributes_to_remove_from_temp ty)
 
 (* Bind a l-value to a temporary variable if it is not invariant. *)
@@ -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 env decl -> assert false) env s =
+let stmt ~expr ?(decl = fun _ _ -> assert false) env s =
   let rec stm s =
   match s.sdesc with
   | Sskip -> s
@@ -163,7 +163,7 @@ let stmt ~expr ?(decl = fun env decl -> 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 lbl -> s
+  | Sgoto _ -> 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 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)
+    ?(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)
     p =
 
   let rec transf_globdecls env accu = function
@@ -204,14 +204,14 @@ let program
   | g :: gl ->
       let (desc', env') =
         match g.gdesc with
-        | Gdecl((sto, id, ty, init) as d) ->
+        | Gdecl((sto, id, ty, _) as d) ->
            (Gdecl(decl env d), Env.add_ident env id sto ty)
         | Gfundef f ->
            (Gfundef(fundef env f),
             Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
         | Gcompositedecl(su, id, attr) ->
             (Gcompositedecl(su, id, attr),
-             Env.add_composite env id (composite_info_decl env su attr))
+             Env.add_composite env id (composite_info_decl su attr))
         | Gcompositedef(su, id, attr, fl) ->
             let (attr', fl') = composite env su id attr fl in
             (Gcompositedef(su, id, attr', fl'),
diff --git a/cparser/Transform.mli b/cparser/Transform.mli
index a04896a9..dbd8e575 100644
--- a/cparser/Transform.mli
+++ b/cparser/Transform.mli
@@ -18,7 +18,7 @@ val reset_temps : unit -> unit
 val get_temps : unit -> C.decl list
 val new_temp_var : ?name:string -> C.typ -> C.ident
 val new_temp : ?name:string -> C.typ -> C.exp
-val mk_temp : Env.t -> ?name:string -> C.typ -> C.exp
+val mk_temp : Env.t -> C.typ -> C.exp
 
 (** Avoiding repeated evaluation of a l-value *)
 
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index ef8bc91c..eaf49164 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(id, fil) ->
+  | Init_struct(_, 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(id, fld, i) ->
+  | Init_union(_, fld, i) ->
       local_initializer env
         { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
         i k
@@ -64,17 +64,6 @@ let add_inits_stmt loc inits s =
     (fun e s -> sseq loc {sdesc = Sdo e; sloc = loc} s)
     inits s
 
-(* Prepend assignments to the given expression. *)
-(* Associate to the left so that it prints more nicely *)
-
-let add_inits_expr inits e =
-  match inits with
-  | [] -> e
-  | i1 :: il ->
-      let comma a b =
-        { edesc = EBinop(Ocomma, a, b, b.etyp); etyp = b.etyp } in
-      comma (List.fold_left comma i1 il) e
-
 (* Record new variables to be locally or globally defined *)
 
 let local_variables = ref ([]: decl list)
@@ -304,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 lbl ->
+  | Sgoto _ ->
       add_lineno ctx ploc s.sloc s
   | Sreturn None ->
       add_lineno ctx ploc s.sloc s
@@ -322,7 +311,7 @@ let rec unblock_stmt env ctx ploc s =
           id:: ctx
         else ctx in
       unblock_block env ctx' ploc sl
-  | Sdecl d ->
+  | Sdecl _ ->
       assert false
   | Sasm(attr, template, outputs, inputs, clob) ->
       let expand_asm_operand (lbl, cstr, e) =
@@ -357,7 +346,7 @@ let unblock_fundef env f =
 
 (* Simplification of compound literals within a top-level declaration *)
 
-let unblock_decl loc env ((sto, id, ty, optinit) as d) =
+let unblock_decl env ((sto, id, ty, optinit) as d) =
   match optinit with
   | None -> [d]
   | Some init ->
@@ -375,8 +364,8 @@ let rec unblock_glob env accu = function
   | [] -> List.rev accu
   | g :: gl ->
       match g.gdesc with
-      | Gdecl((sto, id, ty, init) as d) ->
-          let dl = unblock_decl g.gloc env d in
+      | Gdecl d ->
+          let dl = unblock_decl env d in
           unblock_glob env
             (List.rev_append
                (List.map (fun d' -> {g with gdesc = Gdecl d'}) dl)
@@ -387,7 +376,7 @@ let rec unblock_glob env accu = function
           unblock_glob env ({g with gdesc = Gfundef f'} :: accu) gl
       | Gcompositedecl(su, id, attr) ->
           unblock_glob
-            (Env.add_composite env id (composite_info_decl env su attr))
+            (Env.add_composite env id (composite_info_decl su attr))
             (g :: accu) gl
       | Gcompositedef(su, id, attr, fl) ->
           unblock_glob