From 556f32276894f00124a7aaa674b4e6134e3a9eb3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 31 May 2016 17:22:21 +0000 Subject: [PATCH 1/6] Print git revision with all --version outputs --- src/cbmc/Makefile | 2 ++ src/cbmc/cbmc_parse_options.cpp | 1 - src/cbmc/cbmc_solvers.cpp | 1 - src/cbmc/version.h | 6 ------ src/config.inc | 6 ++++++ src/goto-analyzer/Makefile | 2 ++ src/goto-analyzer/goto_analyzer_parse_options.cpp | 2 -- src/goto-cc/Makefile | 2 ++ src/goto-cc/compile.cpp | 2 -- src/goto-cc/gcc_mode.cpp | 2 -- src/goto-cc/goto_cc_mode.cpp | 1 - src/goto-cc/ms_cl_mode.cpp | 2 -- src/goto-diff/Makefile | 2 ++ src/goto-diff/goto_diff_parse_options.cpp | 2 -- src/goto-instrument/Makefile | 2 ++ src/goto-instrument/goto_instrument_parse_options.cpp | 2 -- src/musketeer/Makefile | 2 ++ src/musketeer/version.h | 6 ------ 18 files changed, 18 insertions(+), 27 deletions(-) delete mode 100644 src/cbmc/version.h delete mode 100644 src/musketeer/version.h diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 37f8b65eb00..83e2f1d0713 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -53,6 +53,8 @@ CLEANFILES = cbmc$(EXEEXT) all: cbmc$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" + ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) CP_CXXFLAGS += -DHAVE_BV_REFINEMENT diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 047e589accc..5429843132b 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -55,7 +55,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "cbmc_solvers.h" #include "cbmc_parse_options.h" #include "bmc.h" -#include "version.h" #include "xml_interface.h" /*******************************************************************\ diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index ccd660dc586..493df864d75 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -24,7 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "bv_cbmc.h" #include "cbmc_dimacs.h" #include "counterexample_beautification.h" -#include "version.h" /*******************************************************************\ diff --git a/src/cbmc/version.h b/src/cbmc/version.h deleted file mode 100644 index 017ded44272..00000000000 --- a/src/cbmc/version.h +++ /dev/null @@ -1,6 +0,0 @@ -#ifndef CPROVER_CBMC_VERSION_H -#define CPROVER_CBMC_VERSION_H - -#define CBMC_VERSION "5.7" - -#endif // CPROVER_CBMC_VERSION_H diff --git a/src/config.inc b/src/config.inc index e1c1266f683..7e82325f268 100644 --- a/src/config.inc +++ b/src/config.inc @@ -28,3 +28,9 @@ MINISAT2 = ../../minisat-2.2.1 # Signing identity for MacOS Gatekeeper OSX_IDENTITY="Developer ID Application: Daniel Kroening" + +# Detailed version information +CBMC_VERSION = 5.7 +GIT_HEAD = $(shell git rev-parse --short HEAD || echo "n/a") +GIT_MOD = $(shell git diff HEAD --quiet || echo +dirty) +RELEASE_INFO = $(GIT_HEAD)$(GIT_MOD) diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 9eb45165f9c..a978ea664bf 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -30,6 +30,8 @@ CLEANFILES = goto-analyzer$(EXEEXT) all: goto-analyzer$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" + ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 5f889ff99d7..1d3c469fc20 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -42,8 +42,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include "goto_analyzer_parse_options.h" #include "taint_analysis.h" #include "unreachable_instructions.h" diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 51ac3f0f9cb..930317eabbd 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -43,6 +43,8 @@ all: goto-cl$(EXEEXT) endif all: goto-cc$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" + ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) endif diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 04d50e76f82..7954313aec9 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -35,8 +35,6 @@ Date: June 2006 #include -#include - #include "compile.h" #define DOTGRAPHSETTINGS "color=black;" \ diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 19444ef1fc5..4a10743be5a 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -26,8 +26,6 @@ Author: CM Wintersteiger, 2006 #include #include -#include - #include "compile.h" #include "gcc_mode.h" diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp index a0e363ad112..84957709d8d 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -17,7 +17,6 @@ Author: CM Wintersteiger, 2006 #include #endif -#include #include "goto_cc_mode.h" diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index 25dc0e039e2..006d3f8ebbd 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -22,8 +22,6 @@ Author: CM Wintersteiger, 2006 #include #include -#include - #include "ms_cl_mode.h" #include "compile.h" diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index b11cb008b3a..50b9c08414c 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -33,6 +33,8 @@ CLEANFILES = goto-diff$(EXEEXT) all: goto-diff$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" + ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c66bd9817a6..e885953a3e4 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -36,8 +36,6 @@ Author: Peter Schrammel #include -#include - #include "goto_diff_parse_options.h" #include "goto_diff.h" #include "syntactic_diff.h" diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 4b74d173ff7..79b642628ec 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -89,6 +89,8 @@ include ../common all: goto-instrument$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" + ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 66421b2e1e1..9760158a8b6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -55,8 +55,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include "goto_instrument_parse_options.h" #include "document_properties.h" #include "uninitialized.h" diff --git a/src/musketeer/Makefile b/src/musketeer/Makefile index be41fa923cc..229138de509 100644 --- a/src/musketeer/Makefile +++ b/src/musketeer/Makefile @@ -46,6 +46,8 @@ include ../common all: musketeer$(EXEEXT) +CP_CXXFLAGS += -DGOTO_FENCE_INSERTER_VERSION="\"0.37 ($(RELEASE_INFO))\"" + ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) CP_CXXFLAGS += -DHAVE_GLPK diff --git a/src/musketeer/version.h b/src/musketeer/version.h deleted file mode 100644 index fde0c82ecea..00000000000 --- a/src/musketeer/version.h +++ /dev/null @@ -1,6 +0,0 @@ -#ifndef CPROVER_MUSKETEER_VERSION_H -#define CPROVER_MUSKETEER_VERSION_H - -#define MUSKETEER_VERSION "0.37" - -#endif // CPROVER_MUSKETEER_VERSION_H From ff9024bb213c4e7e86eea0911273ec9f490185be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 23 Mar 2017 10:31:58 +0100 Subject: [PATCH 2/6] use git-describe for version UID creation This uses the output of `git-describe --tags --always --dirty` to create a UID for binaries. This includes last tag, number of commits after last tag, shortened SHA1 checksum and optional dirty flag for uncommited changes. In case of tagged commit, only the tag name is used. --- src/cbmc/Makefile | 2 +- src/clobber/Makefile | 2 ++ src/clobber/clobber_parse_options.cpp | 2 -- src/config.inc | 4 +--- src/goto-analyzer/Makefile | 2 +- src/goto-cc/Makefile | 2 +- src/goto-cc/as_mode.cpp | 2 -- src/goto-diff/Makefile | 2 +- src/goto-instrument/Makefile | 2 +- src/memory-models/Makefile | 2 ++ src/memory-models/mmcc_parse_options.cpp | 2 -- src/musketeer/Makefile | 2 +- src/musketeer/musketeer_parse_options.cpp | 1 - src/symex/Makefile | 2 ++ src/symex/symex_parse_options.cpp | 2 -- 15 files changed, 13 insertions(+), 18 deletions(-) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 83e2f1d0713..5640212bc73 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -53,7 +53,7 @@ CLEANFILES = cbmc$(EXEEXT) all: cbmc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) diff --git a/src/clobber/Makefile b/src/clobber/Makefile index f3a4c8aed20..707a6ae6935 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -30,6 +30,8 @@ CLEANFILES = clobber$(EXEEXT) all: clobber$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) CP_CXXFLAGS += -DHAVE_BV_REFINEMENT diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 803ab9db5b1..e9067f594b3 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -32,8 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include "clobber_parse_options.h" // #include "clobber_instrumenter.h" diff --git a/src/config.inc b/src/config.inc index 7e82325f268..5a664edb38d 100644 --- a/src/config.inc +++ b/src/config.inc @@ -31,6 +31,4 @@ OSX_IDENTITY="Developer ID Application: Daniel Kroening" # Detailed version information CBMC_VERSION = 5.7 -GIT_HEAD = $(shell git rev-parse --short HEAD || echo "n/a") -GIT_MOD = $(shell git diff HEAD --quiet || echo +dirty) -RELEASE_INFO = $(GIT_HEAD)$(GIT_MOD) +GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index a978ea664bf..0fa8786fd6d 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -30,7 +30,7 @@ CLEANFILES = goto-analyzer$(EXEEXT) all: goto-analyzer$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 930317eabbd..9516a4df0bd 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -43,7 +43,7 @@ all: goto-cl$(EXEEXT) endif all: goto-cc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index bb87b6c6abb..308b549c581 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -24,8 +24,6 @@ Author: Michael Tautschnig #include #include -#include - #include "compile.h" #include "as_mode.h" diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 50b9c08414c..f6337faaa52 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -33,7 +33,7 @@ CLEANFILES = goto-diff$(EXEEXT) all: goto-diff$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 79b642628ec..55a32b8b22a 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -89,7 +89,7 @@ include ../common all: goto-instrument$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(RELEASE_INFO))\"" +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile index e13309deaae..372de18eba0 100644 --- a/src/memory-models/Makefile +++ b/src/memory-models/Makefile @@ -21,6 +21,8 @@ CLEANFILES = memory_models$(LIBEXT) \ all: mmcc$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ############################################################################### mm_y.tab.cpp: parser.y diff --git a/src/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp index 859393f9726..71c0337280e 100644 --- a/src/memory-models/mmcc_parse_options.cpp +++ b/src/memory-models/mmcc_parse_options.cpp @@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include "mm_parser.h" #include "mm2cpp.h" #include "mmcc_parse_options.h" diff --git a/src/musketeer/Makefile b/src/musketeer/Makefile index 229138de509..a836ddf37d3 100644 --- a/src/musketeer/Makefile +++ b/src/musketeer/Makefile @@ -46,7 +46,7 @@ include ../common all: musketeer$(EXEEXT) -CP_CXXFLAGS += -DGOTO_FENCE_INSERTER_VERSION="\"0.37 ($(RELEASE_INFO))\"" +CP_CXXFLAGS += -DMUSKETEER_VERSION="\"0.37 ($(GIT_INFO))\"" ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp index ae40a2f2318..6d26707b36c 100644 --- a/src/musketeer/musketeer_parse_options.cpp +++ b/src/musketeer/musketeer_parse_options.cpp @@ -38,7 +38,6 @@ Module: Main Module #include #include "propagate_const_function_pointers.h" -#include "version.h" #include "musketeer_parse_options.h" #include "fencer.h" #include "fence_shared.h" diff --git a/src/symex/Makefile b/src/symex/Makefile index 672b2e07fc2..48dd73196f0 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -34,6 +34,8 @@ CLEANFILES = symex$(EXEEXT) all: symex$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) CP_CXXFLAGS += -DHAVE_BV_REFINEMENT diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 8001a5b8155..1906d7615ce 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -43,8 +43,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include "path_search.h" From 70d919d8db56242c97608b394c9de4858202fa30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 23 Mar 2017 11:12:42 +0100 Subject: [PATCH 3/6] windowsify compiler options --- src/cbmc/Makefile | 6 +++++- src/clobber/Makefile | 6 +++++- src/common | 4 +++- src/config.inc | 1 - src/goto-analyzer/Makefile | 6 +++++- src/goto-cc/Makefile | 6 +++++- src/goto-diff/Makefile | 6 +++++- src/goto-instrument/Makefile | 6 +++++- src/memory-models/Makefile | 6 +++++- src/musketeer/Makefile | 6 +++++- src/symex/Makefile | 6 +++++- 11 files changed, 48 insertions(+), 11 deletions(-) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 5640212bc73..3c0bd1ffb3e 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -53,7 +53,11 @@ CLEANFILES = cbmc$(EXEEXT) all: cbmc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) diff --git a/src/clobber/Makefile b/src/clobber/Makefile index 707a6ae6935..b0477115c8e 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -30,7 +30,11 @@ CLEANFILES = clobber$(EXEEXT) all: clobber$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) diff --git a/src/common b/src/common index 20c4fadbb44..62b06bfe04d 100644 --- a/src/common +++ b/src/common @@ -1,3 +1,6 @@ +# get version from git +GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") + # Build platform # (use one of AUTO, Unix, OSX, OSX_Universal, MSVC, Cygwin, MinGW) @@ -207,4 +210,3 @@ D_FILES1 = $(SRC:.c=.d) D_FILES = $(D_FILES1:.cpp=.d) -include $(D_FILES) - diff --git a/src/config.inc b/src/config.inc index 5a664edb38d..7fede6e723d 100644 --- a/src/config.inc +++ b/src/config.inc @@ -31,4 +31,3 @@ OSX_IDENTITY="Developer ID Application: Daniel Kroening" # Detailed version information CBMC_VERSION = 5.7 -GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 0fa8786fd6d..b9e0a664330 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -30,7 +30,11 @@ CLEANFILES = goto-analyzer$(EXEEXT) all: goto-analyzer$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 9516a4df0bd..50b25964c56 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -43,7 +43,11 @@ all: goto-cl$(EXEEXT) endif all: goto-cc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index f6337faaa52..24d6795c94e 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -33,7 +33,11 @@ CLEANFILES = goto-diff$(EXEEXT) all: goto-diff$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 55a32b8b22a..49478f61ddf 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -89,7 +89,11 @@ include ../common all: goto-instrument$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(wildcard ../java_bytecode/Makefile),) OBJ += ../java_bytecode/java_bytecode$(LIBEXT) diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile index 372de18eba0..ab9c6114473 100644 --- a/src/memory-models/Makefile +++ b/src/memory-models/Makefile @@ -21,7 +21,11 @@ CLEANFILES = memory_models$(LIBEXT) \ all: mmcc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ############################################################################### diff --git a/src/musketeer/Makefile b/src/musketeer/Makefile index a836ddf37d3..950b7850a46 100644 --- a/src/musketeer/Makefile +++ b/src/musketeer/Makefile @@ -46,7 +46,11 @@ include ../common all: musketeer$(EXEEXT) -CP_CXXFLAGS += -DMUSKETEER_VERSION="\"0.37 ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DMUSKETEER_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DMUSKETEER_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) diff --git a/src/symex/Makefile b/src/symex/Makefile index 48dd73196f0..455626a106c 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -34,7 +34,11 @@ CLEANFILES = symex$(EXEEXT) all: symex$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +ifeq ($(BUILD_ENV_),MSVC) + CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else + CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) From 159bd83bada2742d26adfdac5e4faae2560ee90a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Mar 2017 13:30:25 +0000 Subject: [PATCH 4/6] Build .release_info files containing the version string By adding build-dependencies to all *_parse_options files whenever the contents of .release_info files differs from $(RELEASE_INFO), we ensure that binaries print the correct version strings. --- .gitignore | 1 + src/common | 14 +++++++++++++- 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 7ba5ba011b4..082790b7126 100644 --- a/.gitignore +++ b/.gitignore @@ -20,6 +20,7 @@ src/goto-analyzer/taint_driver_scripts/.idea/* *.obj *.a *.lib +.release_info src/ansi-c/arm_builtin_headers.inc src/ansi-c/clang_builtin_headers.inc src/ansi-c/cprover_library.inc diff --git a/src/common b/src/common index 62b06bfe04d..c48c683e67e 100644 --- a/src/common +++ b/src/common @@ -185,12 +185,24 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) %.obj:%.c $(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@ +# make >= 4.0 has a `file` function that may be fast than `shell cat` +# for now, portability wins +KNOWN_RELEASE_INFO = $(shell cat .release_info 2>/dev/null) +ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO)) +$(filter %_parse_options$(OBJEXT), $(OBJ)): .release_info + +.release_info: + echo $(RELEASE_INFO) > $@ + +.PHONY: .release_info +endif + clean: $(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \ $(patsubst %.cpp, %.d, $(filter %.cpp, $(SRC))) \ $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \ $(patsubst %.cc, %.d, $(filter %.cc, $(SRC))) \ - $(CLEANFILES) + $(CLEANFILES) .release_info .PHONY: first_target clean all .PHONY: sources generated_files From f7be1c44a3461e719c0d9f1141cbc4cd1706adf6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 24 Mar 2017 17:52:13 +0100 Subject: [PATCH 5/6] RELEASE_INFO -> GIT_INFO --- src/common | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/common b/src/common index c48c683e67e..d3022e8734a 100644 --- a/src/common +++ b/src/common @@ -185,14 +185,14 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) %.obj:%.c $(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@ -# make >= 4.0 has a `file` function that may be fast than `shell cat` +# make >= 4.0 has a `file` function that may be faster than `shell cat` # for now, portability wins KNOWN_RELEASE_INFO = $(shell cat .release_info 2>/dev/null) -ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO)) +ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO)) $(filter %_parse_options$(OBJEXT), $(OBJ)): .release_info .release_info: - echo $(RELEASE_INFO) > $@ + echo $(GIT_INFO) > $@ .PHONY: .release_info endif From 4df4a36b894fdf1f5fcfe4ad196505f2d334e36e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 10 May 2017 12:24:25 +0200 Subject: [PATCH 6/6] add centered git version to CBMC banner --- src/cbmc/Makefile | 6 ++++-- src/cbmc/cbmc_parse_options.cpp | 3 ++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 3c0bd1ffb3e..c9f646f63ee 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -54,9 +54,11 @@ CLEANFILES = cbmc$(EXEEXT) all: cbmc$(EXEEXT) ifeq ($(BUILD_ENV_),MSVC) - CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' + CP_CXXFLAGS += /DCBMC_TAG_VERSION='"""$(CBMC_VERSION)"""' \ + /DCBMC_VERSION='"""($(GIT_INFO))"""' else - CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + CP_CXXFLAGS += -DCBMC_TAG_VERSION="\"$(CBMC_VERSION)\"" \ + -DCBMC_VERSION="\"($(GIT_INFO))\"" endif ifneq ($(wildcard ../bv_refinement/Makefile),) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 5429843132b..4414db851bf 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1044,13 +1044,14 @@ void cbmc_parse_optionst::help() { std::cout << "\n" - "* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2016 "; + "* * CBMC " CBMC_TAG_VERSION " - Copyright (C) 2001-2016 "; std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; std::cout << " * *\n"; std::cout << + "* * " CBMC_VERSION " * * \n" "* * Daniel Kroening, Edmund Clarke * *\n" "* * Carnegie Mellon University, Computer Science Department * *\n" "* * kroening@kroening.com * *\n"