Skip to content

Commit ca982a5

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#2373 from tautschnig/git-version-output
Include git revision in version output
2 parents af880a4 + 4b124c8 commit ca982a5

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+173
-114
lines changed

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ Release/*
2828
*.obj
2929
*.a
3030
*.lib
31+
.release_info
3132
src/ansi-c/arm_builtin_headers.inc
3233
src/ansi-c/clang_builtin_headers.inc
3334
src/ansi-c/cprover_builtin_headers.inc

‎CMakeLists.txt

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,52 @@ if(${enable_cbmc_tests})
3838
enable_testing()
3939
endif()
4040

41+
file(STRINGS src/config.inc config_inc_v REGEX "CBMC_VERSION *= *[0-9\.]+")
42+
string(REGEX REPLACE "^CBMC_VERSION *= *" "" CBMC_RELEASE ${config_inc_v})
43+
message(STATUS "CBMC release ${CBMC_RELEASE}")
44+
45+
find_package(Git)
46+
47+
macro(git_revision target files_var)
48+
if(GIT_FOUND)
49+
add_custom_command(
50+
OUTPUT .release_info
51+
COMMAND ${CMAKE_COMMAND} -E echo_append "#define __CBMC_VERSION " > .release_info
52+
COMMAND "${GIT_EXECUTABLE}" "describe" "--tags" "--always" "--long" >> .release_info
53+
COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_str(v) \"${CBMC_RELEASE} (\" # v \")\"" >> .release_info
54+
COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_xstr(v) __CBMC_VERSION_str(v)" >> .release_info
55+
COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION __CBMC_VERSION_xstr(__CBMC_VERSION)" >> .release_info
56+
VERBATIM
57+
)
58+
add_custom_command(
59+
TARGET ${target}
60+
POST_BUILD
61+
COMMAND ${CMAKE_COMMAND} -E remove -f .release_info
62+
)
63+
else()
64+
add_custom_command(
65+
OUTPUT .release_info
66+
COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION \"${CBMC_RELEASE} (n/a)\"" >> .release_info
67+
VERBATIM
68+
)
69+
endif()
70+
71+
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
72+
"${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
73+
)
74+
set_source_files_properties(
75+
${${files_var}}
76+
PROPERTIES
77+
OBJECT_DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/.release_info
78+
COMPILE_FLAGS "-include .release_info")
79+
elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
80+
set_source_files_properties(
81+
${${files_var}}
82+
PROPERTIES
83+
COMPILE_FLAGS "/DCBMC_VERSION=\"${CBMC_RELEASE} (n/a)\"")
84+
endif()
85+
endmacro()
86+
4187
add_subdirectory(src)
4288
add_subdirectory(regression)
4389
add_subdirectory(unit)

‎jbmc/src/janalyzer/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,3 +24,6 @@ target_link_libraries(janalyzer-lib
2424
# Executable
2525
add_executable(janalyzer janalyzer_main.cpp)
2626
target_link_libraries(janalyzer janalyzer-lib)
27+
28+
set(cbmc_version_files janalyzer_parse_options.cpp)
29+
git_revision(janalyzer-lib cbmc_version_files)

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 3 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -50,8 +50,6 @@ Author: Daniel Kroening, [email protected]
5050
#include <util/options.h>
5151
#include <util/unicode.h>
5252

53-
#include <cbmc/version.h>
54-
5553
#include <goto-analyzer/static_show_domain.h>
5654
#include <goto-analyzer/static_simplifier.h>
5755
#include <goto-analyzer/static_verifier.h>
@@ -723,17 +721,11 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
723721
/// display command line help
724722
void janalyzer_parse_optionst::help()
725723
{
726-
std::cout << "\n"
727-
"* * JANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 ";
728-
729-
std::cout << "(" << (sizeof(void *) * 8) << "-bit version)";
730-
731-
std::cout << " * *\n";
732-
733724
// clang-format off
734-
std::cout <<
725+
std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
726+
<<
735727
/* NOLINTNEXTLINE(whitespace/line_length) */
736-
"* * JANALYZER " CBMC_VERSION " - Copyright (C) 2016-2018 * *\n"
728+
"* * Copyright (C) 2016-2018 * *\n"
737729
"* * Daniel Kroening, Diffblue * *\n"
738730
"* * [email protected] * *\n"
739731
"\n"

