Include git revision in version output

.gitignore

@@ -28,6 +28,7 @@ Release/*
 *.obj
 *.a
 *.lib
+.release_info
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc
 src/ansi-c/cprover_builtin_headers.inc

CMakeLists.txt

@@ -38,6 +38,52 @@ 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)
+  if(GIT_FOUND)
+    add_custom_command(
+      OUTPUT .release_info
+      COMMAND ${CMAKE_COMMAND} -E echo_append "#define __CBMC_VERSION " > .release_info
+      COMMAND "${GIT_EXECUTABLE}" "describe" "--tags" "--always" "--long" >> .release_info
+      COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_str(v) \"${CBMC_RELEASE} (\" # v \")\"" >> .release_info
+      COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_xstr(v) __CBMC_VERSION_str(v)" >> .release_info
+      COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION __CBMC_VERSION_xstr(__CBMC_VERSION)" >> .release_info
+      VERBATIM
+      )
+    add_custom_command(
+      TARGET ${target}
+      POST_BUILD
+      COMMAND ${CMAKE_COMMAND} -E remove -f .release_info
+      )
+  else()
+    add_custom_command(
+      OUTPUT .release_info
+      COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION \"${CBMC_RELEASE} (n/a)\"" >> .release_info
+      VERBATIM
+      )
+  endif()
+
+  if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+     "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+  )
+    set_source_files_properties(
+      ${${files_var}}
+      PROPERTIES
+        OBJECT_DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/.release_info
+        COMPILE_FLAGS "-include .release_info")
+  elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    set_source_files_properties(
+      ${${files_var}}
+      PROPERTIES
+        COMPILE_FLAGS "/DCBMC_VERSION=\"${CBMC_RELEASE} (n/a)\"")
+  endif()
+endmacro()
+
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)

jbmc/src/janalyzer/CMakeLists.txt

@@ -24,3 +24,6 @@ target_link_libraries(janalyzer-lib
 # Executable
 add_executable(janalyzer janalyzer_main.cpp)
 target_link_libraries(janalyzer janalyzer-lib)
+
+set(cbmc_version_files janalyzer_parse_options.cpp)
+git_revision(janalyzer-lib cbmc_version_files)

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>
@@ -723,17 +721,11 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 /// display command line help
 void janalyzer_parse_optionst::help()
 {
-  std::cout << "\n"
-               "* * JANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 ";
-
-  std::cout << "(" << (sizeof(void *) * 8) << "-bit version)";
-
-  std::cout << " * *\n";
-
   // clang-format off
-  std::cout <<
+  std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
+            <<
      /* NOLINTNEXTLINE(whitespace/line_length) */
-    "* *         JANALYZER " CBMC_VERSION " - Copyright (C) 2016-2018          * *\n"
+    "* *                   Copyright (C) 2016-2018                    * *\n"
     "* *                  Daniel Kroening, Diffblue                   * *\n"
     "* *                   [email protected]                      * *\n"
     "\n"

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/CMakeLists.txt

