Skip to content

Commit e638f72

Browse files
committed
CBMC_VERSION: Use generated include files instead of command-line defines
Also fixes a number of shortcomings of the earlier approach as far as CMake is concerned: - Adds --dirty to the git command line (as is done for Makefiles). - Does not require a rebuild when there are no changes to the version string. - CBMC release number updates will be reflected and trigger a rebuild (even when no other changes have taken place).
1 parent 1360f7f commit e638f72

29 files changed

+80
-83
lines changed

.gitignore

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Release/*
2828
*.obj
2929
*.a
3030
*.lib
31-
.release_info
31+
version.h
3232
src/ansi-c/arm_builtin_headers.inc
3333
src/ansi-c/clang_builtin_headers.inc
3434
src/ansi-c/cprover_builtin_headers.inc

CMakeLists.txt

Lines changed: 37 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -39,52 +39,47 @@ if(${enable_cbmc_tests})
3939
enable_testing()
4040
endif()
4141

42-
file(STRINGS src/config.inc config_inc_v REGEX "CBMC_VERSION *= *[0-9\.]+")
43-
string(REGEX REPLACE "^CBMC_VERSION *= *" "" CBMC_RELEASE ${config_inc_v})
44-
message(STATUS "CBMC release ${CBMC_RELEASE}")
45-
42+
# based on https://cmake.org/pipermail/cmake/2010-July/038015.html
4643
find_package(Git)
44+
if(GIT_FOUND)
45+
file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
46+
"
47+
file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
48+
config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
49+
string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
50+
execute_process(
51+
COMMAND \"${GIT_EXECUTABLE}\" \"describe\" \"--tags\" \"--always\" \"--dirty\"
52+
OUTPUT_VARIABLE GIT_INFO
53+
OUTPUT_STRIP_TRAILING_WHITESPACE
54+
)
55+
configure_file(\${CUR}/version.h.in version.h)
56+
"
57+
)
58+
else()
59+
file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
60+
"
61+
file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
62+
config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
63+
string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
64+
set(GIT_INFO \"n/a\")
65+
configure_file(\${CUR}/version.h.in version.h)
66+
"
67+
)
68+
endif()
4769

48-
macro(git_revision target files_var)
49-
if(GIT_FOUND)
50-
add_custom_command(
51-
OUTPUT .release_info
52-
COMMAND ${CMAKE_COMMAND} -E echo_append "#define __CBMC_VERSION " > .release_info
53-
COMMAND "${GIT_EXECUTABLE}" "describe" "--tags" "--always" "--long" >> .release_info
54-
COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_str(v) \"${CBMC_RELEASE} (\" # v \")\"" >> .release_info
55-
COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_xstr(v) __CBMC_VERSION_str(v)" >> .release_info
56-
COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION __CBMC_VERSION_xstr(__CBMC_VERSION)" >> .release_info
57-
VERBATIM
58-
)
59-
add_custom_command(
60-
TARGET ${target}
61-
POST_BUILD
62-
COMMAND ${CMAKE_COMMAND} -E remove -f .release_info
63-
)
64-
else()
65-
add_custom_command(
66-
OUTPUT .release_info
67-
COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION \"${CBMC_RELEASE} (n/a)\"" >> .release_info
68-
VERBATIM
69-
)
70-
endif()
71-
72-
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
73-
"${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang" OR
74-
"${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
70+
macro(git_revision target)
71+
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.h.in
72+
"\#define CBMC_VERSION \"@CBMC_RELEASE@ (@GIT_INFO@)\"\n")
73+
add_custom_target(
74+
${target}-version.h
75+
COMMAND ${CMAKE_COMMAND}
76+
-D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR}
77+
-D CUR=${CMAKE_CURRENT_BINARY_DIR}
78+
-P ${CMAKE_BINARY_DIR}/version.cmake
7579
)
76-
set_source_files_properties(
77-
${${files_var}}
78-
PROPERTIES
79-
OBJECT_DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/.release_info
80-
COMPILE_FLAGS "-include .release_info")
81-
elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
82-
set_source_files_properties(
83-
${${files_var}}
84-
PROPERTIES
85-
COMPILE_FLAGS "/DCBMC_VERSION=\"${CBMC_RELEASE} (n/a)\"")
86-
endif()
80+
add_dependencies(${target} ${target}-version.h)
8781
endmacro()
82+
include_directories(${CMAKE_CURRENT_BINARY_DIR})
8883

8984
add_subdirectory(src)
9085
add_subdirectory(regression)

jbmc/src/janalyzer/CMakeLists.txt

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,5 +25,4 @@ target_link_libraries(janalyzer-lib
2525
add_executable(janalyzer janalyzer_main.cpp)
2626
target_link_libraries(janalyzer janalyzer-lib)
2727

28-
set(cbmc_version_files janalyzer_parse_options.cpp)
29-
git_revision(janalyzer-lib cbmc_version_files)
28+
git_revision(janalyzer-lib)

jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,8 @@ Author: Daniel Kroening, kroening@kroening.com
5656
#include <goto-analyzer/taint_analysis.h>
5757
#include <goto-analyzer/unreachable_instructions.h>
5858

59+
#include "version.h"
60+
5961
janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
6062
: parse_options_baset(JANALYZER_OPTIONS, argc, argv),
6163
messaget(ui_message_handler),

jbmc/src/jbmc/CMakeLists.txt

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,5 +30,4 @@ target_link_libraries(jbmc-lib
3030
add_executable(jbmc jbmc_main.cpp)
3131
target_link_libraries(jbmc jbmc-lib)
3232

33-
set(cbmc_version_files jbmc_parse_options.cpp)
34-
git_revision(jbmc-lib cbmc_version_files)
33+
git_revision(jbmc-lib)

jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@ Author: Daniel Kroening, kroening@kroening.com
6060
#include <java_bytecode/replace_java_nondet.h>
6161
#include <java_bytecode/simple_method_stubbing.h>
6262

63+
#include "version.h"
64+
6365
jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
6466
parse_options_baset(JBMC_OPTIONS, argc, argv),
6567
messaget(ui_message_handler),

jbmc/src/jdiff/CMakeLists.txt

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,5 +27,4 @@ target_link_libraries(jdiff-lib
2727
add_executable(jdiff jdiff_main.cpp)
2828
target_link_libraries(jdiff jdiff-lib)
2929

30-
set(cbmc_version_files jdiff_parse_options.cpp)
31-
git_revision(jdiff-lib cbmc_version_files)
30+
git_revision(jdiff-lib)

jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@ Author: Peter Schrammel
6060
#include <goto-diff/goto_diff.h>
6161
#include <goto-diff/unified_diff.h>
6262

63+
#include "version.h"
64+
6365
jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
6466
: parse_options_baset(JDIFF_OPTIONS, argc, argv),
6567
jdiff_languagest(cmdline, ui_message_handler),

src/cbmc/CMakeLists.txt

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,5 +32,4 @@ add_if_library(cbmc-lib jsil)
3232
add_executable(cbmc cbmc_main.cpp)
3333
target_link_libraries(cbmc cbmc-lib)
3434

35-
set(cbmc_version_files cbmc_parse_options.cpp cbmc_solvers.cpp)
36-
git_revision(cbmc-lib cbmc_version_files)
35+
git_revision(cbmc-lib)

src/cbmc/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,15 +56,15 @@ INCLUDES= -I ..
5656

5757
LIBS =
5858

59-
CBMC_VERSION_FILES = cbmc_solvers$(OBJEXT)
60-
6159
include ../config.inc
6260
include ../common
6361

6462
CLEANFILES = cbmc$(EXEEXT)
6563

6664
all: cbmc$(EXEEXT)
6765

66+
cbmc_solvers$(OBJEXT): $(GIT_INFO_FILE)
67+
6868
ifneq ($(wildcard ../bv_refinement/Makefile),)
6969
OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
7070
CP_CXXFLAGS += -DHAVE_BV_REFINEMENT

0 commit comments

Comments
 (0)