‎jbmc/src/janalyzer/module_dependencies.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
analyses
22
ansi-c # should go away
3-
cbmc # version.h
43
java_bytecode
54
jdiff
65
goto-analyzer

‎jbmc/src/jbmc/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,6 @@ target_link_libraries(jbmc-lib
2929
# Executable
3030
add_executable(jbmc jbmc_main.cpp)
3131
target_link_libraries(jbmc jbmc-lib)
32+
33+
set(cbmc_version_files jbmc_parse_options.cpp)
34+
git_revision(jbmc-lib cbmc_version_files)

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -60,8 +60,6 @@ Author: Daniel Kroening, [email protected]
6060
#include <java_bytecode/replace_java_nondet.h>
6161
#include <java_bytecode/simple_method_stubbing.h>
6262

63-
#include <cbmc/version.h>
64-
6563
jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
6664
parse_options_baset(JBMC_OPTIONS, argc, argv),
6765
messaget(ui_message_handler),
@@ -1069,15 +1067,10 @@ bool jbmc_parse_optionst::generate_function_body(
10691067
/// display command line help
10701068
void jbmc_parse_optionst::help()
10711069
{
1072-
std::cout << "\n"
1073-
"* * JBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";
1074-
1075-
std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
1076-
1077-
std::cout << " * *\n";
1078-
10791070
// clang-format off
1080-
std::cout <<
1071+
std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1072+
<<
1073+
"* * Copyright (C) 2001-2018 * *\n"
10811074
"* * Daniel Kroening, Edmund Clarke * *\n"
10821075
"* * Carnegie Mellon University, Computer Science Department * *\n"
10831076
"* * [email protected] * *\n"

‎jbmc/src/jbmc/module_dependencies.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
analyses
22
ansi-c # should go away
3-
cbmc # version.h and bmc.h
3+
cbmc # bmc.h
44
goto-instrument
55
goto-programs
66
goto-symex

‎jbmc/src/jdiff/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,3 +26,6 @@ target_link_libraries(jdiff-lib
2626
# Executable
2727
add_executable(jdiff jdiff_main.cpp)
2828
target_link_libraries(jdiff jdiff-lib)
29+
30+
set(cbmc_version_files jdiff_parse_options.cpp)
31+
git_revision(jdiff-lib cbmc_version_files)

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,6 @@ Author: Peter Schrammel
5555

5656
#include <langapi/mode.h>
5757

58-
#include <cbmc/version.h>
59-
6058
#include "java_syntactic_diff.h"
6159
#include <goto-diff/change_impact.h>
6260
#include <goto-diff/goto_diff.h>
@@ -429,10 +427,9 @@ bool jdiff_parse_optionst::process_goto_program(
429427
void jdiff_parse_optionst::help()
430428
{
431429
// clang-format off
432-
std::cout <<
433-
"\n"
434-
// NOLINTNEXTLINE(whitespace/line_length)
435-
"* * JDIFF " CBMC_VERSION " - Copyright (C) 2016-2018 * *\n"
430+
std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
431+
<<
432+
"* * Copyright (C) 2016-2018 * *\n"
436433
"* * Daniel Kroening, Peter Schrammel * *\n"
437434
"* * [email protected] * *\n"
438435
"\n"

‎jbmc/src/jdiff/module_dependencies.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
analyses
2-
cbmc # version.h
32
java_bytecode
43
jdiff
54
goto-diff

‎src/cbmc/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,3 +31,6 @@ add_if_library(cbmc-lib jsil)
3131
# Executable
3232
add_executable(cbmc cbmc_main.cpp)
3333
target_link_libraries(cbmc cbmc-lib)
34+
35+
set(cbmc_version_files cbmc_parse_options.cpp cbmc_solvers.cpp)
36+
git_revision(cbmc-lib cbmc_version_files)

‎src/cbmc/Makefile

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

5757
LIBS =
5858

59+
CBMC_VERSION_FILES = cbmc_solvers$(OBJEXT)
60+
5961
include ../config.inc
6062
include ../common
6163

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,6 @@ Author: Daniel Kroening, [email protected]
6262

6363
#include <langapi/mode.h>
6464

65-
#include "version.h"
6665
#include "xml_interface.h"
6766

6867
cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
@@ -867,15 +866,9 @@ bool cbmc_parse_optionst::process_goto_program(
867866
void cbmc_parse_optionst::help()
868867
{
869868
// clang-format off
870-
std::cout <<
871-
"\n"
872-
"* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";
873-
874-
std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
875-
876-
std::cout << " * *\n";
877-
878-
std::cout <<
869+
std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
870+
<<
871+
"* * Copyright (C) 2001-2018 * *\n"
879872
"* * Daniel Kroening, Edmund Clarke * *\n"
880873
"* * Carnegie Mellon University, Computer Science Department * *\n"
881874
"* * [email protected] * *\n"

‎src/cbmc/cbmc_solvers.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ Author: Daniel Kroening, [email protected]
2828
#include "bv_cbmc.h"
2929
#include "cbmc_dimacs.h"
3030
#include "counterexample_beautification.h"
31-
#include "version.h"
3231

3332
/// Uses the options to pick an SMT 2.0 solver
3433
/// \return An smt2_dect::solvert giving the solver to use.

‎src/cbmc/version.h

Lines changed: 0 additions & 14 deletions
This file was deleted.

‎src/clobber/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,3 +30,5 @@ add_if_library(clobber-lib bv_refinement)
3030
add_executable(clobber clobber_main.cpp)
3131
target_link_libraries(clobber clobber-lib)
3232

33+
set(cbmc_version_files clobber_parse_options.cpp)
34+
git_revision(clobber-lib cbmc_version_files)

‎src/clobber/clobber_parse_options.cpp

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,6 @@ Author: Daniel Kroening, [email protected]
3434

3535
#include <langapi/mode.h>
3636

37-
#include <cbmc/version.h>
3837

3938
clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
4039
parse_options_baset(CLOBBER_OPTIONS, argc, argv),
@@ -349,15 +348,10 @@ void clobber_parse_optionst::report_failure()
349348
/// display command line help
350349
void clobber_parse_optionst::help()
351350
{
352-
std::cout <<
353-
"\n"
354-
"* * CLOBBER " CBMC_VERSION " - Copyright (C) 2014 ";
355-
356-
std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
357-
358-
std::cout << " * *\n";
359-
360-
std::cout <<
351+
// clang-format off
352+
std::cout << '\n' << banner_string("CLOBBER", CBMC_VERSION) << '\n'
353+
<<
354+
"* * Copyright (C) 2014 * *\n"
361355
"* * Daniel Kroening * *\n"
362356
"* * University of Oxford * *\n"
363357
"* * [email protected] * *\n"
@@ -415,4 +409,5 @@ void clobber_parse_optionst::help()
415409
" --version show version and exit\n"
416410
" --xml-ui use XML-formatted output\n"
417411
"\n";
412+
// clang-format on
418413
}

‎src/common

Lines changed: 29 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -227,12 +227,40 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
227227
%.obj:%.c
228228
$(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@
229229

230+
# get version from git
231+
GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
232+
GIT_INFO_FILE = .release_info
233+
234+
CBMC_VERSION_FILES += $(filter %_parse_options$(OBJEXT), $(OBJ))
235+
236+
ifeq ($(BUILD_ENV_),MSVC)
237+
$(CBMC_VERSION_FILES): CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
238+
else
239+
$(CBMC_VERSION_FILES): CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
240+
endif
241+
242+
# Use make >= 4.0's `file` function, if available - it should be faster than
243+
# `shell cat`
244+
ifeq ($(firstword $(subst ., , $(MAKE_VERSION))), 3)
245+
KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
246+
else
247+
KNOWN_RELEASE_INFO = $(file < $(GIT_INFO_FILE))
248+
endif
249+
ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO))
250+
$(CBMC_VERSION_FILES): $(GIT_INFO_FILE)
251+
252+
$(GIT_INFO_FILE):
253+
echo $(GIT_INFO) > $@
254+
255+
.PHONY: $(GIT_INFO_FILE)
256+
endif
257+
230258
clean:
231259
$(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
232260
$(patsubst %.cpp, %$(DEPEXT), $(filter %.cpp, $(SRC))) \
233261
$(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
234262
$(patsubst %.cc, %$(DEPEXT), $(filter %.cc, $(SRC))) \
235-
$(CLEANFILES)
263+
$(CLEANFILES) $(GIT_INFO_FILE)
236264

237265
.PHONY: first_target clean all
238266
.PHONY: sources generated_files
@@ -252,4 +280,3 @@ D_FILES1 = $(SRC:.c=$(DEPEXT))
252280
D_FILES = $(D_FILES1:.cpp=$(DEPEXT))
253281

254282
-include $(D_FILES)
255-

‎src/config.inc

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,3 +70,6 @@ endif
7070
# Signing identity for MacOS Gatekeeper
7171

7272
OSX_IDENTITY="Developer ID Application: Daniel Kroening"
73+
74+
# Detailed version information
75+
CBMC_VERSION = 5.8

‎src/goto-analyzer/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,3 +26,6 @@ add_if_library(goto-analyzer-lib jsil)
2626
# Executable
2727
add_executable(goto-analyzer goto_analyzer_main.cpp)
2828
target_link_libraries(goto-analyzer goto-analyzer-lib)
29+
30+
set(cbmc_version_files goto_analyzer_parse_options.cpp)
31+
git_revision(goto-analyzer-lib cbmc_version_files)

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,6 @@ Author: Daniel Kroening, [email protected]
5454
#include <util/unicode.h>
5555
#include <util/exit_codes.h>
5656

57-
#include <cbmc/version.h>
5857
#include <goto-programs/adjust_float_expressions.h>
5958

6059
#include "taint_analysis.h"
@@ -790,15 +789,10 @@ bool goto_analyzer_parse_optionst::process_goto_program(
790789
/// display command line help
791790
void goto_analyzer_parse_optionst::help()
792791
{
793-
std::cout << "\n"
794-
"* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 ";
795-
796-
std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
797-
798-
std::cout << " * *\n";
799-
800792
// clang-format off
801-
std::cout <<
793+
std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
794+
<<
795+
"* * Copyright (C) 2017-2018 * *\n"
802796
"* * Daniel Kroening, DiffBlue * *\n"
803797
"* * [email protected] * *\n"
804798
"\n"

‎src/goto-analyzer/module_dependencies.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
ansi-c
22
analyses
3-
cbmc # version.h
43
cpp
54
goto-analyzer
65
goto-programs

‎src/goto-cc/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,3 +34,6 @@ else()
3434
COMMAND "${CMAKE_COMMAND}" -E create_symlink
3535
goto-cc $<TARGET_FILE_DIR:goto-cc>/goto-gcc)
3636
endif()
37+
38+
set(cbmc_version_files as_mode.cpp compile.cpp gcc_mode.cpp goto_cc_mode.cpp)
39+
git_revision(goto-cc-lib cbmc_version_files)

0 commit comments

Comments
 (0)