From ad5c3755cad0edef136193d4ac4674897ea09146 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 30 Jul 2018 22:13:27 +0100 Subject: [PATCH] use a string instead of macro for version number --- .gitignore | 2 +- .../src/janalyzer/janalyzer_parse_options.cpp | 4 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 25 ++++++----- jbmc/src/jdiff/jdiff_parse_options.cpp | 8 ++-- src/cbmc/cbmc_parse_options.cpp | 29 ++++++------- src/cbmc/cbmc_solvers.cpp | 43 +++++++++---------- src/clobber/clobber_parse_options.cpp | 8 ++-- .../goto_analyzer_parse_options.cpp | 13 +++--- src/goto-cc/as_mode.cpp | 15 ++++--- src/goto-cc/compile.cpp | 3 +- src/goto-cc/gcc_mode.cpp | 13 +++--- src/goto-diff/goto_diff_parse_options.cpp | 25 ++++++----- src/util/CMakeLists.txt | 26 +++++------ src/util/Makefile | 5 ++- src/util/version.h | 1 + 15 files changed, 110 insertions(+), 110 deletions(-) create mode 100644 src/util/version.h diff --git a/.gitignore b/.gitignore index e562affcc7..c10ff2decd 100644 --- a/.gitignore +++ b/.gitignore @@ -28,7 +28,7 @@ Release/* *.obj *.a *.lib -version.h +util/version.cpp src/ansi-c/arm_builtin_headers.inc src/ansi-c/clang_builtin_headers.inc src/ansi-c/cprover_builtin_headers.inc diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 4390cf405b..fb2444ce95 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -60,7 +60,7 @@ Author: Daniel Kroening, kroening@kroening.com janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv) : parse_options_baset(JANALYZER_OPTIONS, argc, argv), messaget(ui_message_handler), - ui_message_handler(cmdline, "JANALYZER " CBMC_VERSION) + ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION) { } @@ -342,7 +342,7 @@ int janalyzer_parse_optionst::doit() // // Print a banner // - status() << "JANALYZER version " CBMC_VERSION " " << sizeof(void *) * 8 + status() << "JANALYZER version " << CBMC_VERSION << " " << sizeof(void *) * 8 << "-bit " << config.this_architecture() << " " << config.this_operating_system() << eom; diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 100d28b660..787d47579f 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -61,22 +61,22 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv): - parse_options_baset(JBMC_OPTIONS, argc, argv), - messaget(ui_message_handler), - ui_message_handler(cmdline, "JBMC " CBMC_VERSION), - path_strategy_chooser() +jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv) + : parse_options_baset(JBMC_OPTIONS, argc, argv), + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION), + path_strategy_chooser() { } ::jbmc_parse_optionst::jbmc_parse_optionst( int argc, const char **argv, - const std::string &extra_options): - parse_options_baset(JBMC_OPTIONS+extra_options, argc, argv), - messaget(ui_message_handler), - ui_message_handler(cmdline, "JBMC " CBMC_VERSION), - path_strategy_chooser() + const std::string &extra_options) + : parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv), + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION), + path_strategy_chooser() { } @@ -418,9 +418,8 @@ int jbmc_parse_optionst::doit() // // Print a banner // - status() << "JBMC version " CBMC_VERSION " " - << sizeof(void *)*8 << "-bit " - << config.this_architecture() << " " + status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8 + << "-bit " << config.this_architecture() << " " << config.this_operating_system() << eom; register_language(new_ansi_c_language); diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index f22a5d722c..1fdeb65985 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -64,7 +64,7 @@ Author: Peter Schrammel jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv) : parse_options_baset(JDIFF_OPTIONS, argc, argv), jdiff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, "JDIFF " CBMC_VERSION), + ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler) { } @@ -75,7 +75,7 @@ jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv) const std::string &extra_options) : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv), jdiff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, "JDIFF " CBMC_VERSION), + ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler) { } @@ -206,8 +206,8 @@ int jdiff_parse_optionst::doit() // // Print a banner // - status() << "JDIFF version " CBMC_VERSION " " << sizeof(void *) * 8 << "-bit " - << config.this_architecture() << " " + status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8 + << "-bit " << config.this_architecture() << " " << config.this_operating_system() << eom; if(cmdline.args.size() != 2) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 0fd7408aee..f5074b6b54 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -65,24 +65,24 @@ Author: Daniel Kroening, kroening@kroening.com #include "xml_interface.h" -cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv): - parse_options_baset(CBMC_OPTIONS, argc, argv), - xml_interfacet(cmdline), - messaget(ui_message_handler), - ui_message_handler(cmdline, "CBMC " CBMC_VERSION), - path_strategy_chooser() +cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv) + : parse_options_baset(CBMC_OPTIONS, argc, argv), + xml_interfacet(cmdline), + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION), + path_strategy_chooser() { } ::cbmc_parse_optionst::cbmc_parse_optionst( int argc, const char **argv, - const std::string &extra_options): - parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv), - xml_interfacet(cmdline), - messaget(ui_message_handler), - ui_message_handler(cmdline, "CBMC " CBMC_VERSION), - path_strategy_chooser() + const std::string &extra_options) + : parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv), + xml_interfacet(cmdline), + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION), + path_strategy_chooser() { } @@ -436,9 +436,8 @@ int cbmc_parse_optionst::doit() // // Print a banner // - status() << "CBMC version " CBMC_VERSION " " - << sizeof(void *)*8 << "-bit " - << config.this_architecture() << " " + status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8 + << "-bit " << config.this_architecture() << " " << config.this_operating_system() << eom; // diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 11a1ee7ef0..31e5793ce3 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -173,13 +173,12 @@ std::unique_ptr cbmc_solverst::get_smt2( throw 0; } - auto smt2_dec= - util_make_unique( - ns, - "cbmc", - "Generated by CBMC " CBMC_VERSION, - "QF_AUFBV", - solver); + auto smt2_dec = util_make_unique( + ns, + "cbmc", + std::string("Generated by CBMC ") + CBMC_VERSION, + "QF_AUFBV", + solver); if(options.get_bool_option("fpa")) smt2_dec->use_FPA_theory=true; @@ -188,14 +187,13 @@ std::unique_ptr cbmc_solverst::get_smt2( } else if(filename=="-") { - auto smt2_conv= - util_make_unique( - ns, - "cbmc", - "Generated by CBMC " CBMC_VERSION, - "QF_AUFBV", - solver, - std::cout); + auto smt2_conv = util_make_unique( + ns, + "cbmc", + std::string("Generated by CBMC ") + CBMC_VERSION, + "QF_AUFBV", + solver, + std::cout); if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory=true; @@ -218,14 +216,13 @@ std::unique_ptr cbmc_solverst::get_smt2( throw 0; } - auto smt2_conv= - util_make_unique( - ns, - "cbmc", - "Generated by CBMC " CBMC_VERSION, - "QF_AUFBV", - solver, - *out); + auto smt2_conv = util_make_unique( + ns, + "cbmc", + std::string("Generated by CBMC ") + CBMC_VERSION, + "QF_AUFBV", + solver, + *out); if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory=true; diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 83c2ad6f00..2855e5fa7e 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -35,10 +35,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv): - parse_options_baset(CLOBBER_OPTIONS, argc, argv), - language_uit(cmdline, ui_message_handler), - ui_message_handler(cmdline, "CLOBBER " CBMC_VERSION) +clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv) + : parse_options_baset(CLOBBER_OPTIONS, argc, argv), + language_uit(cmdline, ui_message_handler), + ui_message_handler(cmdline, std::string("CLOBBER ") + CBMC_VERSION) { } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4014ad0f58..038648adaf 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -64,10 +64,10 @@ Author: Daniel Kroening, kroening@kroening.com goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( int argc, - const char **argv): - parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv), - messaget(ui_message_handler), - ui_message_handler(cmdline, "GOTO-ANALYZER " CBMC_VERSION) + const char **argv) + : parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv), + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION) { } @@ -374,9 +374,8 @@ int goto_analyzer_parse_optionst::doit() // // Print a banner // - status() << "GOTO-ANALYSER version " CBMC_VERSION " " - << sizeof(void *)*8 << "-bit " - << config.this_architecture() << " " + status() << "GOTO-ANALYSER version " << CBMC_VERSION << " " + << sizeof(void *) * 8 << "-bit " << config.this_architecture() << " " << config.this_operating_system() << eom; register_languages(); diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index 8355fb2879..8d2a62e37d 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -82,17 +82,18 @@ int as_modet::doit() cmdline.isset("version")) { if(act_as_as86) - status() << "as86 version: 0.16.17 (goto-cc " CBMC_VERSION ")" + status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")" << eom; else status() << "GNU assembler version 2.20.51.0.7 20100318" - << " (goto-cc " CBMC_VERSION ")" << eom; + << " (goto-cc " << CBMC_VERSION << ")" << eom; - status() << '\n' << - "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" << - "CBMC version: " CBMC_VERSION << '\n' << - "Architecture: " << config.this_architecture() << '\n' << - "OS: " << config.this_operating_system() << eom; + status() + << '\n' + << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" + << "CBMC version: " << CBMC_VERSION << '\n' + << "Architecture: " << config.this_architecture() << '\n' + << "OS: " << config.this_operating_system() << eom; return EX_OK; // Exit! } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 2e586ce5c9..e83b1192da 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -677,7 +677,8 @@ unsigned compilet::function_body_count(const goto_functionst &functions) const void compilet::add_compiler_specific_defines(configt &config) const { - config.ansi_c.defines.push_back("__GOTO_CC_VERSION__=" CBMC_VERSION); + config.ansi_c.defines.push_back( + std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION); } void compilet::convert_symbols(goto_functionst &dest) diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 97d316e85b..24d7369b99 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -345,15 +345,16 @@ int gcc_modet::doit() // Compilation continues, don't exit! if(act_as_bcc) - std::cout << "bcc: version " << gcc_version - << " (goto-cc " CBMC_VERSION ")\n"; + std::cout << "bcc: version " << gcc_version << " (goto-cc " + << CBMC_VERSION << ")\n"; else { if(gcc_version.flavor == gcc_versiont::flavort::CLANG) - std::cout << "clang version " << gcc_version - << " (goto-cc " CBMC_VERSION ")\n"; + std::cout << "clang version " << gcc_version << " (goto-cc " + << CBMC_VERSION << ")\n"; else - std::cout << "gcc (goto-cc " CBMC_VERSION ") " << gcc_version << '\n'; + std::cout << "gcc (goto-cc " << CBMC_VERSION << ") " << gcc_version + << '\n'; } } @@ -371,7 +372,7 @@ int gcc_modet::doit() std::cout << '\n' << "Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n" - << "CBMC version: " CBMC_VERSION << '\n' + << "CBMC version: " << CBMC_VERSION << '\n' << "Architecture: " << config.this_architecture() << '\n' << "OS: " << config.this_operating_system() << '\n'; diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c09841c701..b307272be0 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -61,22 +61,22 @@ Author: Peter Schrammel #include "unified_diff.h" #include "change_impact.h" -goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv): - parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv), - goto_diff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION), - languages2(cmdline, ui_message_handler) +goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv) + : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv), + goto_diff_languagest(cmdline, ui_message_handler), + ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), + languages2(cmdline, ui_message_handler) { } ::goto_diff_parse_optionst::goto_diff_parse_optionst( int argc, const char **argv, - const std::string &extra_options): - parse_options_baset(GOTO_DIFF_OPTIONS+extra_options, argc, argv), - goto_diff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION), - languages2(cmdline, ui_message_handler) + const std::string &extra_options) + : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv), + goto_diff_languagest(cmdline, ui_message_handler), + ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), + languages2(cmdline, ui_message_handler) { } @@ -243,9 +243,8 @@ int goto_diff_parse_optionst::doit() // // Print a banner // - status() << "GOTO-DIFF version " CBMC_VERSION " " - << sizeof(void *)*8 << "-bit " - << config.this_architecture() << " " + status() << "GOTO-DIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8 + << "-bit " << config.this_architecture() << " " << config.this_operating_system() << eom; if(cmdline.args.size()!=2) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 710b8086a6..2100c47a54 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,9 +1,4 @@ file(GLOB_RECURSE sources "*.cpp" "*.h") -add_library(util ${sources}) - -generic_includes(util) - -target_link_libraries(util big-int langapi) # based on https://cmake.org/pipermail/cmake/2010-July/038015.html find_package(Git) @@ -18,7 +13,7 @@ if(GIT_FOUND) OUTPUT_VARIABLE GIT_INFO OUTPUT_STRIP_TRAILING_WHITESPACE ) - configure_file(\${CUR}/version.h.in version.h) + configure_file(\${CUR}/version.cpp.in version.cpp) " ) else() @@ -28,18 +23,25 @@ else() config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\") string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v}) set(GIT_INFO \"n/a\") - configure_file(\${CUR}/version.h.in version.h) + configure_file(\${CUR}/version.cpp.in version.cpp) " ) endif() -file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.h.in - "\#define CBMC_VERSION \"@CBMC_RELEASE@ (@GIT_INFO@)\"\n") -add_custom_target( - version.h +file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.cpp.in + "const char *CBMC_VERSION=\"@CBMC_RELEASE@ (@GIT_INFO@)\";\n") +add_custom_command( + OUTPUT version.cpp COMMAND ${CMAKE_COMMAND} -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR} -D CUR=${CMAKE_CURRENT_BINARY_DIR} -P ${CMAKE_BINARY_DIR}/version.cmake ) -add_dependencies(util version.h) + +add_library(util + ${sources} + version.cpp) + +generic_includes(util) + +target_link_libraries(util big-int langapi) diff --git a/src/util/Makefile b/src/util/Makefile index a0c34a66ad..df6b12a297 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -93,6 +93,7 @@ SRC = arith_tools.cpp \ union_find.cpp \ union_find_replace.cpp \ unwrap_nested_exception.cpp \ + version.cpp \ xml.cpp \ xml_expr.cpp \ xml_irep.cpp \ @@ -105,8 +106,8 @@ include ../common # get version from git GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") -RELEASE_INFO = \#define CBMC_VERSION "$(CBMC_VERSION) ($(GIT_INFO))" -GIT_INFO_FILE = version.h +RELEASE_INFO = const char *CBMC_VERSION="$(CBMC_VERSION) ($(GIT_INFO))"; +GIT_INFO_FILE = version.cpp $(GIT_INFO_FILE): echo '$(RELEASE_INFO)' > $@ diff --git a/src/util/version.h b/src/util/version.h new file mode 100644 index 0000000000..dcde3b18e6 --- /dev/null +++ b/src/util/version.h @@ -0,0 +1 @@ +extern const char *CBMC_VERSION;