1 files changed, 0 insertions, 85 deletions
diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml
deleted file mode 100644
index 2f2333fb..00000000
--- a/caml/Linearizeaux.ml
+++ /dev/null
@@ -1,85 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open BinPos
-open Coqlib
-open Datatypes
-open LTL
-open Lattice
-open CList
-open Maps
-open Camlcoq
-
-(* Trivial enumeration, in decreasing order of PC *)
-
-(***
-let enumerate_aux f reach =
-  positive_rec
-    Coq_nil
-    (fun pc nodes ->
-      if PMap.get pc reach
-      then Coq_cons (pc, nodes)
-      else nodes) 
-    f.fn_nextpc
-***)
-
-(* More clever enumeration that flattens basic blocks *)
-
-let rec int_of_pos = function
-  | Coq_xI p -> (int_of_pos p lsl 1) + 1
-  | Coq_xO p -> int_of_pos p lsl 1
-  | Coq_xH -> 1
-
-let rec pos_of_int n =
-  if n = 0 then assert false else
-  if n = 1 then Coq_xH else
-  if n land 1 = 0
-  then Coq_xO (pos_of_int (n lsr 1))
-  else Coq_xI (pos_of_int (n lsr 1))
-
-(* Build the enumeration *)
-
-module IntSet = Set.Make(struct type t = int let compare = compare end)
-
-let enumerate_aux f reach =
-  let enum = ref [] in
-  let emitted = Array.make (int_of_pos f.fn_nextpc) false in
-  let rec emit_block pending pc =
-    let npc = int_of_pos pc in
-    if emitted.(npc)
-    then emit_restart pending
-    else begin
-      enum := pc :: !enum;
-      emitted.(npc) <- true;
-      match PTree.get pc f.fn_code with
-      | None -> assert false
-      | Some i ->
-         match i with
-           | Lnop s -> emit_block pending s
-           | Lop (op, args, res, s) -> emit_block pending s
-           | Lload (chunk, addr, args, dst, s) -> emit_block pending s
-           | Lstore (chunk, addr, args, src, s) -> emit_block pending s
-           | Lcall (sig0, ros, args, res, s) -> emit_block pending s
-           | Ltailcall (sig0, ros, args) -> emit_restart pending
-           | Lalloc (arg, res, s) -> emit_block pending s
-           | Lcond (cond, args, ifso, ifnot) ->
-               emit_restart (IntSet.add (int_of_pos ifso)
-                             (IntSet.add (int_of_pos ifnot) pending))
-           | Lreturn optarg -> emit_restart pending
-    end
-  and emit_restart pending =
-    if not (IntSet.is_empty pending) then begin
-      let npc = IntSet.max_elt pending in
-      emit_block (IntSet.remove npc pending) (pos_of_int npc)
-    end in
-  emit_block IntSet.empty f.fn_entrypoint;
-  CList.rev !enum