Skip to content

Commit f57e2f6

Browse files
author
Daniel Kroening
committed
move build commands for cbmc/version.h from common to cbmc/Makefile
1 parent 6fd77f4 commit f57e2f6

File tree

10 files changed

+53
-58
lines changed

10 files changed

+53
-58
lines changed

‎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/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/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/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/goto_diff_parse_options.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,10 @@ Author: Peter Schrammel
1717
#include <memory>
1818

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

2425
#include <langapi/language.h>
2526

@@ -59,7 +60,6 @@ Author: Peter Schrammel
5960
#include "syntactic_diff.h"
6061
#include "unified_diff.h"
6162
#include "change_impact.h"
62-
#include "version.h"
6363

6464
goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv):
6565
parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),

‎src/goto-instrument/goto_instrument_parse_options.cpp

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

1818
#include <util/config.h>
19+
#include <util/exit_codes.h>
20+
#include <util/json.h>
1921
#include <util/string2int.h>
2022
#include <util/unicode.h>
21-
#include <util/json.h>
22-
#include <util/exit_codes.h>
23+
#include <util/version.h>
2324

2425
#include <goto-programs/class_hierarchy.h>
2526
#include <goto-programs/goto_convert_functions.h>
@@ -99,7 +100,6 @@ Author: Daniel Kroening, [email protected]
99100
#include "undefined_functions.h"
100101
#include "remove_function.h"
101102
#include "splice_call.h"
102-
#include "version.h"
103103

104104
/// invoke main modules
105105
int goto_instrument_parse_optionst::doit()

‎src/util/Makefile

+19-2
Original file line numberDiff line numberDiff line change
@@ -103,9 +103,26 @@ INCLUDES= -I ..
103103
include ../config.inc
104104
include ../common
105105

106-
CLEANFILES = util$(LIBEXT)
106+
# get version from git
107+
GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
108+
RELEASE_INFO = \#define CBMC_VERSION "$(CBMC_VERSION) ($(GIT_INFO))"
109+
GIT_INFO_FILE = version.h
107110

108-
all: util$(LIBEXT)
111+
$(GIT_INFO_FILE):
112+
echo '$(RELEASE_INFO)' > $@
113+
114+
generated_files: $(GIT_INFO_FILE)
115+
116+
# mark the actually generated file as a phony target to enforce a rebuild - but
117+
# only if the version information has changed!
118+
KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
119+
ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO))
120+
.PHONY: $(GIT_INFO_FILE)
121+
endif
122+
123+
CLEANFILES = $(GIT_INFO_FILE) util$(LIBEXT)
124+
125+
all: util$(LIBEXT) $(GIT_INFO_FILE)
109126

110127
util$(LIBEXT): $(OBJ)
111128
$(LINKLIB)

0 commit comments

Comments
 (0)