move build commands for version.h from common to util/

CMakeLists.txt

@@ -39,48 +39,6 @@ if(${enable_cbmc_tests})
     enable_testing()
 endif()
 
-# based on https://cmake.org/pipermail/cmake/2010-July/038015.html
-find_package(Git)
-if(GIT_FOUND)
-  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
-    "
-    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
-      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
-    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
-    execute_process(
-      COMMAND \"${GIT_EXECUTABLE}\" \"describe\" \"--tags\" \"--always\" \"--dirty\"
-      OUTPUT_VARIABLE GIT_INFO
-      OUTPUT_STRIP_TRAILING_WHITESPACE
-    )
-    configure_file(\${CUR}/version.h.in version.h)
-    "
-  )
-else()
-  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
-    "
-    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
-      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
-    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
-    set(GIT_INFO \"n/a\")
-    configure_file(\${CUR}/version.h.in version.h)
-    "
-  )
-endif()
-
-macro(git_revision target)
-  file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.h.in
-    "\#define CBMC_VERSION \"@CBMC_RELEASE@ (@GIT_INFO@)\"\n")
-  add_custom_target(
-    ${target}-version.h
-    COMMAND ${CMAKE_COMMAND}
-      -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR}
-      -D CUR=${CMAKE_CURRENT_BINARY_DIR}
-      -P ${CMAKE_BINARY_DIR}/version.cmake
-  )
- add_dependencies(${target} ${target}-version.h)
-endmacro()
-include_directories(${CMAKE_CURRENT_BINARY_DIR})
-
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)

jbmc/src/janalyzer/CMakeLists.txt

@@ -24,5 +24,3 @@ target_link_libraries(janalyzer-lib
 # Executable
 add_executable(janalyzer janalyzer_main.cpp)
 target_link_libraries(janalyzer janalyzer-lib)
-
-git_revision(janalyzer-lib)

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -49,6 +49,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exit_codes.h>
 #include <util/options.h>
 #include <util/unicode.h>
+#include <util/version.h>
 
 #include <goto-analyzer/static_show_domain.h>
 #include <goto-analyzer/static_simplifier.h>
@@ -56,8 +57,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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

@@ -29,5 +29,3 @@ target_link_libraries(jbmc-lib
 # Executable
 add_executable(jbmc jbmc_main.cpp)
 target_link_libraries(jbmc jbmc-lib)
-
-git_revision(jbmc-lib)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -16,10 +16,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <memory>
 
-#include <util/exit_codes.h>
 #include <util/config.h>
-#include <util/unicode.h>
+#include <util/exit_codes.h>
 #include <util/invariant.h>
+#include <util/unicode.h>
+#include <util/version.h>
 
 #include <langapi/language.h>
 
@@ -60,8 +61,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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

@@ -26,5 +26,3 @@ target_link_libraries(jdiff-lib
 # Executable
 add_executable(jdiff jdiff_main.cpp)
 target_link_libraries(jdiff jdiff-lib)
-
-git_revision(jdiff-lib)

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -20,6 +20,7 @@ Author: Peter Schrammel
 #include <util/exit_codes.h>
 #include <util/make_unique.h>
 #include <util/options.h>
+#include <util/version.h>
 
 #include <langapi/language.h>
 
@@ -60,8 +61,6 @@ 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

@@ -31,5 +31,3 @@ add_if_library(cbmc-lib jsil)
 # Executable
 add_executable(cbmc cbmc_main.cpp)
 target_link_libraries(cbmc cbmc-lib)
-
-git_revision(cbmc-lib)

src/cbmc/Makefile

@@ -63,8 +63,6 @@ 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

@@ -17,9 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/config.h>
-#include <util/unicode.h>
-#include <util/invariant.h>
 #include <util/exit_codes.h>
+#include <util/invariant.h>
+#include <util/unicode.h>
+#include <util/version.h>
 
 #include <langapi/language.h>
 
@@ -64,8 +65,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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),

src/cbmc/cbmc_solvers.cpp

@@ -15,8 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <memory>
 
-#include <util/unicode.h>
 #include <util/make_unique.h>
+#include <util/unicode.h>
+#include <util/version.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
@@ -28,7 +29,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.

src/clobber/CMakeLists.txt

@@ -29,5 +29,3 @@ add_if_library(clobber-lib bv_refinement)
 # Executable
 add_executable(clobber clobber_main.cpp)
 target_link_libraries(clobber clobber-lib)
-
-git_revision(clobber-lib)

src/clobber/clobber_parse_options.cpp

@@ -16,8 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cstdlib>
 
 #include <util/config.h>
-#include <util/options.h>
 #include <util/memory_info.h>
+#include <util/options.h>
+#include <util/version.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
@@ -34,8 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
-#include "version.h"
-
 clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
   parse_options_baset(CLOBBER_OPTIONS, argc, argv),
   language_uit(cmdline, ui_message_handler),

src/common

@@ -227,29 +227,12 @@ 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")
-RELEASE_INFO = \#define CBMC_VERSION "$(CBMC_VERSION) ($(GIT_INFO))"
-GIT_INFO_FILE = version.h
-
-$(GIT_INFO_FILE):
-	echo '$(RELEASE_INFO)' > $@
-
-$(filter %_parse_options$(OBJEXT), $(OBJ)): $(GIT_INFO_FILE)
-
-# mark the actually generated file as a phony target to enforce a rebuild - but
-# only of the version information has changed!
-KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
-ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_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) $(GIT_INFO_FILE)
+		$(CLEANFILES)
 
 .PHONY: first_target clean all
 .PHONY: sources generated_files

src/goto-analyzer/CMakeLists.txt

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

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -24,20 +24,21 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <jsil/jsil_language.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/set_properties.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
-#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_asm.h>
-#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/link_to_library.h>
 
 #include <analyses/is_threaded.h>
 #include <analyses/goto_check.h>
@@ -49,19 +50,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/mode.h>
 #include <langapi/language.h>
 
-#include <util/options.h>
 #include <util/config.h>
-#include <util/unicode.h>
 #include <util/exit_codes.h>
-
-#include <goto-programs/adjust_float_expressions.h>
+#include <util/options.h>
+#include <util/unicode.h>
+#include <util/version.h>
 
 #include "taint_analysis.h"
 #include "unreachable_instructions.h"
 #include "static_show_domain.h"
 #include "static_simplifier.h"
 #include "static_verifier.h"
-#include "version.h"
 
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,

src/goto-cc/CMakeLists.txt

@@ -34,5 +34,3 @@ else()
     COMMAND "${CMAKE_COMMAND}" -E create_symlink
       goto-cc $<TARGET_FILE_DIR:goto-cc>/goto-gcc)
 endif()
