use a string instead of macro for version number

.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

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;
 

jbmc/src/jbmc/jbmc_parse_options.cpp

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

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

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

src/cbmc/cbmc_solvers.cpp

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

src/clobber/clobber_parse_options.cpp

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

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

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;
-
-    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;
+               << " (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;
 
     return EX_OK; // Exit!
   }

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)

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

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)