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

Daniel Kroening · Daniel Kroening · commit 2f3a4af63172 · 2018-07-03T12:53:49.000+01:00
diff --git a/CMakeLists.txt b/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)
diff --git a/jbmc/src/janalyzer/CMakeLists.txt b/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)
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -49,15 +49,14 @@ 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>
 #include <goto-analyzer/static_verifier.h>
 #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),
diff --git a/jbmc/src/jbmc/CMakeLists.txt b/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)
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/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),
diff --git a/jbmc/src/jdiff/CMakeLists.txt b/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)
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/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),
diff --git a/src/cbmc/CMakeLists.txt b/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)
diff --git a/src/cbmc/Makefile b/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
diff --git a/src/clobber/CMakeLists.txt b/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)
diff --git a/src/common b/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
diff --git a/src/goto-analyzer/CMakeLists.txt b/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)
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/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,
diff --git a/src/goto-cc/CMakeLists.txt b/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)
diff --git a/src/goto-cc/Makefile b/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
diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp
@@ -23,14 +23,14 @@ Author: Michael Tautschnig
 #include <iostream>
 #include <cstring>
 
-#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/get_base_name.h>
+#include <util/run.h>
+#include <util/tempdir.h>
+#include <util/version.h>
 
 #include "compile.h"
-#include "version.h"
 
 static std::string assembler_name(
   const cmdlinet &cmdline,
diff --git a/src/goto-cc/compile.cpp b/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
diff --git a/src/goto-cc/gcc_mode.cpp b/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/invariant.h>
-#include <util/tempdir.h>
-#include <util/tempfile.h>
+#include <util/c_types.h>
 #include <util/config.h>
-#include <util/prefix.h>
-#include <util/suffix.h>
+#include <util/expr.h>
 #include <util/get_base_name.h>
-#include <util/run.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/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,
diff --git a/src/goto-cc/goto_cc_mode.cpp b/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(
diff --git a/src/goto-diff/CMakeLists.txt b/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)
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/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),
diff --git a/src/goto-instrument/CMakeLists.txt b/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)
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/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()
diff --git a/src/memory-models/CMakeLists.txt b/src/memory-models/CMakeLists.txt
@@ -11,5 +11,3 @@ add_library(mmcc
 generic_includes(mmcc)
 
 target_link_libraries(mmcc util)
-
-git_revision(mmcc)
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
diff --git a/src/util/Makefile b/src/util/Makefile
