1 files changed, 0 insertions, 91 deletions
diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml
deleted file mode 100644
index 3834f8e6..00000000
--- a/backend/Unusedglob.ml
+++ /dev/null
@@ -1,91 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Removing unused definitions of static functions and global variables *)
-
-open Camlcoq
-open Maps
-open AST
-open Asm
-open Unusedglob1
-
-module IdentSet = Set.Make(struct type t = ident let compare = compare end)
-
-(* The set of globals referenced from a function definition *)
-
-let add_referenced_instr rf i =
-  List.fold_right IdentSet.add (referenced_instr i) rf
-
-let referenced_function f =
-  List.fold_left add_referenced_instr IdentSet.empty (code_of_function f)
-
-(* The set of globals referenced from a variable definition (initialization) *)
-
-let add_referenced_init_data rf = function
-  | Init_addrof(id, ofs) -> IdentSet.add id rf
-  | _ -> rf
-
-let referenced_globvar gv =
-  List.fold_left add_referenced_init_data IdentSet.empty gv.gvar_init
-
-(* The map global |-> set of globals it references *)
-
-let referenced_globdef gd =
-  match gd with
-  | Gfun(Internal f) -> referenced_function f
-  | Gfun(External ef) -> IdentSet.empty
-  | Gvar gv -> referenced_globvar gv
-
-let use_map p =
-  List.fold_left (fun m (id, gd) -> PTree.set id (referenced_globdef gd) m)
-    PTree.empty p.prog_defs
-
-(* Worklist algorithm computing the set of used globals *)
-
-let rec used_idents usemap used wrk =
-  match wrk with
-  | [] -> used
-  | id :: wrk ->
-      if IdentSet.mem id used then used_idents usemap used wrk else
-        match PTree.get id usemap with
-        | None -> used_idents usemap used wrk
-        | Some s -> used_idents usemap (IdentSet.add id used)
-                                       (IdentSet.fold (fun id l -> id::l) s wrk)
-
-(* The worklist is initially populated with all nonstatic globals *)
-
-let add_nonstatic wrk id =
-  if C2C.atom_is_static id then wrk else id :: wrk
-
-let initial_worklist p =
-  List.fold_left (fun wrk (id, gd) -> add_nonstatic wrk id)
-    [] p.prog_defs
-
-(* Eliminate unused definitions *)
-
-let rec filter used = function
-  | [] -> []
-  | (id, def) :: rem ->
-      if IdentSet.mem id used
-      then (id, def) :: filter used rem
-      else filter used rem
-
-let filter_prog used p =
-  { prog_defs = filter used p.prog_defs;
-    prog_public = p.prog_public;
-    prog_main = p.prog_main }
-
-(* Entry point *)
-
-let transf_program p =
-  filter_prog (used_idents (use_map p) IdentSet.empty (initial_worklist p)) p
-