Removed the version from the compcert.ini file and add it again in a separate file.

9 files changed, 27 insertions, 21 deletions

diff --git a/Makefile b/Makefile
index 2205ed64..0a13bf4b 100644
--- a/Makefile
+++ b/Makefile
@@ -135,22 +135,22 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach
 	$(COQEXEC) extraction/extraction.v
 	touch extraction/STAMP
 
-.depend.extr: extraction/STAMP tools/modorder
+.depend.extr: extraction/STAMP tools/modorder driver/Version.ml
 	$(MAKE) -f Makefile.extr depend
 
-ccomp: .depend.extr compcert.ini FORCE
+ccomp: .depend.extr compcert.ini driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr ccomp
-ccomp.byte: .depend.extr compcert.ini FORCE
+ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr ccomp.byte
 
-cchecklink: .depend.extr compcert.ini FORCE
+cchecklink: .depend.extr compcert.ini driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr cchecklink
-cchecklink.byte: .depend.extr compcert.ini FORCE
+cchecklink.byte: .depend.extr compcert.ini driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr cchecklink.byte
 
-clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE
+clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr clightgen
-clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE
+clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr clightgen.byte
 
 runtime:
@@ -192,7 +192,7 @@ latexdoc:
 	@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
 	@chmod -w $*.v
 
-compcert.ini: Makefile.config VERSION
+compcert.ini: Makefile.config
 	(echo "stdlib_path=$(LIBDIR)"; \
          echo "prepro=$(CPREPRO)"; \
          echo "asm=$(CASM)"; \
@@ -206,11 +206,14 @@ compcert.ini: Makefile.config VERSION
          echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
          echo "advanced_debug=$(ADVANCED_DEBUG)"; \
          echo "struct_passing_style=$(STRUCT_PASSING)"; \
-         echo "struct_return_style=$(STRUCT_RETURN)"; \
-         version=`cat VERSION`; \
-         echo version=$$version) \
+         echo "struct_return_style=$(STRUCT_RETURN)";) \
         > compcert.ini
 
+driver/Version.ml: VERSION
+	cat VERSION \
+	| sed -e 's|\(.*\)=\(.*\)|let \1 = \"\2\"|g' \
+	>driver/Version.ml
+
 cparser/Parser.v: cparser/Parser.vy
 	$(MENHIR) --coq cparser/Parser.vy
 
@@ -233,6 +236,7 @@ clean:
 	rm -f $(patsubst %, %/*.vo, $(DIRS))
 	rm -rf doc/html doc/*.glob
 	rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o
+	rm -f driver/Version.ml
 	rm -f compcert.ini
 	rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
 	rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
diff --git a/VERSION b/VERSION
index 6b4950e3..5d18e418 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1,3 @@
-2.4
+version=2.5
+buildnr=
+tag=
\ No newline at end of file
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 497760c1..b54188ca 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -294,7 +294,7 @@ let print_inline_asm print_preg oc txt sg args res =
 (** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
-  fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
+  fprintf oc "%s File generated by CompCert %s\n" comment Version.version;
   fprintf oc "%s Command line:" comment;
   for i = 1 to Array.length Sys.argv - 1 do
     fprintf oc " %s" Sys.argv.(i)
diff --git a/checklink/Check.ml b/checklink/Check.ml
index bfd03c97..10c7aa45 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -2573,7 +2573,7 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
 
 (** Read a .sdump file *)
 
-let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version
+let sdump_magic_number = "CompCertSDUMP" ^ Version.version
 
 let read_sdump file =
   let ic = open_in_bin file in
diff --git a/checklink/Validator.ml b/checklink/Validator.ml
index 6969409a..f9ca0edb 100644
--- a/checklink/Validator.ml
+++ b/checklink/Validator.ml
@@ -97,7 +97,7 @@ let anonymous arg =
     set_elf_file arg
 
 let usage =
-  "The CompCert C post-linking validator, version " ^ Configuration.version ^ "
+  "The CompCert C post-linking validator, version " ^ Version.version ^ "
 Usage: cchecklink [options] <.sdump files> <ELF executable>
 In the absence of options, checks are performed and a short result is displayed.
 Options are:"
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 13d4049e..96332006 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -328,7 +328,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_string oc bt.base_type_name
 
     let print_compilation_unit oc tag =
-      let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Configuration.version Configuration.arch in
+      let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Version.version Configuration.arch in
       print_string oc (Sys.getcwd ());
       print_addr oc (get_start_addr ());
       print_addr oc (get_end_addr ());
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 805d5405..402bdb65 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -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
@@ -387,7 +387,10 @@ let explode_comma_option s =
   | hd :: tl -> tl
 
 let version_string =
-  "The CompCert C verified compiler, version "^ Configuration.version ^ "\n"
+  if Version.buildnr <> "" && Version.tag <> "" then
+    sprintf "The CompCert verified compiler, %s,%s,%s\n" Version.version Version.buildnr Version.tag
+  else
+    "The CompCert C verified compiler, version "^ Version.version ^ "\n"
 
 let usage_string =
   version_string ^