1 files changed, 0 insertions, 121 deletions
diff --git a/driver/Interp_ext.ml b/driver/Interp_ext.ml
deleted file mode 100644
index 2fc12b87..00000000
--- a/driver/Interp_ext.ml
+++ /dev/null
@@ -1,121 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Implementing external functions for the reference interpreter.
-   The only such function currently implemented is "printf". *)
-
-open Format
-open Camlcoq
-open AST
-open Values
-open Memory
-
-(* Extract a string from a global pointer *)
-
-let extract_string m blk ofs =
-  let b = Buffer.create 80 in
-  let rec extract blk ofs =
-    match Mem.load Mint8unsigned m blk ofs with
-    | Some(Vint n) ->
-        let c = Char.chr (Z.to_int n) in
-        if c = '\000' then begin
-          Some(Buffer.contents b)
-        end else begin
-          Buffer.add_char b c; 
-          extract blk (Z.succ ofs)
-        end
-    | _ ->
-        None in
-  extract blk ofs
-
-(* Emulation of printf *)
-
-(* All ISO C 99 formats except size modifier [L] (long double) *)
-
-let re_conversion = Str.regexp
-  "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\|ll\\)?\\([aAcdeEfgGinopsuxX%]\\)"
-
-external format_float: string -> float -> string
-  = "caml_format_float"
-external format_int32: string -> int32 -> string
-  = "caml_int32_format"
-external format_int64: string -> int64 -> string
-  = "caml_int64_format"
-
-let do_printf m fmt args =
-
-  let b = Buffer.create 80 in
-  let len = String.length fmt in
-
-  let opt_search_forward pos =
-    try Some(Str.search_forward re_conversion fmt pos)
-    with Not_found -> None in
-
-  let rec scan pos args =
-    if pos < len then begin
-    match opt_search_forward pos with
-    | None ->
-        Buffer.add_substring b fmt pos (len - pos)
-    | Some pos1 ->
-        Buffer.add_substring b fmt pos (pos1 - pos);
-        let pat = Str.matched_string fmt
-        and conv = Str.matched_group 3 fmt
-        and pos' = Str.match_end() in
-        match args, conv.[0] with
-        | _, '%' ->
-            Buffer.add_char b '%';
-            scan pos' args
-        | [], _ ->
-            Buffer.add_string b "<missing argument>";
-            scan pos' []
-        | Vint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') ->
-            Buffer.add_string b (format_int32 pat (camlint_of_coqint i));
-            scan pos' args'
-        | Vfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') ->
-            Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f));
-            scan pos' args'
-        | Vlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') ->
-            let pat = Str.replace_first (Str.regexp "ll") "" pat in
-            Buffer.add_string b (format_int64 pat (camlint64_of_coqint i));
-            scan pos' args'
-        | Vptr(blk, ofs) :: args', 's' ->
-            Buffer.add_string b
-              (match extract_string m blk ofs with
-               | Some s -> s
-               | None -> "<bad string>");
-            scan pos' args'
-        | Vptr(blk, ofs) :: args', 'p' ->
-            Printf.bprintf b "<%ld%+ld>" (P.to_int32 blk) (camlint_of_coqint ofs);
-            scan pos' args'
-        | _ :: args', _ ->
-            Buffer.add_string b "<formatting error>";
-            scan pos' args'
-    end
-  in scan 0 args; Buffer.contents b
-
-(* Implementation of external functions *)
-
-let re_stub = Str.regexp "\\$[ifl]*$"
-
-let chop_stub name = Str.replace_first re_stub "" name
-
-let do_external_function id sg args m =
-  match chop_stub(extern_atom id), args with
-  | "printf", Vptr(b, ofs) :: args' ->
-      begin match extract_string m b ofs with
-      | Some fmt -> print_string (do_printf m fmt args')
-      | None     -> print_string "<bad printf>\n"
-      end;
-      flush stdout;
-      Some Vundef
-  | _ ->
-      None