From 7ca835bac3c6b8010ad0607597759ce84e8b1a74 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Jun 2018 12:59:15 +0100 Subject: [PATCH 1/5] Added CBMC_VERSION defines to CMake configuration --- CMakeLists.txt | 42 ++++++++++++++++++++++++++++++ jbmc/src/janalyzer/CMakeLists.txt | 3 +++ jbmc/src/jbmc/CMakeLists.txt | 3 +++ jbmc/src/jdiff/CMakeLists.txt | 3 +++ src/cbmc/CMakeLists.txt | 3 +++ src/clobber/CMakeLists.txt | 2 ++ src/goto-analyzer/CMakeLists.txt | 3 +++ src/goto-cc/CMakeLists.txt | 3 +++ src/goto-diff/CMakeLists.txt | 3 +++ src/goto-instrument/CMakeLists.txt | 3 +++ src/memory-models/CMakeLists.txt | 3 +++ 11 files changed, 71 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index d8de16b0011..7d7028bec95 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -38,6 +38,48 @@ if(${enable_cbmc_tests}) enable_testing() endif() +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/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/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/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/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/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-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-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-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/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) From 23455af5497c8410b31039be42abe08c99d86e36 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 31 May 2016 17:22:21 +0000 Subject: [PATCH 2/5] Print git revision with all --version outputs This uses the output of `git-describe --tags --always --dirty` to create a UID for binaries. This includes last tag, number of commits after last tag, shortened SHA1 checksum and optional dirty flag for uncommited changes. In case of tagged commit, only the tag name is used. --- CMakeLists.txt | 4 ++++ jbmc/src/janalyzer/Makefile | 2 ++ jbmc/src/janalyzer/janalyzer_parse_options.cpp | 2 -- jbmc/src/janalyzer/module_dependencies.txt | 1 - jbmc/src/jbmc/Makefile | 2 ++ jbmc/src/jbmc/jbmc_parse_options.cpp | 2 -- jbmc/src/jbmc/module_dependencies.txt | 2 +- jbmc/src/jdiff/Makefile | 2 ++ jbmc/src/jdiff/jdiff_parse_options.cpp | 2 -- jbmc/src/jdiff/module_dependencies.txt | 1 - src/cbmc/Makefile | 2 ++ src/cbmc/cbmc_parse_options.cpp | 1 - src/cbmc/cbmc_solvers.cpp | 1 - src/cbmc/version.h | 14 -------------- src/clobber/Makefile | 2 ++ src/clobber/clobber_parse_options.cpp | 1 - src/config.inc | 4 ++++ src/goto-analyzer/Makefile | 2 ++ src/goto-analyzer/goto_analyzer_parse_options.cpp | 1 - src/goto-analyzer/module_dependencies.txt | 1 - src/goto-cc/Makefile | 2 ++ src/goto-cc/as_mode.cpp | 2 -- src/goto-cc/compile.cpp | 2 -- src/goto-cc/gcc_mode.cpp | 2 -- src/goto-cc/goto_cc_mode.cpp | 1 - src/goto-cc/ld_mode.cpp | 2 -- src/goto-cc/module_dependencies.txt | 1 - src/goto-cc/ms_cl_mode.cpp | 2 -- src/goto-diff/Makefile | 2 ++ src/goto-diff/goto_diff_parse_options.cpp | 2 -- src/goto-diff/module_dependencies.txt | 1 - src/goto-instrument/Makefile | 2 ++ .../goto_instrument_parse_options.cpp | 2 -- src/goto-instrument/module_dependencies.txt | 1 - src/memory-models/Makefile | 2 ++ src/memory-models/mmcc_parse_options.cpp | 2 -- src/memory-models/module_dependencies.txt | 1 - 37 files changed, 29 insertions(+), 49 deletions(-) delete mode 100644 src/cbmc/version.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 7d7028bec95..2516d4c19de 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -38,6 +38,10 @@ 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) diff --git a/jbmc/src/janalyzer/Makefile b/jbmc/src/janalyzer/Makefile index 879939a34d0..8c0701a542d 100644 --- a/jbmc/src/janalyzer/Makefile +++ b/jbmc/src/janalyzer/Makefile @@ -33,6 +33,8 @@ CLEANFILES = janalyzer$(EXEEXT) all: janalyzer$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ifneq ($(wildcard ../jsil/Makefile),) OBJ += ../jsil/jsil$(LIBEXT) CP_CXXFLAGS += -DHAVE_JSIL diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 243ca8682b5..04d50fa9322 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 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/Makefile b/jbmc/src/jbmc/Makefile index ab8c2c962aa..1039c1d48d8 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -63,6 +63,8 @@ CLEANFILES = jbmc$(EXEEXT) all: jbmc$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ############################################################################### jbmc$(EXEEXT): $(OBJ) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index aef623f4536..ca6866cf5bd 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), 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/Makefile b/jbmc/src/jdiff/Makefile index 83742a846d2..1d4ef6a804a 100644 --- a/jbmc/src/jdiff/Makefile +++ b/jbmc/src/jdiff/Makefile @@ -45,6 +45,8 @@ CLEANFILES = jdiff$(EXEEXT) all: jdiff$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ############################################################################### jdiff$(EXEEXT): $(OBJ) diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 402123877fa..00cfe627e61 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 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/Makefile b/src/cbmc/Makefile index e1045b7bc9c..ec463d145b7 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -63,6 +63,8 @@ CLEANFILES = cbmc$(EXEEXT) all: cbmc$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) CP_CXXFLAGS += -DHAVE_BV_REFINEMENT diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 2df3984c6e4..f50bba8e7fe 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): 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/Makefile b/src/clobber/Makefile index 459cae23cd9..456ab7a9546 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -30,6 +30,8 @@ CLEANFILES = clobber$(EXEEXT) all: clobber$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ############################################################################### clobber$(EXEEXT): $(OBJ) diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 0ee4ad81fee..d25550225a0 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), diff --git a/src/config.inc b/src/config.inc index 0f79c2cb2fe..045bf608cb4 100644 --- a/src/config.inc +++ b/src/config.inc @@ -70,3 +70,7 @@ endif # Signing identity for MacOS Gatekeeper OSX_IDENTITY="Developer ID Application: Daniel Kroening" + +# Detailed version information +CBMC_VERSION = 5.8 +GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 2d4a9d99785..d42ac58f1c1 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -32,6 +32,8 @@ CLEANFILES = goto-analyzer$(EXEEXT) all: goto-analyzer$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ifneq ($(wildcard ../jsil/Makefile),) OBJ += ../jsil/jsil$(LIBEXT) CP_CXXFLAGS += -DHAVE_JSIL diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4fd380ed877..de6d6186e8e 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" 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/Makefile b/src/goto-cc/Makefile index 3e8e6e8bdb1..a966a87a04f 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -46,6 +46,8 @@ all: goto-cl$(EXEEXT) endif all: goto-cc$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ifneq ($(wildcard ../jsil/Makefile),) OBJ += ../jsil/jsil$(LIBEXT) CP_CXXFLAGS += -DHAVE_JSIL 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..b74d9037bcf 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -22,7 +22,6 @@ Author: CM Wintersteiger, 2006 #include #endif -#include /// constructor goto_cc_modet::goto_cc_modet( 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/Makefile b/src/goto-diff/Makefile index 167eef00160..3536e07c50e 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -44,6 +44,8 @@ CLEANFILES = goto-diff$(EXEEXT) all: goto-diff$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ############################################################################### goto-diff$(EXEEXT): $(OBJ) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index a106114cca5..5de31e9ac43 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" 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/Makefile b/src/goto-instrument/Makefile index eb67f14f140..c19593807d7 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -101,6 +101,8 @@ include ../common all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) CP_CXXFLAGS += -DHAVE_GLPK diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index efe68017124..2b3c106469f 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" 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/Makefile b/src/memory-models/Makefile index 3b8587611c8..d8a59704a95 100644 --- a/src/memory-models/Makefile +++ b/src/memory-models/Makefile @@ -22,6 +22,8 @@ CLEANFILES = memory_models$(LIBEXT) \ all: mmcc$(EXEEXT) +CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" + ############################################################################### mm_y.tab.cpp: parser.y diff --git a/src/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp index 03644ab95f5..605139febe8 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" 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 From 64163725f4ef2486d6dc55263bbcdb6916db9b7e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 23 Mar 2017 11:12:42 +0100 Subject: [PATCH 3/5] windowsify compiler options --- jbmc/src/janalyzer/Makefile | 2 -- jbmc/src/jbmc/Makefile | 2 -- jbmc/src/jdiff/Makefile | 2 -- src/cbmc/Makefile | 4 ++-- src/clobber/Makefile | 2 -- src/common | 12 +++++++++++- src/config.inc | 1 - src/goto-analyzer/Makefile | 2 -- src/goto-cc/Makefile | 7 +++++-- src/goto-diff/Makefile | 2 -- src/goto-instrument/Makefile | 2 -- src/memory-models/Makefile | 2 -- 12 files changed, 18 insertions(+), 22 deletions(-) diff --git a/jbmc/src/janalyzer/Makefile b/jbmc/src/janalyzer/Makefile index 8c0701a542d..879939a34d0 100644 --- a/jbmc/src/janalyzer/Makefile +++ b/jbmc/src/janalyzer/Makefile @@ -33,8 +33,6 @@ CLEANFILES = janalyzer$(EXEEXT) all: janalyzer$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ifneq ($(wildcard ../jsil/Makefile),) OBJ += ../jsil/jsil$(LIBEXT) CP_CXXFLAGS += -DHAVE_JSIL diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index 1039c1d48d8..ab8c2c962aa 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -63,8 +63,6 @@ CLEANFILES = jbmc$(EXEEXT) all: jbmc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ############################################################################### jbmc$(EXEEXT): $(OBJ) diff --git a/jbmc/src/jdiff/Makefile b/jbmc/src/jdiff/Makefile index 1d4ef6a804a..83742a846d2 100644 --- a/jbmc/src/jdiff/Makefile +++ b/jbmc/src/jdiff/Makefile @@ -45,8 +45,6 @@ CLEANFILES = jdiff$(EXEEXT) all: jdiff$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ############################################################################### jdiff$(EXEEXT): $(OBJ) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index ec463d145b7..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 @@ -63,8 +65,6 @@ CLEANFILES = cbmc$(EXEEXT) all: cbmc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ifneq ($(wildcard ../bv_refinement/Makefile),) OBJ += ../bv_refinement/bv_refinement$(LIBEXT) CP_CXXFLAGS += -DHAVE_BV_REFINEMENT diff --git a/src/clobber/Makefile b/src/clobber/Makefile index 456ab7a9546..459cae23cd9 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -30,8 +30,6 @@ CLEANFILES = clobber$(EXEEXT) all: clobber$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ############################################################################### clobber$(EXEEXT): $(OBJ) diff --git a/src/common b/src/common index ee9cc79d63f..7194df514de 100644 --- a/src/common +++ b/src/common @@ -227,6 +227,17 @@ 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") + +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 + clean: $(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \ $(patsubst %.cpp, %$(DEPEXT), $(filter %.cpp, $(SRC))) \ @@ -252,4 +263,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 045bf608cb4..931ec261114 100644 --- a/src/config.inc +++ b/src/config.inc @@ -73,4 +73,3 @@ OSX_IDENTITY="Developer ID Application: Daniel Kroening" # Detailed version information CBMC_VERSION = 5.8 -GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index d42ac58f1c1..2d4a9d99785 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -32,8 +32,6 @@ CLEANFILES = goto-analyzer$(EXEEXT) all: goto-analyzer$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ifneq ($(wildcard ../jsil/Makefile),) OBJ += ../jsil/jsil$(LIBEXT) CP_CXXFLAGS += -DHAVE_JSIL diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index a966a87a04f..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 @@ -46,8 +51,6 @@ all: goto-cl$(EXEEXT) endif all: goto-cc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ifneq ($(wildcard ../jsil/Makefile),) OBJ += ../jsil/jsil$(LIBEXT) CP_CXXFLAGS += -DHAVE_JSIL diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 3536e07c50e..167eef00160 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -44,8 +44,6 @@ CLEANFILES = goto-diff$(EXEEXT) all: goto-diff$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ############################################################################### goto-diff$(EXEEXT): $(OBJ) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index c19593807d7..eb67f14f140 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -101,8 +101,6 @@ include ../common all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) CP_CXXFLAGS += -DHAVE_GLPK diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile index d8a59704a95..3b8587611c8 100644 --- a/src/memory-models/Makefile +++ b/src/memory-models/Makefile @@ -22,8 +22,6 @@ CLEANFILES = memory_models$(LIBEXT) \ all: mmcc$(EXEEXT) -CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\"" - ############################################################################### mm_y.tab.cpp: parser.y From 718e926870dc3ed0a6c89b08041b55c15be2ff88 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Mar 2017 13:30:25 +0000 Subject: [PATCH 4/5] Build .release_info files containing the version string By adding build-dependencies to all *_parse_options files whenever the contents of .release_info files differs from $(RELEASE_INFO), we ensure that binaries print the correct version strings. --- .gitignore | 1 + src/common | 19 ++++++++++++++++++- 2 files changed, 19 insertions(+), 1 deletion(-) 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/src/common b/src/common index 7194df514de..ba8d0b89ba3 100644 --- a/src/common +++ b/src/common @@ -229,6 +229,7 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) # 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)) @@ -238,12 +239,28 @@ 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 From 4b124c86dcec92e2803b8fe768a782e7d83c89f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 10 May 2017 12:24:25 +0200 Subject: [PATCH 5/5] add centered git version to CBMC banner --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 12 +++--------- jbmc/src/jbmc/jbmc_parse_options.cpp | 11 +++-------- jbmc/src/jdiff/jdiff_parse_options.cpp | 7 +++---- src/cbmc/cbmc_parse_options.cpp | 12 +++--------- src/clobber/clobber_parse_options.cpp | 14 +++++--------- .../goto_analyzer_parse_options.cpp | 11 +++-------- src/goto-cc/goto_cc_mode.cpp | 10 ++++++---- src/goto-diff/goto_diff_parse_options.cpp | 7 +++---- .../goto_instrument_parse_options.cpp | 6 +++--- src/memory-models/mmcc_parse_options.cpp | 10 +++++----- src/util/parse_options.cpp | 17 +++++++++++++++++ src/util/parse_options.h | 3 +++ 12 files changed, 57 insertions(+), 63 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 04d50fa9322..d8daccfd60f 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -721,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/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index ca6866cf5bd..2869050ffcb 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -1067,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/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 00cfe627e61..1f4e875ab2f 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -427,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/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f50bba8e7fe..4bc131fab38 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -866,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/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index d25550225a0..715cd0b4acb 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -348,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" @@ -414,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/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index de6d6186e8e..b7bede4b04d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -789,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-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp index b74d9037bcf..d42201c4a50 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -22,6 +22,7 @@ Author: CM Wintersteiger, 2006 #include #endif +#include /// constructor goto_cc_modet::goto_cc_modet( @@ -43,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"; @@ -64,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-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 5de31e9ac43..1a6c82240f4 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -484,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-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 2b3c106469f..9afe3be526c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1439,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/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp index 605139febe8..d0c7dcbbc94 100644 --- a/src/memory-models/mmcc_parse_options.cpp +++ b/src/memory-models/mmcc_parse_options.cpp @@ -95,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" @@ -107,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/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