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.

3 files changed, 68 insertions, 60 deletions

diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index 1d048ac4..abfd3ab4 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -12,27 +12,37 @@
 
 val arch: string
   (** Target architecture *)
+
 val model: string
   (** Sub-model for this architecture *)
+
 val abi: string
   (** ABI to use *)
+
 val system: string
   (** Flavor of operating system that runs CompCert *)
 
 val prepro: string list
   (** How to invoke the external preprocessor *)
+
 val asm: string list
   (** How to invoke the external assembler *)
+
 val linker: string list
   (** How to invoke the external linker *)
+
 val asm_supports_cfi: bool
   (** True if the assembler supports Call Frame Information *)
+
 val stdlib_path: string
   (** Path to CompCert's library *)
+
 val has_runtime_lib: bool
   (** True if CompCert's library is available. *)
+
 val has_standard_headers: bool
   (** True if CompCert's standard header files is available. *)
+
 val advanced_debug: bool
   (** True if advanced debug is implement for the Target *)
 
@@ -52,6 +62,7 @@ type struct_return_style =
 val struct_passing_style: struct_passing_style
   (** Calling conventions to use for passing structs and unions as
       first-class values *)
+
 val struct_return_style: struct_return_style
   (** Calling conventions to use for returning structs and unions as
       first-class values *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index bbd949e0..7b245e6e 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -58,7 +58,7 @@ let command ?stdout args =
     if stdout <> None then Unix.close fd_out;
     match status with
     | Unix.WEXITED rc -> rc
-    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+    | Unix.WSIGNALED _ | Unix.WSTOPPED _ ->
         eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
   with Unix.Unix_error(err, fn, param) ->
     eprintf "Error executing '%s': %s: %s %s\n"
@@ -159,7 +159,7 @@ let parse_c_file sourcename ifile =
     PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     close_out oc
   end;
-  csyntax,None
+  csyntax
 
 (* Dump Asm code in asm format for the validator *)
 
@@ -174,7 +174,7 @@ let dump_jasm asm sourcename destfile =
 
 (* From CompCert C AST to asm *)
 
-let compile_c_ast sourcename csyntax ofile debug =
+let compile_c_ast sourcename csyntax ofile =
   (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
     dst := if !opt then Some (output_filename sourcename ".c" ext)
@@ -200,14 +200,14 @@ let compile_c_ast sourcename csyntax ofile debug =
       dump_jasm asm sourcename (output_filename sourcename ".c" !sdump_suffix);
   (* Print Asm in text form *)
   let oc = open_out ofile in
-  PrintAsm.print_program oc asm debug;
+  PrintAsm.print_program oc asm;
   close_out oc
 
 (* From C source to asm *)
 
 let compile_c_file sourcename ifile ofile =
-  let ast,debug = parse_c_file sourcename ifile in
-  compile_c_ast sourcename ast ofile debug
+  let ast = parse_c_file sourcename ifile in
+  compile_c_ast sourcename ast ofile
 
 (* From Cminor to asm *)
 
@@ -232,7 +232,7 @@ let compile_cminor_file ifile ofile =
         exit 2
     | Errors.OK p ->
         let oc = open_out ofile in
-        PrintAsm.print_program oc p None;
+        PrintAsm.print_program oc p;
         close_out oc
   with Parsing.Parse_error ->
          eprintf "File %s, character %d: Syntax error\n"
@@ -304,7 +304,7 @@ let process_c_file sourcename =
     let name =
       if !option_interp then begin
         Machine.config := Machine.compcert_interpreter !Machine.config;
-        let csyntax,_ = parse_c_file sourcename preproname in
+        let csyntax = parse_c_file sourcename preproname in
         if not !option_dprepro then
           safe_remove preproname;
        Interp.execute csyntax;
@@ -338,7 +338,7 @@ let process_c_file sourcename =
 let process_i_file sourcename =
   ensure_inputfile_exists sourcename;
   if !option_interp then begin
-    let csyntax,_ = parse_c_file sourcename sourcename in
+    let csyntax = parse_c_file sourcename sourcename in
     Interp.execute csyntax;
     ""
   end else if !option_S then begin
@@ -438,7 +438,7 @@ let perform_actions () =
 let explode_comma_option s =
   match Str.split (Str.regexp ",") s with
   | [] -> assert false
-  | hd :: tl -> tl
+  | _ :: tl -> tl
 
 let version_string =
   if Version.buildnr <> "" && Version.tag <> "" then
@@ -681,13 +681,13 @@ let cmdline_actions =
   Exact "-fall", Self (fun _ -> set_all language_support_options);
   Exact "-fnone", Self (fun _ -> unset_all language_support_options);
 (* Debugging options *)
-  Exact "-g", Self (fun s -> option_g := true;
+  Exact "-g", Self (fun _ -> option_g := true;
     option_gdwarf := 3);
-  Exact "-gdwarf-2", Self (fun s -> option_g:=true;
+  Exact "-gdwarf-2", Self (fun _ -> option_g:=true;
     option_gdwarf := 2);
-  Exact "-gdwarf-3", Self (fun s -> option_g := true;
+  Exact "-gdwarf-3", Self (fun _ -> option_g := true;
     option_gdwarf := 3);
-  Exact "-frename-static", Self (fun s -> option_rename_static:= true);
+  Exact "-frename-static", Self (fun _ -> option_rename_static:= true);
    Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin
      option_g := false
    end else begin
diff --git a/driver/Interp.ml b/driver/Interp.ml
index fb1c85f0..8dd4a7c9 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -12,20 +12,17 @@
 
 (* Interpreting CompCert C sources *)
 
-open Format
+open !Format
 open Camlcoq
-open Datatypes
 open AST
 open Integers
 open Values
 open Memory
 open Globalenvs
 open Events
-open Ctypes
-open Cop
-open Csyntax
+open !Ctypes
+open !Csyntax
 open Csem
-open Clflags
 
 (* Configuration *)
 
@@ -84,18 +81,18 @@ let name_of_fundef prog fd =
   | [] -> "<unknown function>"
   | (id, Gfun fd') :: rem ->
       if fd == fd' then extern_atom id else find_name rem
-  | (id, Gvar v) :: rem ->
+  | (_, Gvar _) :: rem ->
       find_name rem
-  in find_name prog.prog_defs
+  in find_name prog.Csyntax.prog_defs
 
 let name_of_function prog fn =
   let rec find_name = function
   | [] -> "<unknown function>"
-  | (id, Gfun(Internal fn')) :: rem ->
+  | (id, Gfun(Csyntax.Internal fn')) :: rem ->
       if fn == fn' then extern_atom id else find_name rem
-  | (id, _) :: rem ->
+  | _ :: rem ->
       find_name rem
-  in find_name prog.prog_defs
+  in find_name prog.Csyntax.prog_defs
 
 let invert_local_variable e b =
   Maps.PTree.fold
@@ -121,22 +118,22 @@ let print_val_list p vl =
 
 let print_state p (prog, ge, s) =
   match s with
-  | State(f, s, k, e, m) ->
+  | State(f, s, _, e, _) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "in function %s, statement@ @[<hv 0>%a@]"
               (name_of_function prog f)
               PrintCsyntax.print_stmt s
-  | ExprState(f, r, k, e, m) ->
+  | ExprState(f, r, _, e, _) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "in function %s, expression@ @[<hv 0>%a@]"
               (name_of_function prog f)
               PrintCsyntax.print_expr r
-  | Callstate(fd, args, k, m) ->
+  | Callstate(fd, args, _, _) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty;
       fprintf p "calling@ @[<hov 2>%s(%a)@]"
               (name_of_fundef prog fd)
               print_val_list args
-  | Returnstate(res, k, m) ->
+  | Returnstate(res, _, _) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty;
       fprintf p "returning@ %a"
               print_val res
@@ -223,10 +220,10 @@ let rank_state = function
   | Stuckstate -> assert false
 
 let mem_state = function
-  | State(f, s, k, e, m) -> m
-  | ExprState(f, r, k, e, m) -> m
-  | Callstate(fd, args, k, m) -> m
-  | Returnstate(res, k, m) -> m
+  | State(_, _, _, _, m) -> m
+  | ExprState(_, _, _, _, m) -> m
+  | Callstate(_, _, _, m) -> m
+  | Returnstate(_, _, m) -> m
   | Stuckstate -> assert false
 
 let compare_state s1 s2 =
@@ -397,14 +394,14 @@ let do_external_function id sg ge w args m =
   | _ ->
       None
 
-let do_inline_assembly txt sg ge w args m = None
+let do_inline_assembly _ _ _ _ _ _ = None
 
 (* Implementing external functions producing observable events *)
 
 let rec world ge m =
   lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m))
 
-and world_io ge m id args =
+and world_io _ _ _ _ =
   None
 
 and world_vload ge m chunk id ofs =
@@ -419,7 +416,7 @@ and world_vstore ge m chunk id ofs ev =
   Mem.store chunk m b ofs v >>= fun m' ->
   Some(world ge m')
 
-let do_event p ge time w ev =
+let do_event p _ time w ev =
   if !trace >= 1 then
     fprintf p "@[<hov 2>Time %d: observable event:@ %a@]@."
               time print_event ev;
@@ -441,30 +438,30 @@ let rec do_events p ge time w t =
 
 let (|||) a b = a || b (* strict boolean or *)
 
-let diagnose_stuck_expr p ge w f a kont e m =
+let diagnose_stuck_expr p ge w _ a _ e m =
   let rec diagnose k a =
   (* diagnose subexpressions first *)
   let found =
     match k, a with
-    | LV, Ederef(r, ty) -> diagnose RV r
-    | LV, Efield(r, f, ty) -> diagnose RV r
-    | RV, Evalof(l, ty) -> diagnose LV l
-    | RV, Eaddrof(l, ty) -> diagnose LV l
-    | RV, Eunop(op, r1, ty) -> diagnose RV r1
-    | RV, Ebinop(op, r1, r2, ty) -> diagnose RV r1 ||| diagnose RV r2
-    | RV, Ecast(r1, ty) -> diagnose RV r1
-    | RV, Econdition(r1, r2, r3, ty) -> diagnose RV r1
-    | RV, Eassign(l1, r2, ty) -> diagnose LV l1 ||| diagnose RV r2
-    | RV, Eassignop(op, l1, r2, tyres, ty) -> diagnose LV l1 ||| diagnose RV r2
-    | RV, Epostincr(id, l, ty) -> diagnose LV l
-    | RV, Ecomma(r1, r2, ty) -> diagnose RV r1
-    | RV, Eparen(r1, tycast, ty) -> diagnose RV r1
-    | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs
-    | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs
+    | LV, Ederef(r, _) -> diagnose RV r
+    | LV, Efield(r, _, _) -> diagnose RV r
+    | RV, Evalof(l, _) -> diagnose LV l
+    | RV, Eaddrof(l, _) -> diagnose LV l
+    | RV, Eunop(_, r1, _) -> diagnose RV r1
+    | RV, Ebinop(_, r1, r2, _) -> diagnose RV r1 ||| diagnose RV r2
+    | RV, Ecast(r1, _) -> diagnose RV r1
+    | RV, Econdition(r1, _, _, _) -> diagnose RV r1
+    | RV, Eassign(l1, r2, _) -> diagnose LV l1 ||| diagnose RV r2
+    | RV, Eassignop(_, l1, r2, _, _) -> diagnose LV l1 ||| diagnose RV r2
+    | RV, Epostincr(_, l, _) -> diagnose LV l
+    | RV, Ecomma(r1, _, _) -> diagnose RV r1
+    | RV, Eparen(r1, _, _) -> diagnose RV r1
+    | RV, Ecall(r1, rargs, _) -> diagnose RV r1 ||| diagnose_list rargs
+    | RV, Ebuiltin(_, _, rargs, _) -> diagnose_list rargs
     | _, _ -> false in
   if found then true else begin
     let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in
-    if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin
+    if List.exists (fun (_,red) -> red = Cexec.Stuckred) l then begin
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@."
               PrintCsyntax.print_expr a;
@@ -499,7 +496,7 @@ let do_step p prog ge time s w =
   | None ->
       let l = Cexec.do_step ge do_external_function do_inline_assembly w s in
       if l = []
-      || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l
+      || List.exists (fun (Cexec.TR(_,_,s)) -> s = Stuckstate) l
       then begin
         pp_set_max_boxes p 1000;
         fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s);
@@ -532,7 +529,7 @@ let rec explore_one p prog ge time s w =
 let rec explore_all p prog ge time states =
   if !trace >= 2 then begin
     List.iter
-      (fun (n, s, w) ->
+      (fun (n, s, _) ->
          fprintf p "@[<hov 2>State %d.%d: @ %a@]@."
                    time n print_state (prog, ge, s))
       states
@@ -582,9 +579,9 @@ let world_program prog =
           else
             {gv with gvar_init = []} in
         (id, Gvar gv')
-    | Gfun fd ->
+    | Gfun _ ->
         (id, gd) in
- {prog with prog_defs = List.map change_def prog.prog_defs}
+ {prog with Csyntax.prog_defs = List.map change_def prog.Csyntax.prog_defs}
 
 (* Massaging the program to get a suitable "main" function *)
 
@@ -599,7 +596,7 @@ let change_main_function p old_main old_main_ty =
       fn_params = []; fn_vars = []; fn_body = body } in
   let new_main_id = intern_string "___main" in
   { prog_main = new_main_id;
-    prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs;
+    Csyntax.prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.Csyntax.prog_defs;
     prog_public = p.prog_public;
     prog_types = p.prog_types;
     prog_comp_env = p.prog_comp_env }
@@ -607,10 +604,10 @@ let change_main_function p old_main old_main_ty =
 let rec find_main_function name = function
   | [] -> None
   | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl
-  | (id, Gvar v) :: gdl -> find_main_function name gdl
+  | (_, Gvar _) :: gdl -> find_main_function name gdl
 
 let fixup_main p =
-  match find_main_function p.prog_main p.prog_defs with
+  match find_main_function p.Csyntax.prog_main p.prog_defs with
   | None ->
       fprintf err_formatter "ERROR: no main() function@.";
       None