move version.h 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,15 +49,14 @@ Author: Daniel Kroening, [email protected]
 #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),

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, [email protected]
 #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, [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

@@ -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, [email protected]
 #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, [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),

src/cbmc/cbmc_solvers.cpp

@@ -15,8 +15,9 @@ Author: Daniel Kroening, [email protected]
 #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, [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

@@ -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, [email protected]
 #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, [email protected]
 
 #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, [email protected]
 
 #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, [email protected]
 #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/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,

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/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,

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)