replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

use a string instead of macro for version number

This commit is contained in:
Daniel Kroening 2018-07-30 22:13:27 +01:00
parent 0618f7d30a
commit ad5c3755ca
15 changed files with 110 additions and 110 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -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

4
jbmc/src/janalyzer/janalyzer_parse_options.cpp
View File

@ -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;

25
jbmc/src/jbmc/jbmc_parse_options.cpp
View File

@ -61,22 +61,22 @@ Author: Daniel Kroening, kroening@kroening.com
#include <java_bytecode/replace_java_nondet.h>
#include <java_bytecode/simple_method_stubbing.h>
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);

8
jbmc/src/jdiff/jdiff_parse_options.cpp
View File

@ -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)

29
src/cbmc/cbmc_parse_options.cpp
View File

@ -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;
//

43
src/cbmc/cbmc_solvers.cpp
View File

@ -173,13 +173,12 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
throw 0;
}
auto smt2_dec=
util_make_unique<smt2_dect>(
ns,
"cbmc",
"Generated by CBMC " CBMC_VERSION,
"QF_AUFBV",
solver);
auto smt2_dec = util_make_unique<smt2_dect>(
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::solvert> cbmc_solverst::get_smt2(
}
else if(filename=="-")
{
auto smt2_conv=
util_make_unique<smt2_convt>(
ns,
"cbmc",
"Generated by CBMC " CBMC_VERSION,
"QF_AUFBV",
solver,
std::cout);
auto smt2_conv = util_make_unique<smt2_convt>(
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::solvert> cbmc_solverst::get_smt2(
throw 0;
}
auto smt2_conv=
util_make_unique<smt2_convt>(
ns,
"cbmc",
"Generated by CBMC " CBMC_VERSION,
"QF_AUFBV",
solver,
*out);
auto smt2_conv = util_make_unique<smt2_convt>(
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;

8
src/clobber/clobber_parse_options.cpp
View File

@ -35,10 +35,10 @@ Author: Daniel Kroening, kroening@kroening.com
#include <langapi/mode.h>
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)
{
}

13
src/goto-analyzer/goto_analyzer_parse_options.cpp
View File

@ -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();

15
src/goto-cc/as_mode.cpp
View File

@ -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!
}

3
src/goto-cc/compile.cpp
View File

@ -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)

13
src/goto-cc/gcc_mode.cpp
View File

@ -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';

25
src/goto-diff/goto_diff_parse_options.cpp
View File

@ -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)

26
src/util/CMakeLists.txt
View File

@ -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)

5
src/util/Makefile
View File

@ -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)' > $@

1
src/util/version.h Normal file
View File

@ -0,0 +1 @@
extern const char *CBMC_VERSION;