-
-git_revision(goto-cc-lib)

src/goto-cc/Makefile

@@ -46,8 +46,6 @@ all: goto-cl$(EXEEXT)
 endif
 all: goto-cc$(EXEEXT)
 
-as_mode$(OBJEXT) compile$(OBJEXT) gcc_mode$(OBJEXT) goto_cc_mode$(OBJEXT): $(GIT_INFO_FILE)
-
 ifneq ($(wildcard ../jsil/Makefile),)
   OBJ += ../jsil/jsil$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JSIL

src/goto-cc/as_mode.cpp

@@ -23,14 +23,14 @@ Author: Michael Tautschnig
 #include <iostream>
 #include <cstring>
 
+#include <util/config.h>
+#include <util/cout_message.h>
+#include <util/get_base_name.h>
 #include <util/run.h>
 #include <util/tempdir.h>
-#include <util/config.h>
-#include <util/get_base_name.h>
-#include <util/cout_message.h>
+#include <util/version.h>
 
 #include "compile.h"
-#include "version.h"
 
 static std::string assembler_name(
   const cmdlinet &cmdline,

src/goto-cc/compile.cpp

@@ -24,6 +24,7 @@ Date: June 2006
 #include <util/suffix.h>
 #include <util/tempdir.h>
 #include <util/unicode.h>
+#include <util/version.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/ansi_c_entry_point.h>
@@ -63,8 +64,6 @@ Date: June 2006
 #define pclose _pclose
 #endif
 
-#include "version.h"
-
 /// reads and source and object files, compiles and links them into goto program
 /// objects.
 /// \return true on error, false otherwise

src/goto-cc/gcc_mode.cpp

@@ -31,24 +31,24 @@ Author: CM Wintersteiger, 2006
 
 #include <json/json_parser.h>
 
-#include <util/expr.h>
-#include <util/c_types.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/config.h>
+#include <util/expr.h>
+#include <util/get_base_name.h>
 #include <util/invariant.h>
+#include <util/prefix.h>
+#include <util/replace_symbol.h>
+#include <util/run.h>
+#include <util/suffix.h>
 #include <util/tempdir.h>
 #include <util/tempfile.h>
-#include <util/config.h>
-#include <util/prefix.h>
-#include <util/suffix.h>
-#include <util/get_base_name.h>
-#include <util/run.h>
-#include <util/replace_symbol.h>
+#include <util/version.h>
 
 #include <goto-programs/read_goto_binary.h>
 
 #include "hybrid_binary.h"
 #include "linker_script_merge.h"
-#include "version.h"
 
 static std::string compiler_name(
   const cmdlinet &cmdline,

src/goto-cc/goto_cc_mode.cpp

@@ -23,8 +23,7 @@ Author: CM Wintersteiger, 2006
 #endif
 
 #include <util/parse_options.h>
-
-#include "version.h"
+#include <util/version.h>
 
 /// constructor
 goto_cc_modet::goto_cc_modet(

src/goto-diff/CMakeLists.txt

@@ -28,5 +28,3 @@ add_if_library(goto-diff-lib jsil)
 # Executable
 add_executable(goto-diff goto_diff_main.cpp)
 target_link_libraries(goto-diff goto-diff-lib)
-
-git_revision(goto-diff-lib)

src/goto-diff/goto_diff_parse_options.cpp

@@ -17,9 +17,10 @@ Author: Peter Schrammel
 #include <memory>
 
 #include <util/config.h>
-#include <util/options.h>
-#include <util/make_unique.h>
 #include <util/exit_codes.h>
+#include <util/make_unique.h>
+#include <util/options.h>
+#include <util/version.h>
 
 #include <langapi/language.h>
 
@@ -59,7 +60,6 @@ Author: Peter Schrammel
 #include "syntactic_diff.h"
 #include "unified_diff.h"
 #include "change_impact.h"
-#include "version.h"
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),

src/goto-instrument/CMakeLists.txt

@@ -29,5 +29,3 @@ add_if_library(goto-instrument-lib glpk)
 # Executable
 add_executable(goto-instrument goto_instrument_main.cpp)
 target_link_libraries(goto-instrument goto-instrument-lib)
-
-git_revision(goto-instrument-lib)

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -16,10 +16,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/config.h>
+#include <util/exit_codes.h>
+#include <util/json.h>
 #include <util/string2int.h>
 #include <util/unicode.h>
-#include <util/json.h>
-#include <util/exit_codes.h>
+#include <util/version.h>
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_convert_functions.h>
@@ -99,7 +100,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "undefined_functions.h"
 #include "remove_function.h"
 #include "splice_call.h"
-#include "version.h"
 
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()

src/memory-models/CMakeLists.txt

@@ -11,5 +11,3 @@ add_library(mmcc
 generic_includes(mmcc)
 
 target_link_libraries(mmcc util)
-
-git_revision(mmcc)

src/memory-models/mmcc_parse_options.cpp

@@ -15,10 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 
 #include <util/cout_message.h>
+#include <util/version.h>
 
 #include "mm_parser.h"
 #include "mm2cpp.h"
-#include "version.h"
 
 mmcc_parse_optionst::mmcc_parse_optionst(int argc, const char **argv):
   parse_options_baset(MMCC_OPTIONS, argc, argv)

src/util/CMakeLists.txt

@@ -4,3 +4,42 @@ add_library(util ${sources})
 generic_includes(util)
 
 target_link_libraries(util big-int langapi)
+
+# based on https://cmake.org/pipermail/cmake/2010-July/038015.html
+find_package(Git)
+if(GIT_FOUND)
+  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
+    "
+    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
+    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
+    execute_process(
+      COMMAND \"${GIT_EXECUTABLE}\" \"describe\" \"--tags\" \"--always\" \"--dirty\"
+      OUTPUT_VARIABLE GIT_INFO
+      OUTPUT_STRIP_TRAILING_WHITESPACE
+    )
+    configure_file(\${CUR}/version.h.in version.h)
+    "
+  )
+else()
+  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
+    "
+    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
+    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
+    set(GIT_INFO \"n/a\")
+    configure_file(\${CUR}/version.h.in version.h)
+    "
+  )
+endif()
+
+file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.h.in
+  "\#define CBMC_VERSION \"@CBMC_RELEASE@ (@GIT_INFO@)\"\n")
+add_custom_target(
+  version.h
+  COMMAND ${CMAKE_COMMAND}
+    -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR}
+    -D CUR=${CMAKE_CURRENT_BINARY_DIR}
+    -P ${CMAKE_BINARY_DIR}/version.cmake
+)
+add_dependencies(util version.h)

src/util/Makefile

@@ -103,9 +103,26 @@ INCLUDES= -I ..
 include ../config.inc
 include ../common
 
-CLEANFILES = util$(LIBEXT)
+# get version from git
+GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
+RELEASE_INFO = \#define CBMC_VERSION "$(CBMC_VERSION) ($(GIT_INFO))"
+GIT_INFO_FILE = version.h
 
-all: util$(LIBEXT)
+$(GIT_INFO_FILE):
+	echo '$(RELEASE_INFO)' > $@
+
+generated_files: $(GIT_INFO_FILE)
+
+# mark the actually generated file as a phony target to enforce a rebuild - but
+# only if the version information has changed!
+KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
+ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO))
+.PHONY: $(GIT_INFO_FILE)
+endif
+
+CLEANFILES = $(GIT_INFO_FILE) util$(LIBEXT)
+
+all: util$(LIBEXT) $(GIT_INFO_FILE)
 
 util$(LIBEXT): $(OBJ)
 	$(LINKLIB)