From fbaeaaec35da748db98a3cf9e405024024561426 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 19 Apr 2016 17:14:50 +0200
Subject: Moved some system functions into own module.

The process handling is now in its own file, like the output name
generation etc.
Bug 18768
---
 driver/Driver.ml | 69 +-------------------------------------------------------
 1 file changed, 1 insertion(+), 68 deletions(-)

(limited to 'driver/Driver.ml')

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 567ff018..0cacae13 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -15,6 +15,7 @@ open Commandline
 open Camlcoq
 open Clflags
 open Timing
+open Sysaux
 
 (* Location of the compatibility library *)
 
@@ -28,49 +29,6 @@ let dump_options = ref false
 (* Optional sdump suffix *)
 let sdump_suffix = ref ".json"
 
-(* Invocation of external tools *)
-
-let rec waitpid_no_intr pid =
-  try Unix.waitpid [] pid
-  with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid
-
-let command ?stdout args =
-  if !option_v then begin
-    eprintf "+ %s" (String.concat " " args);
-    begin match stdout with
-    | None -> ()
-    | Some f -> eprintf " > %s" f
-    end;
-    prerr_endline ""
-  end;
-  let argv = Array.of_list args in
-  assert (Array.length argv > 0);
-  try
-    let fd_out =
-      match stdout with
-      | None -> Unix.stdout
-      | Some f ->
-          Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
-    let pid =
-      Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
-    let (_, status) =
-      waitpid_no_intr pid in
-    if stdout <> None then Unix.close fd_out;
-    match status with
-    | Unix.WEXITED rc -> rc
-    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        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"
-            argv.(0) fn (Unix.error_message err) param;
-    -1
-
-let command_error n exc =
-  eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc
-
-let safe_remove file =
-  try Sys.remove file with Sys_error _ -> ()
-
 (* Printing of error messages *)
 
 let print_error oc msg =
@@ -82,24 +40,6 @@ let print_error oc msg =
     List.iter print_one_error msg;
     output_char oc '\n'
 
-(* Determine names for output files.  We use -o option if specified
-   and if this is the final destination file (not a dump file).
-   Otherwise, we generate a file in the current directory. *)
-
-let output_filename ?(final = false) source_file source_suffix output_suffix =
-  match !option_o with
-  | Some file when final -> file
-  | _ ->
-    Filename.basename (Filename.chop_suffix source_file source_suffix)
-    ^ output_suffix
-
-(* A variant of [output_filename] where the default output name is fixed *)
-
-let output_filename_default default_file =
-  match !option_o with
-  | Some file -> file
-  | None -> default_file
-
 (* From C to preprocessed C *)
 
 let preprocess ifile ofile =
@@ -280,13 +220,6 @@ let linker exe_name files =
     exit 2
   end
 
-(* All input files should exist *)
-
-let ensure_inputfile_exists name =
-  if not (Sys.file_exists name) then begin
-    eprintf "error: no such file or directory: '%s'\n" name;
-    exit 2
-  end
 
 (* Processing of a .c file *)
 
-- 
cgit