Merge branch 'master' into json_export

Conflicts:
	driver/Driver.ml

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;