Merge pull request #2373 from tautschnig/git-version-output

Include git revision in version output

Author: kroening

.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, 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>
@@ -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"
     "* *                   kroening@kroening.com                      * *\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, 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),
@@ -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"
     "* *                 kroening@kroening.com                   * *\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"
     "* *                 kroening@kroening.com                   * *\n"
     "\n"