Moved shared frontend code in own file.

Clightgen and CompCert share the code for preprocessing as well as
parsing C files. The code as well as command line switches is moved
in the new module Frontend.
Bug 18768

1 files changed, 43 insertions, 0 deletions

diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli
new file mode 100644
index 00000000..539b1797
--- /dev/null
+++ b/driver/Driveraux.mli
@@ -0,0 +1,43 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*      Bernhard Schommer, AbsInt Angewandte Informatik GmbH           *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+
+val command: ?stdout:string  -> string list -> int
+    (** Execute the command with the given arguments and an optional file for
+        the stdout. Returns the exit code. *)
+
+val command_error: string -> int -> unit
+   (** Generate an error message for the given command and exit code *)
+
+val safe_remove: string -> unit
+   (** Remove the given file if it exists *)
+
+val output_filename: ?final:bool -> string -> string -> string -> string
+   (** 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. *)
+
+val output_filename_default: string -> string
+   (** Return either the file specified by -o or the given file name *)
+
+val ensure_inputfile_exists: string -> unit
+   (** Test whether the given input file exists *)
+
+val print_error:out_channel -> Errors.errcode list -> unit
+   (** Printing of error messages *)
+
+val gnu_option: string -> bool
+   (** Set the options for gnu systems *)
+
+val explode_comma_option: string -> string list
+   (** Split options by whitespace *)