Print git revision with all --version outputs

tautschnig · tautschnig · commit 23455af5497c · 2018-06-21T15:42:20.000Z
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.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -38,6 +38,10 @@ if(${enable_cbmc_tests})
     enable_testing()
 endif()
 
+file(STRINGS src/config.inc config_inc_v REGEX "CBMC_VERSION *= *[0-9\.]+")
+string(REGEX REPLACE "^CBMC_VERSION *= *" "" CBMC_RELEASE ${config_inc_v})
+message(STATUS "CBMC release ${CBMC_RELEASE}")
+
 find_package(Git)
 
 macro(git_revision target files_var)
diff --git a/jbmc/src/janalyzer/Makefile b/jbmc/src/janalyzer/Makefile
@@ -33,6 +33,8 @@ CLEANFILES = janalyzer$(EXEEXT)
 
 all: janalyzer$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ifneq ($(wildcard ../jsil/Makefile),)
   OBJ += ../jsil/jsil$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JSIL
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -50,8 +50,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/options.h>
 #include <util/unicode.h>
 
-#include <cbmc/version.h>
-
 #include <goto-analyzer/static_show_domain.h>
 #include <goto-analyzer/static_simplifier.h>
 #include <goto-analyzer/static_verifier.h>
diff --git a/jbmc/src/janalyzer/module_dependencies.txt b/jbmc/src/janalyzer/module_dependencies.txt
@@ -1,6 +1,5 @@
 analyses
 ansi-c # should go away
-cbmc # version.h
 java_bytecode
 jdiff
 goto-analyzer
diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
@@ -63,6 +63,8 @@ CLEANFILES = jbmc$(EXEEXT)
 
 all: jbmc$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ###############################################################################
 
 jbmc$(EXEEXT): $(OBJ)
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -60,8 +60,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <java_bytecode/replace_java_nondet.h>
 #include <java_bytecode/simple_method_stubbing.h>
 
-#include <cbmc/version.h>
-
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(JBMC_OPTIONS, argc, argv),
   messaget(ui_message_handler),
diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt
@@ -1,6 +1,6 @@
 analyses
 ansi-c # should go away
-cbmc # version.h and bmc.h
+cbmc # bmc.h
 goto-instrument
 goto-programs
 goto-symex
diff --git a/jbmc/src/jdiff/Makefile b/jbmc/src/jdiff/Makefile
@@ -45,6 +45,8 @@ CLEANFILES = jdiff$(EXEEXT)
 
 all: jdiff$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ###############################################################################
 
 jdiff$(EXEEXT): $(OBJ)
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -55,8 +55,6 @@ Author: Peter Schrammel
 
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
-
 #include "java_syntactic_diff.h"
 #include <goto-diff/change_impact.h>
 #include <goto-diff/goto_diff.h>
diff --git a/jbmc/src/jdiff/module_dependencies.txt b/jbmc/src/jdiff/module_dependencies.txt
@@ -1,5 +1,4 @@
 analyses
-cbmc # version.h
 java_bytecode
 jdiff
 goto-diff
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
@@ -63,6 +63,8 @@ CLEANFILES = cbmc$(EXEEXT)
 
 all: cbmc$(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/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -62,7 +62,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
-#include "version.h"
 #include "xml_interface.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
@@ -28,7 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "bv_cbmc.h"
 #include "cbmc_dimacs.h"
 #include "counterexample_beautification.h"
-#include "version.h"
 
 /// Uses the options to pick an SMT 2.0 solver
 /// \return An smt2_dect::solvert giving the solver to use.
diff --git a/src/cbmc/version.h b/src/cbmc/version.h
diff --git 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))\""
+
 ###############################################################################
 
 clobber$(EXEEXT): $(OBJ)
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
@@ -34,7 +34,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
 
 clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
   parse_options_baset(CLOBBER_OPTIONS, argc, argv),
diff --git a/src/config.inc b/src/config.inc
@@ -70,3 +70,7 @@ endif
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"
+
+# Detailed version information
+CBMC_VERSION = 5.8
+GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
@@ -32,6 +32,8 @@ CLEANFILES = goto-analyzer$(EXEEXT)
 
 all: goto-analyzer$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ifneq ($(wildcard ../jsil/Makefile),)
   OBJ += ../jsil/jsil$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JSIL
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -54,7 +54,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/unicode.h>
 #include <util/exit_codes.h>
 
-#include <cbmc/version.h>
 #include <goto-programs/adjust_float_expressions.h>
 
 #include "taint_analysis.h"
