CBMC_VERSION: Use generated include files instead of command-line defines

Author: tautschnig

CMakeLists.txt

@@ -44,47 +44,27 @@ 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)
+macro(git_revision target)
   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
+    add_custom_target(
+      ${target}-version.h
+      COMMAND ${CMAKE_COMMAND} -E echo_append "#define __CBMC_VERSION " > version.h
+      COMMAND "${GIT_EXECUTABLE}" "describe" "--tags" "--always" "--long" >> version.h
+      COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_str(v) \"${CBMC_RELEASE} (\" # v \")\"" >> version.h
+      COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_xstr(v) __CBMC_VERSION_str(v)" >> version.h
+      COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION __CBMC_VERSION_xstr(__CBMC_VERSION)" >> version.h
       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
+    add_custom_target(
+      ${target}-version.h
+      COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION \"${CBMC_RELEASE} (n/a)\"" >> version.h
       VERBATIM
       )
   endif()
-
-  if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
-     "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang" 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()
+  add_dependencies(${target} ${target}-version.h)
 endmacro()
+include_directories(${CMAKE_BINARY_DIR})
 
 add_subdirectory(src)
 add_subdirectory(regression)

jbmc/src/janalyzer/CMakeLists.txt

@@ -25,5 +25,4 @@ target_link_libraries(janalyzer-lib
 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)
+git_revision(janalyzer-lib)

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -56,6 +56,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-analyzer/taint_analysis.h>
 #include <goto-analyzer/unreachable_instructions.h>
 
+#include "version.h"
+
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JANALYZER_OPTIONS, argc, argv),
     messaget(ui_message_handler),

jbmc/src/jbmc/CMakeLists.txt

@@ -30,5 +30,4 @@ target_link_libraries(jbmc-lib
 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)
+git_revision(jbmc-lib)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -60,6 +60,8 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/replace_java_nondet.h>
 #include <java_bytecode/simple_method_stubbing.h>
 
+#include "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/jdiff/CMakeLists.txt

@@ -27,5 +27,4 @@ target_link_libraries(jdiff-lib
 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)
+git_revision(jdiff-lib)

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -60,6 +60,8 @@ Author: Peter Schrammel
 #include <goto-diff/goto_diff.h>
 #include <goto-diff/unified_diff.h>
 
+#include "version.h"
+
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JDIFF_OPTIONS, argc, argv),
     jdiff_languagest(cmdline, ui_message_handler),

src/cbmc/CMakeLists.txt

@@ -32,5 +32,4 @@ add_if_library(cbmc-lib jsil)
 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)
+git_revision(cbmc-lib)

src/cbmc/Makefile

@@ -56,15 +56,15 @@ INCLUDES= -I ..
 
 LIBS =
 
-CBMC_VERSION_FILES = cbmc_solvers$(OBJEXT)
-
 include ../config.inc
 include ../common
 
 CLEANFILES = cbmc$(EXEEXT)
 
 all: cbmc$(EXEEXT)
 
+cbmc_solvers$(OBJEXT): $(GIT_INFO_FILE)
+
 ifneq ($(wildcard ../bv_refinement/Makefile),)
   OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT

src/cbmc/cbmc_parse_options.cpp

@@ -64,6 +64,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "xml_interface.h"
 
+#include "version.h"
+
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),