From 7247e4bb85d50834983bc71e6415fe1bf065aa46 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 10 Mar 2016 19:17:24 +0100 Subject: Cleanup of Clightgen code. Removed unused code and code generating warnings. Bug 18394 --- exportclight/Clightgen.ml | 5 ++- exportclight/ExportClight.ml | 81 +++++++++++++++++++++----------------------- 2 files changed, 41 insertions(+), 45 deletions(-) (limited to 'exportclight') diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index a5d48a3f..ccdaabc4 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -47,7 +47,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" @@ -186,7 +186,7 @@ let process_c_file sourcename = let explode_comma_option s = match Str.split (Str.regexp ",") s with | [] -> assert false - | hd :: tl -> tl + | _ :: tl -> tl let usage_string = "The CompCert Clight generator @@ -293,4 +293,3 @@ let _ = Builtins.set C2C.builtins; CPragmas.initialize(); parse_cmdline cmdline_actions - diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 5d4ab88b..4ae6f1f5 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -17,12 +17,10 @@ open Format open Camlcoq -open Datatypes -open Values open AST -open Ctypes +open !Ctypes open Cop -open Clight +open !Clight (* Options, lists, pairs *) @@ -37,7 +35,7 @@ let print_list fn p l = match l with | [] -> fprintf p "nil" - | hd :: tl -> + | _ :: _ -> fprintf p "@[("; let rec plist = function | [] -> fprintf p "nil" @@ -50,15 +48,15 @@ let print_list fn p l = exception Not_an_identifier let sanitize s = - let s' = String.create (String.length s) in + let s' = Bytes.create (String.length s) in for i = 0 to String.length s - 1 do - s'.[i] <- - match s.[i] with + Bytes.set s' i + (match String.get s i with | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c | ' ' | '$' -> '_' - | _ -> raise Not_an_identifier + | _ -> raise Not_an_identifier) done; - s' + Bytes.to_string s' let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17 @@ -75,11 +73,11 @@ let ident p id = let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) = List.iter f - (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2) + (List.fast_sort (fun (_, d1) (_, d2) -> String.compare d1 d2) (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h [])) let define_idents p = - iter_hashtbl_sorted + iter_hashtbl_sorted string_of_atom (fun (id, name) -> try @@ -400,17 +398,17 @@ let print_variable p (id, v) = let print_globdef p (id, gd) = match gd with - | Gfun(Internal f) -> print_function p (id, f) - | Gfun(External _) -> () + | Gfun(Clight.Internal f) -> print_function p (id, f) + | Gfun(Clight.External _) -> () | Gvar v -> print_variable p (id, v) let print_ident_globdef p = function - | (id, Gfun(Internal f)) -> + | (id, Gfun(Clight.Internal _)) -> fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id) - | (id, Gfun(External(ef, targs, tres, cc))) -> + | (id, Gfun(Clight.External(ef, targs, tres, cc))) -> fprintf p "@[(%a,@ @[Gfun(External %a@ %a@ %a@ %a))@]@]" ident id external_function ef typlist targs typ tres callconv cc - | (id, Gvar v) -> + | (id, Gvar _) -> fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id) (* Composite definitions *) @@ -451,7 +449,7 @@ let print_assertion p (txt, targs) = frags; fprintf p " | \"%s\"%%string, " txt; list_iteri - (fun i targ -> fprintf p "_x%d :: " (i + 1)) + (fun i _ -> fprintf p "_x%d :: " (i + 1)) targs; fprintf p "nil =>@ "; fprintf p " "; @@ -483,20 +481,20 @@ Local Open Scope Z_scope. (* Naming the compiler-generated temporaries occurring in the program *) let rec name_expr = function - | Evar(id, t) -> () - | Etempvar(id, t) -> name_temporary id - | Ederef(a1, t) -> name_expr a1 - | Efield(a1, f, t) -> name_expr a1 - | Econst_int(n, t) -> () - | Econst_float(n, t) -> () - | Econst_long(n, t) -> () - | Econst_single(n, t) -> () - | Eunop(op, a1, t) -> name_expr a1 - | Eaddrof(a1, t) -> name_expr a1 - | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2 - | Ecast(a1, t) -> name_expr a1 - | Esizeof(t1, t) -> () - | Ealignof(t1, t) -> () + | Evar _ -> () + | Etempvar(id, _) -> name_temporary id + | Ederef(a1, _) -> name_expr a1 + | Efield(a1, _, _) -> name_expr a1 + | Econst_int _ -> () + | Econst_float _ -> () + | Econst_long _ -> () + | Econst_single _ -> () + | Eunop(_, a1, _) -> name_expr a1 + | Eaddrof(a1, _) -> name_expr a1 + | Ebinop(_, a1, a2, _) -> name_expr a1; name_expr a2 + | Ecast(a1, _) -> name_expr a1 + | Esizeof _ -> () + | Ealignof _ -> () let rec name_stmt = function | Sskip -> () @@ -504,7 +502,7 @@ let rec name_stmt = function | Sset(id, e2) -> name_temporary id; name_expr e2 | Scall(optid, e1, el) -> name_opt_temporary optid; name_expr e1; List.iter name_expr el - | Sbuiltin(optid, ef, tyl, el) -> + | Sbuiltin(optid, _, _, el) -> name_opt_temporary optid; List.iter name_expr el | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2 | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2 @@ -514,25 +512,25 @@ let rec name_stmt = function | Sswitch(e, cases) -> name_expr e; name_lblstmts cases | Sreturn (Some e) -> name_expr e | Sreturn None -> () - | Slabel(lbl, s1) -> name_stmt s1 - | Sgoto lbl -> () + | Slabel(_, s1) -> name_stmt s1 + | Sgoto _ -> () and name_lblstmts = function | LSnil -> () - | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls + | LScons(_, s, ls) -> name_stmt s; name_lblstmts ls let name_function f = - List.iter (fun (id, ty) -> name_temporary id) f.fn_temps; + List.iter (fun (id, _) -> name_temporary id) f.fn_temps; name_stmt f.fn_body -let name_globdef (id, g) = +let name_globdef (_, g) = match g with - | Gfun(Internal f) -> name_function f + | Gfun(Clight.Internal f) -> name_function f | _ -> () let name_program p = - List.iter name_globdef p.prog_defs - + List.iter name_globdef p.Clight.prog_defs + (* All together *) let print_program p prog = @@ -555,4 +553,3 @@ let print_program p prog = fprintf p "|}.@ "; print_assertions p; fprintf p "@]@." - -- cgit