diff --git a/src/goto-analyzer/module_dependencies.txt b/src/goto-analyzer/module_dependencies.txt
@@ -1,6 +1,5 @@
 ansi-c
 analyses
-cbmc # version.h
 cpp
 goto-analyzer
 goto-programs
diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile
@@ -46,6 +46,8 @@ all: goto-cl$(EXEEXT)
 endif
 all: goto-cc$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ifneq ($(wildcard ../jsil/Makefile),)
   OBJ += ../jsil/jsil$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JSIL
diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp
@@ -29,8 +29,6 @@ Author: Michael Tautschnig
 #include <util/get_base_name.h>
 #include <util/cout_message.h>
 
-#include <cbmc/version.h>
-
 #include "compile.h"
 
 static std::string assembler_name(
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
@@ -37,8 +37,6 @@ Date: June 2006
 
 #include <linking/static_lifetime_init.h>
 
-#include <cbmc/version.h>
-
 #define DOTGRAPHSETTINGS  "color=black;" \
                           "orientation=portrait;" \
                           "fontsize=20;"\
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
@@ -46,8 +46,6 @@ Author: CM Wintersteiger, 2006
 
 #include <goto-programs/read_goto_binary.h>
 
-#include <cbmc/version.h>
-
 #include "hybrid_binary.h"
 #include "linker_script_merge.h"
 
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
@@ -22,7 +22,6 @@ Author: CM Wintersteiger, 2006
 #include <sysexits.h>
 #endif
 
-#include <cbmc/version.h>
 
 /// constructor
 goto_cc_modet::goto_cc_modet(
diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp
@@ -46,8 +46,6 @@ Author: CM Wintersteiger, 2006
 
 #include <goto-programs/read_goto_binary.h>
 
-#include <cbmc/version.h>
-
 #include "hybrid_binary.h"
 #include "linker_script_merge.h"
 
diff --git a/src/goto-cc/module_dependencies.txt b/src/goto-cc/module_dependencies.txt
@@ -1,5 +1,4 @@
 ansi-c
-cbmc # version.h
 cpp
 goto-cc
 goto-programs
diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp
@@ -26,8 +26,6 @@ Author: CM Wintersteiger, 2006
 #include <util/config.h>
 #include <util/get_base_name.h>
 
-#include <cbmc/version.h>
-
 #include "compile.h"
 
 /// does it.
diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile
@@ -44,6 +44,8 @@ CLEANFILES = goto-diff$(EXEEXT)
 
 all: goto-diff$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ###############################################################################
 
 goto-diff$(EXEEXT): $(OBJ)
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
@@ -55,8 +55,6 @@ Author: Peter Schrammel
 #include <ansi-c/cprover_library.h>
 #include <cpp/cprover_library.h>
 
-#include <cbmc/version.h>
-
 #include "goto_diff.h"
 #include "syntactic_diff.h"
 #include "unified_diff.h"
diff --git a/src/goto-diff/module_dependencies.txt b/src/goto-diff/module_dependencies.txt
@@ -1,6 +1,5 @@
 analyses
 ansi-c
-cbmc # version.h
 cpp
 goto-diff
 goto-instrument
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
@@ -101,6 +101,8 @@ include ../common
 
 all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ifneq ($(LIB_GLPK),)
   LIBS += $(LIB_GLPK)
   CP_CXXFLAGS += -DHAVE_GLPK
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -65,8 +65,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/cprover_library.h>
 #include <cpp/cprover_library.h>
 
-#include <cbmc/version.h>
-
 #include "document_properties.h"
 #include "uninitialized.h"
 #include "full_slicer.h"
diff --git a/src/goto-instrument/module_dependencies.txt b/src/goto-instrument/module_dependencies.txt
@@ -1,7 +1,6 @@
 accelerate
 analyses
 ansi-c
-cbmc # version.h
 cpp
 goto-instrument
 goto-programs
diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile
@@ -22,6 +22,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
@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/cout_message.h>
 
-#include <cbmc/version.h>
-
 #include "mm_parser.h"
 #include "mm2cpp.h"
 
diff --git a/src/memory-models/module_dependencies.txt b/src/memory-models/module_dependencies.txt
@@ -1,4 +1,3 @@
-cbmc # version.h
 memory-models
 langapi # should go away
 util

Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,4 @@`
`1`	`1`	`analyses`
`2`		`-cbmc # version.h`
`3`	`2`	`java_bytecode`
`4`	`3`	`jdiff`
`5`	`4`	`goto-diff`