Print git revision with all --version outputs

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.

Author: tautschnig

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)
 if(GIT_FOUND)
   message(STATUS "Found Git executable: ${GIT_EXECUTABLE}")

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

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -50,8 +50,6 @@ Author: Daniel Kroening, [email protected]
 #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>

jbmc/src/janalyzer/module_dependencies.txt

@@ -1,6 +1,5 @@
 analyses
 ansi-c # should go away
-cbmc # version.h
 java_bytecode
 jdiff
 goto-analyzer

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)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -60,8 +60,6 @@ Author: Daniel Kroening, [email protected]
 #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),

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

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)

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>

jbmc/src/jdiff/module_dependencies.txt

@@ -1,5 +1,4 @@
 analyses
-cbmc # version.h
 java_bytecode
 jdiff
 goto-diff

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

src/cbmc/cbmc_parse_options.cpp

@@ -62,7 +62,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
-#include "version.h"
 #include "xml_interface.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):

src/cbmc/cbmc_solvers.cpp

@@ -28,7 +28,6 @@ Author: Daniel Kroening, [email protected]
 #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.

src/cbmc/version.h

@@ -30,6 +30,8 @@ CLEANFILES = clobber$(EXEEXT)
 
 all: clobber$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ###############################################################################
 
 clobber$(EXEEXT): $(OBJ)

src/clobber/Makefile

@@ -34,7 +34,6 @@ Author: Daniel Kroening, [email protected]
 
 #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),

src/clobber/clobber_parse_options.cpp

@@ -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")

src/config.inc

@@ -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

src/goto-analyzer/Makefile

@@ -54,7 +54,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/unicode.h>
 #include <util/exit_codes.h>
 
-#include <cbmc/version.h>
 #include <goto-programs/adjust_float_expressions.h>
 
 #include "taint_analysis.h"

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -1,6 +1,5 @@
 ansi-c
 analyses
-cbmc # version.h
 cpp
 goto-analyzer
 goto-programs

src/goto-analyzer/module_dependencies.txt

@@ -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

src/goto-cc/Makefile

@@ -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(

src/goto-cc/as_mode.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;"\

src/goto-cc/compile.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"
 

src/goto-cc/gcc_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(

src/goto-cc/goto_cc_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"
 

src/goto-cc/ld_mode.cpp

@@ -1,5 +1,4 @@
 ansi-c
-cbmc # version.h
 cpp
 goto-cc
 goto-programs

src/goto-cc/module_dependencies.txt

@@ -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.

src/goto-cc/ms_cl_mode.cpp

@@ -44,6 +44,8 @@ CLEANFILES = goto-diff$(EXEEXT)
 
 all: goto-diff$(EXEEXT)
 
+CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+
 ###############################################################################
 
 goto-diff$(EXEEXT): $(OBJ)

src/goto-diff/Makefile

@@ -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"

src/goto-diff/goto_diff_parse_options.cpp

@@ -1,6 +1,5 @@
 analyses
 ansi-c
-cbmc # version.h
 cpp
 goto-diff
 goto-instrument

src/goto-diff/module_dependencies.txt

@@ -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

src/goto-instrument/Makefile

@@ -65,8 +65,6 @@ Author: Daniel Kroening, [email protected]
 #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"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1,7 +1,6 @@
 accelerate
 analyses
 ansi-c
-cbmc # version.h
 cpp
 goto-instrument
 goto-programs

src/goto-instrument/module_dependencies.txt

@@ -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

src/memory-models/Makefile

@@ -16,8 +16,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/cout_message.h>
 
-#include <cbmc/version.h>
-
 #include "mm_parser.h"
 #include "mm2cpp.h"
 

src/memory-models/mmcc_parse_options.cpp

@@ -1,4 +1,3 @@
-cbmc # version.h
 memory-models
 langapi # should go away
 util