From 840d47fa47997d9d74e9fdbfc4e0840e1c2bbf40 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 20 May 2025 18:39:51 +0100 Subject: [PATCH] EBMC: include git commit in version To distinguish in-between release builds from releases, include the git commit in the version output, using the same style as CBMC. --- src/Makefile | 2 +- src/config.inc | 1 + src/ebmc/Makefile | 18 +++++++++++++++++- src/ebmc/ebmc_parse_options.cpp | 14 +++++++------- src/ebmc/ebmc_parse_options.h | 2 +- src/ebmc/ebmc_solver_factory.cpp | 6 +++--- src/ebmc/ebmc_version.h | 2 +- src/vlindex/Makefile | 1 + src/vlindex/vlindex_parse_options.cpp | 5 ++--- src/vlindex/vlindex_parse_options.h | 2 +- 10 files changed, 35 insertions(+), 18 deletions(-) diff --git a/src/Makefile b/src/Makefile index 64c375856..a1fc826b3 100644 --- a/src/Makefile +++ b/src/Makefile @@ -24,7 +24,7 @@ endif hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \ vhdl.dir smvlang.dir cprover.dir temporal-logic.dir -vlindex.dir: cprover.dir verilog.dir +vlindex.dir: ebmc.dir cprover.dir verilog.dir # building cbmc proper .PHONY: cprover.dir diff --git a/src/config.inc b/src/config.inc index e69de29bb..c54ee8987 100644 --- a/src/config.inc +++ b/src/config.inc @@ -0,0 +1 @@ +EBMC_VERSION = 5.7 diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index da61dc177..0c592f5a9 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -16,6 +16,7 @@ SRC = \ ebmc_parse_options.cpp \ ebmc_properties.cpp \ ebmc_solver_factory.cpp \ + ebmc_version.cpp \ instrument_past.cpp \ k_induction.cpp \ liveness_to_safety.cpp \ @@ -69,12 +70,27 @@ endif include ../config.inc include ../common +# get version from git +GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") +RELEASE_INFO = const char *EBMC_VERSION="$(EBMC_VERSION) ($(GIT_INFO))"; +GIT_INFO_FILE = ebmc_version.cpp + +$(GIT_INFO_FILE): + echo '$(RELEASE_INFO)' > $@ + +# mark the actually generated file as a phony target to enforce a rebuild - but +# only if the version information has changed! +KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null) +ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO)) +.PHONY: $(GIT_INFO_FILE) +endif + ifneq ($(wildcard ../vhdl/Makefile),) OBJ += ../vhdl/vhdl$(LIBEXT) CXXFLAGS += -DHAVE_VHDL endif -CLEANFILES = ebmc$(EXEEXT) +CLEANFILES = $(GIT_INFO_FILE) ebmc$(EXEEXT) all: ebmc$(EXEEXT) diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 573c43932..f810078a2 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -344,13 +344,13 @@ Function: ebmc_parse_optionst::help void ebmc_parse_optionst::help() { - std::cout << - "\n" - "* * EBMC - Copyright (C) 2001-2017 Daniel Kroening * *\n" - "* * Version " EBMC_VERSION " * *\n" - "* * University of Oxford, Computer Science Department * *\n" - "* * kroening@kroening.com * *\n" - "\n"; + std::cout + << '\n' + << banner_string("EBMC", EBMC_VERSION) << '\n' + << "* * EBMC - Copyright (C) 2001-2017 Daniel Kroening * *\n" + "* * University of Oxford, Computer Science Department * *\n" + "* * kroening@kroening.com * *\n" + "\n"; std::cout << help_formatter( // clang-format off diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index aa3b69688..b9b678e63 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -55,7 +55,7 @@ class ebmc_parse_optionst:public parse_options_baset argc, argv, std::string("EBMC ") + EBMC_VERSION), - ui_message_handler(cmdline, "EBMC " EBMC_VERSION) + ui_message_handler(cmdline, std::string("EBMC ") + EBMC_VERSION) { } diff --git a/src/ebmc/ebmc_solver_factory.cpp b/src/ebmc/ebmc_solver_factory.cpp index acdba0440..39f04f86d 100644 --- a/src/ebmc/ebmc_solver_factory.cpp +++ b/src/ebmc/ebmc_solver_factory.cpp @@ -92,7 +92,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline) auto dec = std::make_unique( ns, "ebmc", - "Generated by EBMC " EBMC_VERSION, + std::string("Generated by EBMC ") + EBMC_VERSION, "QF_AUFBV", smt2_solver.value(), *outfile_ptr); @@ -118,7 +118,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline) return ebmc_solvert{std::make_unique( ns, "ebmc", - "Generated by EBMC " EBMC_VERSION, + std::string("Generated by EBMC ") + EBMC_VERSION, "QF_AUFBV", smt2_solver.value(), std::cout)}; @@ -128,7 +128,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline) return ebmc_solvert{std::make_unique( ns, "ebmc", - "Generated by EBMC " EBMC_VERSION, + std::string("Generated by EBMC ") + EBMC_VERSION, "QF_AUFBV", smt2_solver.value(), message_handler)}; diff --git a/src/ebmc/ebmc_version.h b/src/ebmc/ebmc_version.h index 0361d5e9f..b20d52c00 100644 --- a/src/ebmc/ebmc_version.h +++ b/src/ebmc/ebmc_version.h @@ -1 +1 @@ -#define EBMC_VERSION "5.7" +extern const char *EBMC_VERSION; diff --git a/src/vlindex/Makefile b/src/vlindex/Makefile index 50b5d52a0..7254b242e 100644 --- a/src/vlindex/Makefile +++ b/src/vlindex/Makefile @@ -8,6 +8,7 @@ SRC = \ OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \ $(CPROVER_DIR)/langapi/langapi$(LIBEXT) \ $(CPROVER_DIR)/big-int/big-int$(LIBEXT) \ + ../ebmc/ebmc_version$(OBJEXT) \ ../verilog/verilog$(LIBEXT) include ../config.inc diff --git a/src/vlindex/vlindex_parse_options.cpp b/src/vlindex/vlindex_parse_options.cpp index e49f210e1..6bc8cd885 100644 --- a/src/vlindex/vlindex_parse_options.cpp +++ b/src/vlindex/vlindex_parse_options.cpp @@ -79,9 +79,8 @@ void vlindex_parse_optionst::help() { std::cout << "\n" - "* * VLINDEX - Copyright (C) 2024 * *\n" - "* * Version " EBMC_VERSION - " * *\n" + << banner_string("VLINDEX", EBMC_VERSION) << '\n' + << "* * Copyright (C) 2024 * *\n" "* * dkr@amazon.com * *\n" "\n"; diff --git a/src/vlindex/vlindex_parse_options.h b/src/vlindex/vlindex_parse_options.h index 0b4c2ed11..4f67bf3fd 100644 --- a/src/vlindex/vlindex_parse_options.h +++ b/src/vlindex/vlindex_parse_options.h @@ -35,7 +35,7 @@ class vlindex_parse_optionst : public parse_options_baset argc, argv, std::string("EBMC ") + EBMC_VERSION), - ui_message_handler(cmdline, "EBMC " EBMC_VERSION) + ui_message_handler(cmdline, std::string("EBMC ") + EBMC_VERSION) { }