@@ -29,3 +29,6 @@ target_link_libraries(jbmc-lib
 # Executable
 add_executable(jbmc jbmc_main.cpp)
 target_link_libraries(jbmc jbmc-lib)
+
+set(cbmc_version_files jbmc_parse_options.cpp)
+git_revision(jbmc-lib cbmc_version_files)

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),
@@ -1069,15 +1067,10 @@ bool jbmc_parse_optionst::generate_function_body(
 /// display command line help
 void jbmc_parse_optionst::help()
 {
-  std::cout << "\n"
-               "* *   JBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << "   * *\n";
-
   // clang-format off
-  std::cout <<
+  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
+            <<
+    "* *                 Copyright (C) 2001-2018                 * *\n"
     "* *              Daniel Kroening, Edmund Clarke             * *\n"
     "* * Carnegie Mellon University, Computer Science Department * *\n"
     "* *                 [email protected]                   * *\n"

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/CMakeLists.txt

@@ -26,3 +26,6 @@ target_link_libraries(jdiff-lib
 # Executable
 add_executable(jdiff jdiff_main.cpp)
 target_link_libraries(jdiff jdiff-lib)
+
+set(cbmc_version_files jdiff_parse_options.cpp)
+git_revision(jdiff-lib cbmc_version_files)

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>
@@ -429,10 +427,9 @@ bool jdiff_parse_optionst::process_goto_program(
 void jdiff_parse_optionst::help()
 {
   // clang-format off
-  std::cout <<
-    "\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "* *           JDIFF " CBMC_VERSION " - Copyright (C) 2016-2018       * *\n"
+  std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
+            <<
+    "* *                Copyright (C) 2016-2018                  * *\n"
     "* *            Daniel Kroening, Peter Schrammel             * *\n"
     "* *                 [email protected]                   * *\n"
     "\n"

jbmc/src/jdiff/module_dependencies.txt

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

src/cbmc/CMakeLists.txt

@@ -31,3 +31,6 @@ add_if_library(cbmc-lib jsil)
 # Executable
 add_executable(cbmc cbmc_main.cpp)
 target_link_libraries(cbmc cbmc-lib)
+
+set(cbmc_version_files cbmc_parse_options.cpp cbmc_solvers.cpp)
+git_revision(cbmc-lib cbmc_version_files)

src/cbmc/Makefile

@@ -56,6 +56,8 @@ INCLUDES= -I ..
 
 LIBS =
 
+CBMC_VERSION_FILES = cbmc_solvers$(OBJEXT)
+
 include ../config.inc
 include ../common
 

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):
@@ -867,15 +866,9 @@ bool cbmc_parse_optionst::process_goto_program(
 void cbmc_parse_optionst::help()
 {
   // clang-format off
-  std::cout <<
-    "\n"
-    "* *   CBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << "   * *\n";
-
-  std::cout <<
+  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
+            <<
+    "* *                 Copyright (C) 2001-2018                 * *\n"
     "* *              Daniel Kroening, Edmund Clarke             * *\n"
     "* * Carnegie Mellon University, Computer Science Department * *\n"
     "* *                 [email protected]                   * *\n"

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/clobber/CMakeLists.txt

@@ -30,3 +30,5 @@ add_if_library(clobber-lib bv_refinement)
 add_executable(clobber clobber_main.cpp)
 target_link_libraries(clobber clobber-lib)
 
+set(cbmc_version_files clobber_parse_options.cpp)
+git_revision(clobber-lib cbmc_version_files)

src/clobber/clobber_parse_options.cpp

@@ -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),
@@ -349,15 +348,10 @@ void clobber_parse_optionst::report_failure()
 /// display command line help
 void clobber_parse_optionst::help()
 {
-  std::cout <<
-    "\n"
-    "* *     CLOBBER " CBMC_VERSION " - Copyright (C) 2014 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << "     * *\n";
-
-  std::cout <<
+  // clang-format off
+  std::cout << '\n' << banner_string("CLOBBER", CBMC_VERSION) << '\n'
+            <<
+    "* *                   Copyright (C) 2014                    * *\n"
     "* *                    Daniel Kroening                      * *\n"
     "* *                 University of Oxford                    * *\n"
     "* *                 [email protected]                   * *\n"
@@ -415,4 +409,5 @@ void clobber_parse_optionst::help()
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     "\n";
+  // clang-format on
 }

src/common

@@ -227,12 +227,40 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
 %.obj:%.c
 	$(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@
 
+# get version from git
+GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
+GIT_INFO_FILE = .release_info
+
+CBMC_VERSION_FILES += $(filter %_parse_options$(OBJEXT), $(OBJ))
+
+ifeq ($(BUILD_ENV_),MSVC)
+$(CBMC_VERSION_FILES): CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+$(CBMC_VERSION_FILES): CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
+# Use make >= 4.0's `file` function, if available - it should be faster than
+# `shell cat`
+ifeq ($(firstword $(subst ., , $(MAKE_VERSION))), 3)
+KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
+else
+KNOWN_RELEASE_INFO = $(file < $(GIT_INFO_FILE))
+endif
+ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO))
+$(CBMC_VERSION_FILES): $(GIT_INFO_FILE)
+
+$(GIT_INFO_FILE):
+	echo $(GIT_INFO) > $@
+
+.PHONY: $(GIT_INFO_FILE)
+endif
+
 clean:
 	$(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
 		$(patsubst %.cpp, %$(DEPEXT), $(filter %.cpp, $(SRC))) \
 		$(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
 		$(patsubst %.cc, %$(DEPEXT), $(filter %.cc, $(SRC))) \
-		$(CLEANFILES)
+		$(CLEANFILES) $(GIT_INFO_FILE)
 
 .PHONY: first_target clean all
 .PHONY: sources generated_files
@@ -252,4 +280,3 @@ D_FILES1 = $(SRC:.c=$(DEPEXT))
 D_FILES = $(D_FILES1:.cpp=$(DEPEXT))
 
 -include $(D_FILES)
-

src/config.inc

@@ -70,3 +70,6 @@ endif
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"
+
+# Detailed version information
+CBMC_VERSION = 5.8

src/goto-analyzer/CMakeLists.txt

@@ -26,3 +26,6 @@ add_if_library(goto-analyzer-lib jsil)
 # Executable
 add_executable(goto-analyzer goto_analyzer_main.cpp)
 target_link_libraries(goto-analyzer goto-analyzer-lib)
+
+set(cbmc_version_files goto_analyzer_parse_options.cpp)
+git_revision(goto-analyzer-lib cbmc_version_files)

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -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"
@@ -790,15 +789,10 @@ bool goto_analyzer_parse_optionst::process_goto_program(
 /// display command line help
 void goto_analyzer_parse_optionst::help()
 {
-  std::cout << "\n"
-               "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << " * *\n";
-
   // clang-format off
-  std::cout <<
+  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
+            <<
+    "* *                   Copyright (C) 2017-2018                    * *\n"
     "* *                  Daniel Kroening, DiffBlue                   * *\n"
     "* *                   [email protected]                      * *\n"
     "\n"

src/goto-analyzer/module_dependencies.txt

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

src/goto-cc/CMakeLists.txt

@@ -34,3 +34,6 @@ else()
     COMMAND "${CMAKE_COMMAND}" -E create_symlink
       goto-cc $<TARGET_FILE_DIR:goto-cc>/goto-gcc)
 endif()
+
+set(cbmc_version_files as_mode.cpp compile.cpp gcc_mode.cpp goto_cc_mode.cpp)
+git_revision(goto-cc-lib cbmc_version_files)