diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Configuration.ml | 1 | ||||
-rw-r--r-- | driver/Configuration.mli | 2 | ||||
-rw-r--r-- | driver/Driver.ml | 33 |
3 files changed, 23 insertions, 13 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 70131fc6..64f24820 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -104,7 +104,6 @@ let advanced_debug = | "false" -> false | v -> bad_config "advanced_debug" [v] -let version = get_config_string "version" type struct_passing_style = | SP_ref_callee (* by reference, callee takes copy *) diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 72810456..f82ce213 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -36,8 +36,6 @@ val has_standard_headers: bool val advanced_debug: bool (** True if advanced debug is implement for the Target *) -val version: string - (** CompCert version string *) type struct_passing_style = | SP_ref_callee (* by reference, callee takes copy *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 352483bf..1b58fe61 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -74,7 +74,7 @@ let print_error oc msg = 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 @@ -127,7 +127,7 @@ let parse_c_file sourcename ifile = let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc - end; + end; (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with @@ -145,7 +145,7 @@ let parse_c_file sourcename ifile = (* Dump Asm code in binary format for the validator *) -let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version +let sdump_magic_number = "CompCertSDUMP" ^ Version.version let dump_asm asm destfile = let oc = open_out_bin destfile in @@ -155,7 +155,7 @@ let dump_asm asm destfile = output_value oc C2C.decl_atom; close_out oc -let jdump_magic_number = "CompCertJDUMP" ^ Configuration.version +let jdump_magic_number = "CompCertJDUMP" ^ Version.version let dump_jasm asm destfile = let oc = open_out_bin destfile in @@ -231,7 +231,7 @@ let compile_cminor_file ifile ofile = eprintf "File %s, character %d: Syntax error\n" ifile (Lexing.lexeme_start lb); exit 2 - | CMlexer.Error msg -> + | CMlexer.Error msg -> eprintf "File %s, character %d: %s\n" ifile (Lexing.lexeme_start lb) msg; exit 2 @@ -373,7 +373,7 @@ let process_h_file sourcename = end else begin eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename; exit 2 - end + end (* Record actions to be performed after parsing the command line *) @@ -398,9 +398,15 @@ let explode_comma_option s = | [] -> assert false | hd :: tl -> tl +let version_string = + if Version.buildnr <> "" && Version.tag <> "" then + sprintf "The CompCert verified compiler, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag + else + "The CompCert C verified compiler, version "^ Version.version ^ "\n" + let usage_string = -"The CompCert C verified compiler, version " ^ Configuration.version ^ " -Usage: ccomp [options] <source files> + version_string ^ + "Usage: ccomp [options] <source files> Recognized source files: .c C source file .i or .p C source file that should not be preprocessed @@ -477,6 +483,7 @@ General options: -stdlib <dir> Set the path of the Compcert run-time library -v Print external commands before invoking them -timings Show the time spent in various compiler passes + -version Print the version string and exit Interpreter mode: -interp Execute given .c files using the reference interpreter -quiet Suppress diagnostic messages for the interpreter @@ -488,6 +495,9 @@ Interpreter mode: let print_usage_and_exit _ = printf "%s" usage_string; exit 0 +let print_version_and_exit _ = + printf "%s" version_string; exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_return; option_fvararg_calls; option_funprototyped; @@ -510,13 +520,16 @@ let cmdline_actions = (* Getting help *) Exact "-help", Self print_usage_and_exit; Exact "--help", Self print_usage_and_exit; +(* Getting version info *) + Exact "-version", Self print_version_and_exit; + Exact "--version", Self print_version_and_exit; (* Processing options *) Exact "-c", Set option_c; Exact "-E", Set option_E; Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in - option_o := Some s); + option_o := Some s); (* Preprocessing options *) Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options); @@ -563,7 +576,7 @@ let cmdline_actions = Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; Exact "-sdump", Set option_sdump; -(* General options *) +(* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); Exact "-timings", Set option_timings; |