Skip to content

Commit 6e554d9

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#2500 from diffblue/git-version-speedup
move version.h to util/
2 parents f90ed9e + b96c7ba commit 6e554d9

30 files changed

+105
-140
lines changed

‎CMakeLists.txt

-42
Original file line numberDiff line numberDiff line change
@@ -39,48 +39,6 @@ if(${enable_cbmc_tests})
3939
enable_testing()
4040
endif()
4141

42-
# based on https://cmake.org/pipermail/cmake/2010-July/038015.html
43-
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()
69-
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
79-
)
80-
add_dependencies(${target} ${target}-version.h)
81-
endmacro()
82-
include_directories(${CMAKE_CURRENT_BINARY_DIR})
83-
8442
add_subdirectory(src)
8543
add_subdirectory(regression)
8644
add_subdirectory(unit)

‎jbmc/src/janalyzer/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -24,5 +24,3 @@ target_link_libraries(janalyzer-lib
2424
# Executable
2525
add_executable(janalyzer janalyzer_main.cpp)
2626
target_link_libraries(janalyzer janalyzer-lib)
27-
28-
git_revision(janalyzer-lib)

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -49,15 +49,14 @@ Author: Daniel Kroening, [email protected]
4949
#include <util/exit_codes.h>
5050
#include <util/options.h>
5151
#include <util/unicode.h>
52+
#include <util/version.h>
5253

5354
#include <goto-analyzer/static_show_domain.h>
5455
#include <goto-analyzer/static_simplifier.h>
5556
#include <goto-analyzer/static_verifier.h>
5657
#include <goto-analyzer/taint_analysis.h>
5758
#include <goto-analyzer/unreachable_instructions.h>
5859

59-
#include "version.h"
60-
6160
janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
6261
: parse_options_baset(JANALYZER_OPTIONS, argc, argv),
6362
messaget(ui_message_handler),

‎jbmc/src/jbmc/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -29,5 +29,3 @@ target_link_libraries(jbmc-lib
2929
# Executable
3030
add_executable(jbmc jbmc_main.cpp)
3131
target_link_libraries(jbmc jbmc-lib)
32-
33-
git_revision(jbmc-lib)

‎jbmc/src/jbmc/jbmc_parse_options.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,11 @@ Author: Daniel Kroening, [email protected]
1616
#include <iostream>
1717
#include <memory>
1818

19-
#include <util/exit_codes.h>
2019
#include <util/config.h>
21-
#include <util/unicode.h>
20+
#include <util/exit_codes.h>
2221
#include <util/invariant.h>
22+
#include <util/unicode.h>
23+
#include <util/version.h>
2324

2425
#include <langapi/language.h>
2526

@@ -60,8 +61,6 @@ Author: Daniel Kroening, [email protected]
6061
#include <java_bytecode/replace_java_nondet.h>
6162
#include <java_bytecode/simple_method_stubbing.h>
6263

63-
#include "version.h"
64-
6564
jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
6665
parse_options_baset(JBMC_OPTIONS, argc, argv),
6766
messaget(ui_message_handler),

‎jbmc/src/jdiff/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -26,5 +26,3 @@ target_link_libraries(jdiff-lib
2626
# Executable
2727
add_executable(jdiff jdiff_main.cpp)
2828
target_link_libraries(jdiff jdiff-lib)
29-
30-
git_revision(jdiff-lib)

‎jbmc/src/jdiff/jdiff_parse_options.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Peter Schrammel
2020
#include <util/exit_codes.h>
2121
#include <util/make_unique.h>
2222
#include <util/options.h>
23+
#include <util/version.h>
2324

2425
#include <langapi/language.h>
2526

@@ -60,8 +61,6 @@ Author: Peter Schrammel
6061
#include <goto-diff/goto_diff.h>
6162
#include <goto-diff/unified_diff.h>
6263

63-
#include "version.h"
64-
6564
jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
6665
: parse_options_baset(JDIFF_OPTIONS, argc, argv),
6766
jdiff_languagest(cmdline, ui_message_handler),

‎src/cbmc/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -31,5 +31,3 @@ add_if_library(cbmc-lib jsil)
3131
# Executable
3232
add_executable(cbmc cbmc_main.cpp)
3333
target_link_libraries(cbmc cbmc-lib)
34-
35-
git_revision(cbmc-lib)

‎src/cbmc/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -63,8 +63,6 @@ CLEANFILES = cbmc$(EXEEXT)
6363

6464
all: cbmc$(EXEEXT)
6565

66-
cbmc_solvers$(OBJEXT): $(GIT_INFO_FILE)
67-
6866
ifneq ($(wildcard ../bv_refinement/Makefile),)
6967
OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
7068
CP_CXXFLAGS += -DHAVE_BV_REFINEMENT

‎src/cbmc/cbmc_parse_options.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,10 @@ Author: Daniel Kroening, [email protected]
1717
#include <memory>
1818

1919
#include <util/config.h>
20-
#include <util/unicode.h>
21-
#include <util/invariant.h>
2220
#include <util/exit_codes.h>
21+
#include <util/invariant.h>
22+
#include <util/unicode.h>
23+
#include <util/version.h>
2324

2425
#include <langapi/language.h>
2526

@@ -64,8 +65,6 @@ Author: Daniel Kroening, [email protected]
6465

6566
#include "xml_interface.h"
6667

67-
#include "version.h"
68-
6968
cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
7069
parse_options_baset(CBMC_OPTIONS, argc, argv),
7170
xml_interfacet(cmdline),

‎src/cbmc/cbmc_solvers.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,9 @@ Author: Daniel Kroening, [email protected]
1515
#include <iostream>
1616
#include <memory>
1717

18-
#include <util/unicode.h>
1918
#include <util/make_unique.h>
19+
#include <util/unicode.h>
20+
#include <util/version.h>
2021

2122
#include <solvers/sat/satcheck.h>
2223
#include <solvers/refinement/bv_refinement.h>
@@ -28,7 +29,6 @@ Author: Daniel Kroening, [email protected]
2829
#include "bv_cbmc.h"
2930
#include "cbmc_dimacs.h"
3031
#include "counterexample_beautification.h"
31-
#include "version.h"
3232

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

‎src/clobber/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -29,5 +29,3 @@ add_if_library(clobber-lib bv_refinement)
2929
# Executable
3030
add_executable(clobber clobber_main.cpp)
3131
target_link_libraries(clobber clobber-lib)
32-
33-
git_revision(clobber-lib)

‎src/clobber/clobber_parse_options.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,9 @@ Author: Daniel Kroening, [email protected]
1616
#include <cstdlib>
1717

1818
#include <util/config.h>
19-
#include <util/options.h>
2019
#include <util/memory_info.h>
20+
#include <util/options.h>
21+
#include <util/version.h>
2122

2223
#include <ansi-c/ansi_c_language.h>
2324
#include <cpp/cpp_language.h>
@@ -34,8 +35,6 @@ Author: Daniel Kroening, [email protected]
3435

3536
#include <langapi/mode.h>
3637

37-
#include "version.h"
38-
3938
clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
4039
parse_options_baset(CLOBBER_OPTIONS, argc, argv),
4140
language_uit(cmdline, ui_message_handler),

‎src/common

+1-18
Original file line numberDiff line numberDiff line change
@@ -227,29 +227,12 @@ 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-
RELEASE_INFO = \#define CBMC_VERSION "$(CBMC_VERSION) ($(GIT_INFO))"
233-
GIT_INFO_FILE = version.h
234-
235-
$(GIT_INFO_FILE):
236-
echo '$(RELEASE_INFO)' > $@
237-
238-
$(filter %_parse_options$(OBJEXT), $(OBJ)): $(GIT_INFO_FILE)
239-
240-
# mark the actually generated file as a phony target to enforce a rebuild - but
241-
# only of the version information has changed!
242-
KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
243-
ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO))
244-
.PHONY: $(GIT_INFO_FILE)
245-
endif
246-
247230
clean:
248231
$(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
249232
$(patsubst %.cpp, %$(DEPEXT), $(filter %.cpp, $(SRC))) \
250233
$(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
251234
$(patsubst %.cc, %$(DEPEXT), $(filter %.cc, $(SRC))) \
252-
$(CLEANFILES) $(GIT_INFO_FILE)
235+
$(CLEANFILES)
253236

254237
.PHONY: first_target clean all
255238
.PHONY: sources generated_files

‎src/goto-analyzer/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -26,5 +26,3 @@ 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-
git_revision(goto-analyzer-lib)

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

+12-13
Original file line numberDiff line numberDiff line change
@@ -24,20 +24,21 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include <jsil/jsil_language.h>
2626

27+
#include <goto-programs/adjust_float_expressions.h>
28+
#include <goto-programs/goto_convert_functions.h>
29+
#include <goto-programs/goto_inline.h>
2730
#include <goto-programs/initialize_goto_model.h>
28-
#include <goto-programs/set_properties.h>
31+
#include <goto-programs/link_to_library.h>
32+
#include <goto-programs/read_goto_binary.h>
33+
#include <goto-programs/remove_asm.h>
34+
#include <goto-programs/remove_complex.h>
2935
#include <goto-programs/remove_function_pointers.h>
30-
#include <goto-programs/remove_virtual_functions.h>
3136
#include <goto-programs/remove_returns.h>
3237
#include <goto-programs/remove_vector.h>
33-
#include <goto-programs/remove_complex.h>
34-
#include <goto-programs/remove_asm.h>
35-
#include <goto-programs/goto_convert_functions.h>
38+
#include <goto-programs/remove_virtual_functions.h>
39+
#include <goto-programs/set_properties.h>
3640
#include <goto-programs/show_properties.h>
3741
#include <goto-programs/show_symbol_table.h>
38-
#include <goto-programs/read_goto_binary.h>
39-
#include <goto-programs/goto_inline.h>
40-
#include <goto-programs/link_to_library.h>
4142

4243
#include <analyses/is_threaded.h>
4344
#include <analyses/goto_check.h>
@@ -49,19 +50,17 @@ Author: Daniel Kroening, [email protected]
4950
#include <langapi/mode.h>
5051
#include <langapi/language.h>
5152

52-
#include <util/options.h>
5353
#include <util/config.h>
54-
#include <util/unicode.h>
5554
#include <util/exit_codes.h>
56-
57-
#include <goto-programs/adjust_float_expressions.h>
55+
#include <util/options.h>
56+
#include <util/unicode.h>
57+
#include <util/version.h>
5858

5959
#include "taint_analysis.h"
6060
#include "unreachable_instructions.h"
6161
#include "static_show_domain.h"
6262
#include "static_simplifier.h"
6363
#include "static_verifier.h"
64-
#include "version.h"
6564

6665
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
6766
int argc,

‎src/goto-cc/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -34,5 +34,3 @@ else()
3434
COMMAND "${CMAKE_COMMAND}" -E create_symlink
3535
goto-cc $<TARGET_FILE_DIR:goto-cc>/goto-gcc)
3636
endif()
37-
38-
git_revision(goto-cc-lib)

‎src/goto-cc/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,6 @@ all: goto-cl$(EXEEXT)
4646
endif
4747
all: goto-cc$(EXEEXT)
4848

49-
as_mode$(OBJEXT) compile$(OBJEXT) gcc_mode$(OBJEXT) goto_cc_mode$(OBJEXT): $(GIT_INFO_FILE)
50-
5149
ifneq ($(wildcard ../jsil/Makefile),)
5250
OBJ += ../jsil/jsil$(LIBEXT)
5351
CP_CXXFLAGS += -DHAVE_JSIL

‎src/goto-cc/as_mode.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -23,14 +23,14 @@ Author: Michael Tautschnig
2323
#include <iostream>
2424
#include <cstring>
2525

26-
#include <util/run.h>
27-
#include <util/tempdir.h>
2826
#include <util/config.h>
29-
#include <util/get_base_name.h>
3027
#include <util/cout_message.h>
28+
#include <util/get_base_name.h>
29+
#include <util/run.h>
30+
#include <util/tempdir.h>
31+
#include <util/version.h>
3132

3233
#include "compile.h"
33-
#include "version.h"
3434

3535
static std::string assembler_name(
3636
const cmdlinet &cmdline,

‎src/goto-cc/compile.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Date: June 2006
2424
#include <util/suffix.h>
2525
#include <util/tempdir.h>
2626
#include <util/unicode.h>
27+
#include <util/version.h>
2728

2829
#include <ansi-c/ansi_c_language.h>
2930
#include <ansi-c/ansi_c_entry_point.h>
@@ -63,8 +64,6 @@ Date: June 2006
6364
#define pclose _pclose
6465
#endif
6566

66-
#include "version.h"
67-
6867
/// reads and source and object files, compiles and links them into goto program
6968
/// objects.
7069
/// \return true on error, false otherwise

‎src/goto-cc/gcc_mode.cpp

+9-9
Original file line numberDiff line numberDiff line change
@@ -31,24 +31,24 @@ Author: CM Wintersteiger, 2006
3131

3232
#include <json/json_parser.h>
3333

34-
#include <util/expr.h>
35-
#include <util/c_types.h>
3634
#include <util/arith_tools.h>
37-
#include <util/invariant.h>
38-
#include <util/tempdir.h>
39-
#include <util/tempfile.h>
35+
#include <util/c_types.h>
4036
#include <util/config.h>
41-
#include <util/prefix.h>
42-
#include <util/suffix.h>
37+
#include <util/expr.h>
4338
#include <util/get_base_name.h>
44-
#include <util/run.h>
39+
#include <util/invariant.h>
40+
#include <util/prefix.h>
4541
#include <util/replace_symbol.h>
42+
#include <util/run.h>
43+
#include <util/suffix.h>
44+
#include <util/tempdir.h>
45+
#include <util/tempfile.h>
46+
#include <util/version.h>
4647

4748
#include <goto-programs/read_goto_binary.h>
4849

4950
#include "hybrid_binary.h"
5051
#include "linker_script_merge.h"
51-
#include "version.h"
5252

5353
static std::string compiler_name(
5454
const cmdlinet &cmdline,

‎src/goto-cc/goto_cc_mode.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,7 @@ Author: CM Wintersteiger, 2006
2323
#endif
2424

2525
#include <util/parse_options.h>
26-
27-
#include "version.h"
26+
#include <util/version.h>
2827

2928
/// constructor
3029
goto_cc_modet::goto_cc_modet(

‎src/goto-diff/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -28,5 +28,3 @@ add_if_library(goto-diff-lib jsil)
2828
# Executable
2929
add_executable(goto-diff goto_diff_main.cpp)
3030
target_link_libraries(goto-diff goto-diff-lib)
31-
32-
git_revision(goto-diff-lib)

0 commit comments

Comments
 (0)