diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-01 17:25:44 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-01 17:25:44 +0200 |
commit | b59b2b182a6832e1b6ebf3cf7ba4fd1943843b74 (patch) | |
tree | 3fa8c338c917d4f72f3408b6a45cffcc6e1e0f8a | |
parent | d8ed56833c508b5103a900ef04975013bd9ba77b (diff) | |
download | compcert-b59b2b182a6832e1b6ebf3cf7ba4fd1943843b74.tar.gz compcert-b59b2b182a6832e1b6ebf3cf7ba4fd1943843b74.zip |
Removed the version from the compcert.ini file and add it again in a separate file.
-rw-r--r-- | Makefile | 26 | ||||
-rw-r--r-- | VERSION | 4 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 2 | ||||
-rw-r--r-- | checklink/Check.ml | 2 | ||||
-rw-r--r-- | checklink/Validator.ml | 2 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 2 | ||||
-rw-r--r-- | driver/Configuration.ml | 1 | ||||
-rw-r--r-- | driver/Configuration.mli | 2 | ||||
-rw-r--r-- | driver/Driver.ml | 7 |
9 files changed, 27 insertions, 21 deletions
@@ -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 @@ -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 ^ |