diff --git a/.gitignore b/.gitignore index 822bd06e8bc..e751bb0f4da 100644 --- a/.gitignore +++ b/.gitignore @@ -28,6 +28,7 @@ Release/* *.obj *.a *.lib +.release_info src/ansi-c/arm_builtin_headers.inc src/ansi-c/clang_builtin_headers.inc src/ansi-c/cprover_builtin_headers.inc diff --git a/CMakeLists.txt b/CMakeLists.txt index d8de16b0011..2516d4c19de 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -38,6 +38,52 @@ if(${enable_cbmc_tests}) enable_testing() endif() +file(STRINGS src/config.inc config_inc_v REGEX "CBMC_VERSION *= *[0-9\.]+") +string(REGEX REPLACE "^CBMC_VERSION *= *" "" CBMC_RELEASE ${config_inc_v}) +message(STATUS "CBMC release ${CBMC_RELEASE}") + +find_package(Git) + +macro(git_revision target files_var) + if(GIT_FOUND) + add_custom_command( + OUTPUT .release_info + COMMAND ${CMAKE_COMMAND} -E echo_append "#define __CBMC_VERSION " > .release_info + COMMAND "${GIT_EXECUTABLE}" "describe" "--tags" "--always" "--long" >> .release_info + COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_str(v) \"${CBMC_RELEASE} (\" # v \")\"" >> .release_info + COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_xstr(v) __CBMC_VERSION_str(v)" >> .release_info + COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION __CBMC_VERSION_xstr(__CBMC_VERSION)" >> .release_info + VERBATIM + ) + add_custom_command( + TARGET ${target} + POST_BUILD + COMMAND ${CMAKE_COMMAND} -E remove -f .release_info + ) + else() + add_custom_command( + OUTPUT .release_info + COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION \"${CBMC_RELEASE} (n/a)\"" >> .release_info + VERBATIM + ) + endif() + + if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR + "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" + ) + set_source_files_properties( + ${${files_var}} + PROPERTIES + OBJECT_DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/.release_info + COMPILE_FLAGS "-include .release_info") + elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") + set_source_files_properties( + ${${files_var}} + PROPERTIES + COMPILE_FLAGS "/DCBMC_VERSION=\"${CBMC_RELEASE} (n/a)\"") + endif() +endmacro() + add_subdirectory(src) add_subdirectory(regression) add_subdirectory(unit) diff --git a/jbmc/src/janalyzer/CMakeLists.txt b/jbmc/src/janalyzer/CMakeLists.txt index f4ff29ae0d4..dfb42b409f8 100644 --- a/jbmc/src/janalyzer/CMakeLists.txt +++ b/jbmc/src/janalyzer/CMakeLists.txt @@ -24,3 +24,6 @@ target_link_libraries(janalyzer-lib # Executable add_executable(janalyzer janalyzer_main.cpp) target_link_libraries(janalyzer janalyzer-lib) + +set(cbmc_version_files janalyzer_parse_options.cpp) +git_revision(janalyzer-lib cbmc_version_files) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 243ca8682b5..d8daccfd60f 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -50,8 +50,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include #include @@ -723,17 +721,11 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options) /// display command line help void janalyzer_parse_optionst::help() { - std::cout << "\n" - "* * JANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 "; - - std::cout << "(" << (sizeof(void *) * 8) << "-bit version)"; - - std::cout << " * *\n"; - // clang-format off - std::cout << + std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n' + << /* NOLINTNEXTLINE(whitespace/line_length) */ - "* * JANALYZER " CBMC_VERSION " - Copyright (C) 2016-2018 * *\n" + "* * Copyright (C) 2016-2018 * *\n" "* * Daniel Kroening, Diffblue * *\n" "* * kroening@kroening.com * *\n" "\n" diff --git a/jbmc/src/janalyzer/module_dependencies.txt b/jbmc/src/janalyzer/module_dependencies.txt index cc11b9898b7..1aa013f0c31 100644 --- a/jbmc/src/janalyzer/module_dependencies.txt +++ b/jbmc/src/janalyzer/module_dependencies.txt @@ -1,6 +1,5 @@ analyses ansi-c # should go away -cbmc # version.h java_bytecode jdiff goto-analyzer diff --git a/jbmc/src/jbmc/CMakeLists.txt b/jbmc/src/jbmc/CMakeLists.txt index 7015ae0fdbe..706797abbcc 100644 --- a/jbmc/src/jbmc/CMakeLists.txt +++ b/jbmc/src/jbmc/CMakeLists.txt @@ -29,3 +29,6 @@ target_link_libraries(jbmc-lib # Executable add_executable(jbmc jbmc_main.cpp) target_link_libraries(jbmc jbmc-lib) + +set(cbmc_version_files jbmc_parse_options.cpp) +git_revision(jbmc-lib cbmc_version_files) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index aef623f4536..2869050ffcb 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -60,8 +60,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv): parse_options_baset(JBMC_OPTIONS, argc, argv), messaget(ui_message_handler), @@ -1069,15 +1067,10 @@ bool jbmc_parse_optionst::generate_function_body( /// display command line help void jbmc_parse_optionst::help() { - std::cout << "\n" - "* * JBMC " CBMC_VERSION " - Copyright (C) 2001-2018 "; - - std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; - - std::cout << " * *\n"; - // clang-format off - std::cout << + std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2001-2018 * *\n" "* * Daniel Kroening, Edmund Clarke * *\n" "* * Carnegie Mellon University, Computer Science Department * *\n" "* * kroening@kroening.com * *\n" diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt index 76529547422..1c492ac0359 100644 --- a/jbmc/src/jbmc/module_dependencies.txt +++ b/jbmc/src/jbmc/module_dependencies.txt @@ -1,6 +1,6 @@ analyses ansi-c # should go away -cbmc # version.h and bmc.h +cbmc # bmc.h goto-instrument goto-programs goto-symex diff --git a/jbmc/src/jdiff/CMakeLists.txt b/jbmc/src/jdiff/CMakeLists.txt index 1f1b82e6ad2..04d6122e95e 100644 --- a/jbmc/src/jdiff/CMakeLists.txt +++ b/jbmc/src/jdiff/CMakeLists.txt @@ -26,3 +26,6 @@ target_link_libraries(jdiff-lib # Executable add_executable(jdiff jdiff_main.cpp) target_link_libraries(jdiff jdiff-lib) + +set(cbmc_version_files jdiff_parse_options.cpp) +git_revision(jdiff-lib cbmc_version_files) diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 402123877fa..1f4e875ab2f 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -55,8 +55,6 @@ Author: Peter Schrammel #include -#include - #include "java_syntactic_diff.h" #include #include @@ -429,10 +427,9 @@ bool jdiff_parse_optionst::process_goto_program( void jdiff_parse_optionst::help() { // clang-format off - std::cout << - "\n" - // NOLINTNEXTLINE(whitespace/line_length) - "* * JDIFF " CBMC_VERSION " - Copyright (C) 2016-2018 * *\n" + std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2016-2018 * *\n" "* * Daniel Kroening, Peter Schrammel * *\n" "* * kroening@kroening.com * *\n" "\n" diff --git a/jbmc/src/jdiff/module_dependencies.txt b/jbmc/src/jdiff/module_dependencies.txt index 5c97868ddf1..05504d848ca 100644 --- a/jbmc/src/jdiff/module_dependencies.txt +++ b/jbmc/src/jdiff/module_dependencies.txt @@ -1,5 +1,4 @@ analyses -cbmc # version.h java_bytecode jdiff goto-diff diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index b1cae0f8b01..e3b69f6daf0 100644 --- a/src/cbmc/CMakeLists.txt +++ b/src/cbmc/CMakeLists.txt @@ -31,3 +31,6 @@ add_if_library(cbmc-lib jsil) # Executable add_executable(cbmc cbmc_main.cpp) target_link_libraries(cbmc cbmc-lib) + +set(cbmc_version_files cbmc_parse_options.cpp cbmc_solvers.cpp) +git_revision(cbmc-lib cbmc_version_files) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index e1045b7bc9c..a00997b7531 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -56,6 +56,8 @@ INCLUDES= -I .. LIBS = +CBMC_VERSION_FILES = cbmc_solvers$(OBJEXT) + include ../config.inc include ../common diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 2df3984c6e4..4bc131fab38 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -62,7 +62,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "version.h" #include "xml_interface.h" cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv): @@ -867,15 +866,9 @@ bool cbmc_parse_optionst::process_goto_program( void cbmc_parse_optionst::help() { // clang-format off - std::cout << - "\n" - "* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2018 "; - - std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; - - std::cout << " * *\n"; - - std::cout << + std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2001-2018 * *\n" "* * Daniel Kroening, Edmund Clarke * *\n" "* * Carnegie Mellon University, Computer Science Department * *\n" "* * kroening@kroening.com * *\n" diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 8b216839f92..da9f28b8c36 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -28,7 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "bv_cbmc.h" #include "cbmc_dimacs.h" #include "counterexample_beautification.h" -#include "version.h" /// Uses the options to pick an SMT 2.0 solver /// \return An smt2_dect::solvert giving the solver to use. diff --git a/src/cbmc/version.h b/src/cbmc/version.h deleted file mode 100644 index 535f7027b8c..00000000000 --- a/src/cbmc/version.h +++ /dev/null @@ -1,14 +0,0 @@ -/*******************************************************************\ - -Module: Bounded Model Checking for ANSI-C + HDL - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_CBMC_VERSION_H -#define CPROVER_CBMC_VERSION_H - -#define CBMC_VERSION "5.8" - -#endif // CPROVER_CBMC_VERSION_H diff --git a/src/clobber/CMakeLists.txt b/src/clobber/CMakeLists.txt index a67792c0e87..02194f9511e 100644 --- a/src/clobber/CMakeLists.txt +++ b/src/clobber/CMakeLists.txt @@ -30,3 +30,5 @@ add_if_library(clobber-lib bv_refinement) add_executable(clobber clobber_main.cpp) target_link_libraries(clobber clobber-lib) +set(cbmc_version_files clobber_parse_options.cpp) +git_revision(clobber-lib cbmc_version_files) diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 0ee4ad81fee..715cd0b4acb 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -34,7 +34,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv): parse_options_baset(CLOBBER_OPTIONS, argc, argv), @@ -349,15 +348,10 @@ void clobber_parse_optionst::report_failure() /// display command line help void clobber_parse_optionst::help() { - std::cout << - "\n" - "* * CLOBBER " CBMC_VERSION " - Copyright (C) 2014 "; - - std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; - - std::cout << " * *\n"; - - std::cout << + // clang-format off + std::cout << '\n' << banner_string("CLOBBER", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2014 * *\n" "* * Daniel Kroening * *\n" "* * University of Oxford * *\n" "* * kroening@kroening.com * *\n" @@ -415,4 +409,5 @@ void clobber_parse_optionst::help() " --version show version and exit\n" " --xml-ui use XML-formatted output\n" "\n"; + // clang-format on } diff --git a/src/common b/src/common index ee9cc79d63f..ba8d0b89ba3 100644 --- a/src/common +++ b/src/common @@ -227,12 +227,40 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) %.obj:%.c $(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@ +# get version from git +GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") +GIT_INFO_FILE = .release_info + +CBMC_VERSION_FILES += $(filter %_parse_options$(OBJEXT), $(OBJ)) + +ifeq ($(BUILD_ENV_),MSVC) +$(CBMC_VERSION_FILES): CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""' +else +$(CBMC_VERSION_FILES): CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" +endif + +# Use make >= 4.0's `file` function, if available - it should be faster than +# `shell cat` +ifeq ($(firstword $(subst ., , $(MAKE_VERSION))), 3) +KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null) +else +KNOWN_RELEASE_INFO = $(file < $(GIT_INFO_FILE)) +endif +ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO)) +$(CBMC_VERSION_FILES): $(GIT_INFO_FILE) + +$(GIT_INFO_FILE): + echo $(GIT_INFO) > $@ + +.PHONY: $(GIT_INFO_FILE) +endif + clean: $(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \ $(patsubst %.cpp, %$(DEPEXT), $(filter %.cpp, $(SRC))) \ $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \ $(patsubst %.cc, %$(DEPEXT), $(filter %.cc, $(SRC))) \ - $(CLEANFILES) + $(CLEANFILES) $(GIT_INFO_FILE) .PHONY: first_target clean all .PHONY: sources generated_files @@ -252,4 +280,3 @@ D_FILES1 = $(SRC:.c=$(DEPEXT)) D_FILES = $(D_FILES1:.cpp=$(DEPEXT)) -include $(D_FILES) - diff --git a/src/config.inc b/src/config.inc index 0f79c2cb2fe..931ec261114 100644 --- a/src/config.inc +++ b/src/config.inc @@ -70,3 +70,6 @@ endif # Signing identity for MacOS Gatekeeper OSX_IDENTITY="Developer ID Application: Daniel Kroening" + +# Detailed version information +CBMC_VERSION = 5.8 diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt index 0ad6aadc0de..a2373d2138a 100644 --- a/src/goto-analyzer/CMakeLists.txt +++ b/src/goto-analyzer/CMakeLists.txt @@ -26,3 +26,6 @@ add_if_library(goto-analyzer-lib jsil) # Executable add_executable(goto-analyzer goto_analyzer_main.cpp) target_link_libraries(goto-analyzer goto-analyzer-lib) + +set(cbmc_version_files goto_analyzer_parse_options.cpp) +git_revision(goto-analyzer-lib cbmc_version_files) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4fd380ed877..b7bede4b04d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -54,7 +54,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "taint_analysis.h" @@ -790,15 +789,10 @@ bool goto_analyzer_parse_optionst::process_goto_program( /// display command line help void goto_analyzer_parse_optionst::help() { - std::cout << "\n" - "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 "; - - std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; - - std::cout << " * *\n"; - // clang-format off - std::cout << + std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2017-2018 * *\n" "* * Daniel Kroening, DiffBlue * *\n" "* * kroening@kroening.com * *\n" "\n" diff --git a/src/goto-analyzer/module_dependencies.txt b/src/goto-analyzer/module_dependencies.txt index e3ad5a094da..fbe3c1b8b0a 100644 --- a/src/goto-analyzer/module_dependencies.txt +++ b/src/goto-analyzer/module_dependencies.txt @@ -1,6 +1,5 @@ ansi-c analyses -cbmc # version.h cpp goto-analyzer goto-programs diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt index bd281a73c93..504f54a8ea6 100644 --- a/src/goto-cc/CMakeLists.txt +++ b/src/goto-cc/CMakeLists.txt @@ -34,3 +34,6 @@ else() COMMAND "${CMAKE_COMMAND}" -E create_symlink goto-cc $/goto-gcc) endif() + +set(cbmc_version_files as_mode.cpp compile.cpp gcc_mode.cpp goto_cc_mode.cpp) +git_revision(goto-cc-lib cbmc_version_files) diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 3e8e6e8bdb1..976cc339d77 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -38,6 +38,11 @@ LIBS = CLEANFILES = goto-cc$(EXEEXT) goto-cl$(EXEEXT) +CBMC_VERSION_FILES = as_mode$(OBJEXT) \ + compile$(OBJEXT) \ + gcc_mode$(OBJEXT) \ + goto_cc_mode$(OBJEXT) + include ../config.inc include ../common diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index d130e63cb94..b7796e945c0 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -29,8 +29,6 @@ Author: Michael Tautschnig #include #include -#include - #include "compile.h" static std::string assembler_name( diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 1a29d8bf6c1..671de8d5893 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -37,8 +37,6 @@ Date: June 2006 #include -#include - #define DOTGRAPHSETTINGS "color=black;" \ "orientation=portrait;" \ "fontsize=20;"\ diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index bb004c51540..143465ac278 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -46,8 +46,6 @@ Author: CM Wintersteiger, 2006 #include -#include - #include "hybrid_binary.h" #include "linker_script_merge.h" diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp index 81fda73ecbb..d42201c4a50 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -22,7 +22,7 @@ Author: CM Wintersteiger, 2006 #include #endif -#include +#include /// constructor goto_cc_modet::goto_cc_modet( @@ -44,10 +44,10 @@ goto_cc_modet::~goto_cc_modet() /// display command line help void goto_cc_modet::help() { - std::cout << - "\n" - // NOLINTNEXTLINE(whitespace/line_length) - "* * goto-cc " CBMC_VERSION " - Copyright (C) 2006-2018 * *\n" + // clang-format off + std::cout << '\n' << banner_string("goto-cc", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2006-2018 * *\n" "* * Daniel Kroening, Michael Tautschnig, * *\n" "* * Christoph Wintersteiger * *\n" "\n"; @@ -65,6 +65,7 @@ void goto_cc_modet::help() " --print-rejected-preprocessed-source file\n" " copy failing (preprocessed) source to file\n" "\n"; + // clang-format on } /// starts the compiler diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp index 84dd936b986..12b316ee3e1 100644 --- a/src/goto-cc/ld_mode.cpp +++ b/src/goto-cc/ld_mode.cpp @@ -46,8 +46,6 @@ Author: CM Wintersteiger, 2006 #include -#include - #include "hybrid_binary.h" #include "linker_script_merge.h" diff --git a/src/goto-cc/module_dependencies.txt b/src/goto-cc/module_dependencies.txt index 6d867541014..1e28f751979 100644 --- a/src/goto-cc/module_dependencies.txt +++ b/src/goto-cc/module_dependencies.txt @@ -1,5 +1,4 @@ ansi-c -cbmc # version.h cpp goto-cc goto-programs diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index 5a459ac048c..08d845c1bab 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -26,8 +26,6 @@ Author: CM Wintersteiger, 2006 #include #include -#include - #include "compile.h" /// does it. diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index 080bb643e66..43dd2fc88da 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -28,3 +28,6 @@ add_if_library(goto-diff-lib jsil) # Executable add_executable(goto-diff goto_diff_main.cpp) target_link_libraries(goto-diff goto-diff-lib) + +set(cbmc_version_files goto_diff_parse_options.cpp) +git_revision(goto-diff-lib cbmc_version_files) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index a106114cca5..1a6c82240f4 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -55,8 +55,6 @@ Author: Peter Schrammel #include #include -#include - #include "goto_diff.h" #include "syntactic_diff.h" #include "unified_diff.h" @@ -486,10 +484,9 @@ bool goto_diff_parse_optionst::process_goto_program( void goto_diff_parse_optionst::help() { // clang-format off - std::cout << - "\n" - // NOLINTNEXTLINE(whitespace/line_length) - "* * GOTO_DIFF " CBMC_VERSION " - Copyright (C) 2016 * *\n" + std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2016 * *\n" "* * Daniel Kroening, Peter Schrammel * *\n" "* * kroening@kroening.com * *\n" "\n" diff --git a/src/goto-diff/module_dependencies.txt b/src/goto-diff/module_dependencies.txt index cd004e5e879..e2660397624 100644 --- a/src/goto-diff/module_dependencies.txt +++ b/src/goto-diff/module_dependencies.txt @@ -1,6 +1,5 @@ analyses ansi-c -cbmc # version.h cpp goto-diff goto-instrument diff --git a/src/goto-instrument/CMakeLists.txt b/src/goto-instrument/CMakeLists.txt index 30350ca03b2..225fa1200ea 100644 --- a/src/goto-instrument/CMakeLists.txt +++ b/src/goto-instrument/CMakeLists.txt @@ -32,3 +32,6 @@ add_if_library(goto-instrument-lib glpk) # Executable add_executable(goto-instrument goto_instrument_main.cpp) target_link_libraries(goto-instrument goto-instrument-lib) + +set(cbmc_version_files "goto_instrument_parse_options.cpp") +git_revision(goto-instrument-lib cbmc_version_files) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index efe68017124..9afe3be526c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -65,8 +65,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include "document_properties.h" #include "uninitialized.h" #include "full_slicer.h" @@ -1441,9 +1439,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() void goto_instrument_parse_optionst::help() { // clang-format off - std::cout << - "\n" - "* * Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013 * *\n" // NOLINT(*) + std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n' + << + "* * Copyright (C) 2008-2013 * *\n" "* * Daniel Kroening * *\n" "* * kroening@kroening.com * *\n" "\n" diff --git a/src/goto-instrument/module_dependencies.txt b/src/goto-instrument/module_dependencies.txt index 44bc38028be..a5e8c9fa445 100644 --- a/src/goto-instrument/module_dependencies.txt +++ b/src/goto-instrument/module_dependencies.txt @@ -1,7 +1,6 @@ accelerate analyses ansi-c -cbmc # version.h cpp goto-instrument goto-programs diff --git a/src/memory-models/CMakeLists.txt b/src/memory-models/CMakeLists.txt index 9cb6152a86f..4fc92ff6f12 100644 --- a/src/memory-models/CMakeLists.txt +++ b/src/memory-models/CMakeLists.txt @@ -11,3 +11,6 @@ add_library(mmcc generic_includes(mmcc) target_link_libraries(mmcc util) + +set(cbmc_version_files mmcc_parse_options.cpp) +git_revision(mmcc cbmc_version_files) diff --git a/src/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp index 03644ab95f5..d0c7dcbbc94 100644 --- a/src/memory-models/mmcc_parse_options.cpp +++ b/src/memory-models/mmcc_parse_options.cpp @@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include "mm_parser.h" #include "mm2cpp.h" @@ -97,11 +95,10 @@ int mmcc_parse_optionst::convert( /// display command line help void mmcc_parse_optionst::help() { - std::cout << - "\n" - "* * MMCC " CBMC_VERSION " - Copyright (C) 2015-2015 * *\n"; - - std::cout << + // clang-format off + std::cout << '\n' << banner_string("MMCC", CBMC_VERSION) << '\n' + << + " Copyright (C) 2015-2015\n" "\n" "Usage: Purpose:\n" "\n" @@ -109,4 +106,5 @@ void mmcc_parse_optionst::help() " mmcc file.cat convert given source file\n" " mmcc convert from stdin\n" "\n"; + // clang-format on } diff --git a/src/memory-models/module_dependencies.txt b/src/memory-models/module_dependencies.txt index f53e123b0fd..b6eeb0c5f01 100644 --- a/src/memory-models/module_dependencies.txt +++ b/src/memory-models/module_dependencies.txt @@ -1,4 +1,3 @@ -cbmc # version.h memory-models langapi # should go away util diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 79feb29bc8f..2428c236889 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -65,3 +65,20 @@ int parse_options_baset::main() return doit(); } + +std::string +banner_string(const std::string &front_end, const std::string &version) +{ + const std::string version_str = front_end + " " + version + " " + + std::to_string(sizeof(void *) * 8) + "-bit"; + + std::string::size_type left_padding = 0, right_padding = 0; + if(version_str.size() < 57) + { + left_padding = (57 - version_str.size() + 1) / 2; + right_padding = (57 - version_str.size()) / 2; + } + + return "* *" + std::string(left_padding, ' ') + version_str + + std::string(right_padding, ' ') + "* *"; +} diff --git a/src/util/parse_options.h b/src/util/parse_options.h index b2e64722e85..6b2b982fd51 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -35,4 +35,7 @@ class parse_options_baset bool parse_result; }; +std::string +banner_string(const std::string &front_end, const std::string &version); + #endif // CPROVER_UTIL_PARSE_OPTIONS_H