diff --git a/.gitignore b/.gitignore index e751bb0f4da..adc42985353 100644 --- a/.gitignore +++ b/.gitignore @@ -28,7 +28,7 @@ Release/* *.obj *.a *.lib -.release_info +version.h src/ansi-c/arm_builtin_headers.inc src/ansi-c/clang_builtin_headers.inc src/ansi-c/cprover_builtin_headers.inc diff --git a/CMakeLists.txt b/CMakeLists.txt index 2516d4c19de..ed952e80190 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -17,6 +17,7 @@ set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR + "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang" OR "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" ) # Ensure NDEBUG is not set for release builds @@ -38,51 +39,47 @@ 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}") - +# 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 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" +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 ) - 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_CURRENT_BINARY_DIR}) add_subdirectory(src) add_subdirectory(regression) diff --git a/jbmc/src/janalyzer/CMakeLists.txt b/jbmc/src/janalyzer/CMakeLists.txt index dfb42b409f8..a9fcbe725a8 100644 --- a/jbmc/src/janalyzer/CMakeLists.txt +++ b/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) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index d8daccfd60f..32299505d7a 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -56,6 +56,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#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 index 706797abbcc..b6a6a266fb7 100644 --- a/jbmc/src/jbmc/CMakeLists.txt +++ b/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) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 2869050ffcb..a36b61d4757 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -60,6 +60,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#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 index 04d6122e95e..ee861db2daa 100644 --- a/jbmc/src/jdiff/CMakeLists.txt +++ b/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) diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 1f4e875ab2f..9eaee6b0cf3 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -60,6 +60,8 @@ Author: Peter Schrammel #include #include +#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 index e3b69f6daf0..a9deb883d16 100644 --- a/src/cbmc/CMakeLists.txt +++ b/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) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index a00997b7531..996a0901bdc 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -56,8 +56,6 @@ INCLUDES= -I .. LIBS = -CBMC_VERSION_FILES = cbmc_solvers$(OBJEXT) - include ../config.inc include ../common @@ -65,6 +63,8 @@ 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/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 4bc131fab38..b5ea4553f17 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -64,6 +64,8 @@ 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), diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index da9f28b8c36..8b216839f92 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -28,6 +28,7 @@ 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. diff --git a/src/clobber/CMakeLists.txt b/src/clobber/CMakeLists.txt index 02194f9511e..e3dbd108a09 100644 --- a/src/clobber/CMakeLists.txt +++ b/src/clobber/CMakeLists.txt @@ -30,5 +30,4 @@ add_if_library(clobber-lib bv_refinement) add_executable(clobber clobber_main.cpp) target_link_libraries(clobber clobber-lib) -set(cbmc_version_files clobber_parse_options.cpp) -git_revision(clobber-lib cbmc_version_files) +git_revision(clobber-lib) diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 715cd0b4acb..57d2e142c4f 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "version.h" clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv): parse_options_baset(CLOBBER_OPTIONS, argc, argv), diff --git a/src/common b/src/common index 5586bf8f937..e69f47cabd3 100644 --- a/src/common +++ b/src/common @@ -229,23 +229,18 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) # get version from git GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") -GIT_INFO_FILE = .release_info +RELEASE_INFO = \#define CBMC_VERSION "$(CBMC_VERSION) ($(GIT_INFO))" +GIT_INFO_FILE = version.h -CBMC_VERSION_FILES += $(filter %_parse_options$(OBJEXT), $(OBJ)) +$(GIT_INFO_FILE): + echo '$(RELEASE_INFO)' > $@ -ifeq ($(BUILD_ENV_),MSVC) -$(CBMC_VERSION_FILES): CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' -else -$(CBMC_VERSION_FILES): CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" -endif +$(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 ($(GIT_INFO), $(KNOWN_RELEASE_INFO)) -$(CBMC_VERSION_FILES): $(GIT_INFO_FILE) - -$(GIT_INFO_FILE): - echo $(GIT_INFO) > $@ - +ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO)) .PHONY: $(GIT_INFO_FILE) endif diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt index a2373d2138a..86e39f073dc 100644 --- a/src/goto-analyzer/CMakeLists.txt +++ b/src/goto-analyzer/CMakeLists.txt @@ -27,5 +27,4 @@ add_if_library(goto-analyzer-lib jsil) add_executable(goto-analyzer goto_analyzer_main.cpp) target_link_libraries(goto-analyzer goto-analyzer-lib) -set(cbmc_version_files goto_analyzer_parse_options.cpp) -git_revision(goto-analyzer-lib cbmc_version_files) +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 index b7bede4b04d..4593d3eb642 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -61,6 +61,7 @@ Author: Daniel Kroening, kroening@kroening.com #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 index 504f54a8ea6..a2562caf92b 100644 --- a/src/goto-cc/CMakeLists.txt +++ b/src/goto-cc/CMakeLists.txt @@ -35,5 +35,4 @@ else() goto-cc $/goto-gcc) endif() -set(cbmc_version_files as_mode.cpp compile.cpp gcc_mode.cpp goto_cc_mode.cpp) -git_revision(goto-cc-lib cbmc_version_files) +git_revision(goto-cc-lib) diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 976cc339d77..25ee6514b42 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -38,11 +38,6 @@ LIBS = CLEANFILES = goto-cc$(EXEEXT) goto-cl$(EXEEXT) -CBMC_VERSION_FILES = as_mode$(OBJEXT) \ - compile$(OBJEXT) \ - gcc_mode$(OBJEXT) \ - goto_cc_mode$(OBJEXT) - include ../config.inc include ../common @@ -51,6 +46,8 @@ 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 index b7796e945c0..13ace1c5b80 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -30,6 +30,7 @@ Author: Michael Tautschnig #include #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 index 671de8d5893..e51d324cecc 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -63,6 +63,8 @@ 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 index 143465ac278..42b09a83cb7 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -48,6 +48,7 @@ Author: CM Wintersteiger, 2006 #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 index d42201c4a50..c50b404c023 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -24,6 +24,8 @@ Author: CM Wintersteiger, 2006 #include +#include "version.h" + /// constructor goto_cc_modet::goto_cc_modet( goto_cc_cmdlinet &_cmdline, diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index 43dd2fc88da..ac09c817587 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -29,5 +29,4 @@ add_if_library(goto-diff-lib jsil) add_executable(goto-diff goto_diff_main.cpp) target_link_libraries(goto-diff goto-diff-lib) -set(cbmc_version_files goto_diff_parse_options.cpp) -git_revision(goto-diff-lib cbmc_version_files) +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 index 1a6c82240f4..05c67a7424e 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -59,6 +59,7 @@ 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 index 225fa1200ea..42827ef12f0 100644 --- a/src/goto-instrument/CMakeLists.txt +++ b/src/goto-instrument/CMakeLists.txt @@ -33,5 +33,4 @@ add_if_library(goto-instrument-lib glpk) add_executable(goto-instrument goto_instrument_main.cpp) target_link_libraries(goto-instrument goto-instrument-lib) -set(cbmc_version_files "goto_instrument_parse_options.cpp") -git_revision(goto-instrument-lib cbmc_version_files) +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 index 9afe3be526c..134ef0ab953 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -98,6 +98,7 @@ 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 index 4fc92ff6f12..8378dca8968 100644 --- a/src/memory-models/CMakeLists.txt +++ b/src/memory-models/CMakeLists.txt @@ -12,5 +12,4 @@ generic_includes(mmcc) target_link_libraries(mmcc util) -set(cbmc_version_files mmcc_parse_options.cpp) -git_revision(mmcc cbmc_version_files) +git_revision(mmcc) diff --git a/src/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp index d0c7dcbbc94..d992eb8e654 100644 --- a/src/memory-models/mmcc_parse_options.cpp +++ b/src/memory-models/mmcc_parse_options.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #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)