Remove `binary_name` option (#6693)

The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index caa0340bd2e998d0c1b10cd089340316b6cd3a93..697501d13361dda776ea563848aa0a0ae4cb0988 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -57,7 +57,7 @@ thread_local Options* pOptions;
 const char* progPath;
 
 /** Just the basename component of argv[0] */
-const std::string* progName;
+std::string progName;
 
 /** A pointer to the CommandExecutor (the signal handlers need it) */
 std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
@@ -80,7 +80,7 @@ TotalTimer::~TotalTimer()
 
 void printUsage(Options& opts, bool full) {
   stringstream ss;
-  ss << "usage: " << options::getBinaryName(opts) << " [options] [input-file]"
+  ss << "usage: " << progName << " [options] [input-file]"
      << endl
      << endl
      << "Without an input file, or with `-', cvc5 reads from standard input."
@@ -106,13 +106,11 @@ int runCvc5(int argc, char* argv[], Options& opts)
   progPath = argv[0];
 
   // Parse the options
-  vector<string> filenames = Options::parseOptions(&opts, argc, argv);
+  std::vector<string> filenames =
+      Options::parseOptions(&opts, argc, argv, progName);
 
   auto limit = install_time_limit(opts);
 
-  string progNameStr = options::getBinaryName(opts);
-  progName = &progNameStr;
-
   if (opts.driver.help)
   {
     printUsage(opts, true);

diff --git a/src/main/main.h b/src/main/main.h
index 54abbdbe980733dcc66939775975904163f54ad6..14d99f79cc18136b836085ee17bc078045fdd4ad 100644 (file)
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -34,7 +34,7 @@ class CommandExecutor;
 extern const char* progPath;
 
 /** Just the basename component of argv[0] */
-extern const std::string* progName;
+extern std::string progName;
 
 /** A reference for use by the signal handlers to print statistics */
 extern std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;

diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index d0628e2a7b4c55ecbcbb5bd14ebc81f80be8d138..b65600eb5fb39128abe2ffc0995b636aeb2e6fd6 100644 (file)
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -136,14 +136,14 @@ void segv_handler(int sig, siginfo_t* info, void* c)
     safe_print(STDERR_FILENO,
                "Spinning so that a debugger can be connected.\n");
     safe_print(STDERR_FILENO, "Try:  gdb ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, " ");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, "\n");
     safe_print(STDERR_FILENO, " or:  gdb --pid=");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, " ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, "\n");
     for (;;)
     {
@@ -191,14 +191,14 @@ void ill_handler(int sig, siginfo_t* info, void*)
     safe_print(STDERR_FILENO,
                "Spinning so that a debugger can be connected.\n");
     safe_print(STDERR_FILENO, "Try:  gdb ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, " ");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, "\n");
     safe_print(STDERR_FILENO, " or:  gdb --pid=");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, " ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, "\n");
     for (;;)
     {

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 7b2cde54acea0cf6f51c0d0b6d7e96f8f6e85383..f9d1c1a187e4c36a35ba2e80f74cd33bc086daa3 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -1,11 +1,6 @@
 id     = "BASE"
 name   = "Base"
 
-[[option]]
-  name       = "binary_name"
-  category   = "undocumented"
-  type       = "std::string"
-
 [[option]]
   name       = "in"
   category   = "undocumented"

diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
index 7d72496aa94a43868797c0b9837e9cd11bae718c..35e891f5ab5eafb4acc6f46174ed3830e65dd9b4 100644 (file)
--- a/src/options/options_public.cpp
+++ b/src/options/options_public.cpp
@@ -103,10 +103,6 @@ int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; }
 std::istream* getIn(const Options& opts) { return opts.base.in; }
 std::ostream* getErr(const Options& opts) { return opts.base.err; }
 std::ostream* getOut(const Options& opts) { return opts.base.out; }
-const std::string& getBinaryName(const Options& opts)
-{
-  return opts.base.binary_name;
-}
 
 void setInputLanguage(InputLanguage val, Options& opts)
 {

diff --git a/src/options/options_public.h b/src/options/options_public.h
index 9b549601f7ea1839897757fcaa6bbf7eeced3756..1d2f9edba8ee1a04d880c99b28a84c2d3d6c7e06 100644 (file)
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -55,7 +55,6 @@ int32_t getVerbosity(const Options& opts) CVC5_EXPORT;
 std::istream* getIn(const Options& opts) CVC5_EXPORT;
 std::ostream* getErr(const Options& opts) CVC5_EXPORT;
 std::ostream* getOut(const Options& opts) CVC5_EXPORT;
-const std::string& getBinaryName(const Options& opts) CVC5_EXPORT;
 
 void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT;
 void setOut(std::ostream* val, Options& opts) CVC5_EXPORT;

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 0d6b7f01b6a3dd639494300910d269eaecda06d1..e909a5f0a73de6544dd026236dfed8b297508071 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -364,7 +364,8 @@ public:
  */
 std::vector<std::string> Options::parseOptions(Options* options,
                                                int argc,
-                                               char* argv[])
+                                               char* argv[],
+                                               std::string& binaryName)
 {
   Assert(options != NULL);
   Assert(argv != NULL);
@@ -386,7 +387,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
   if(x != NULL) {
     progName = x + 1;
   }
-  options->base.binary_name = std::string(progName);
+  binaryName = std::string(progName);
 
   std::vector<std::string> nonoptions;
   options->parseOptionsRecursive(argc, argv, &nonoptions);

diff --git a/src/options/options_template.h b/src/options/options_template.h
index 76c599d23b14a98ccd4a95c7153977b2a98bc5e2..e9a4a6999cf47f9ccc99a430ffb0332ab0ecc345 100644 (file)
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -174,7 +174,8 @@ public:
    */
   static std::vector<std::string> parseOptions(Options* options,
                                                int argc,
-                                               char* argv[]);
+                                               char* argv[],
+                                               std::string& binaryName);
 
   /**
    * Get the setting for all options.

diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 94a2e5fb641ac3a3b3531602535ad325c807ce31..98fabc727f680153550c6c05072fd67b28482a07 100644 (file)
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -67,7 +67,8 @@ class TestNodeBlackNode : public TestNode
     char* argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-lang=ast");
-    Options::parseOptions(&opts, 2, argv);
+    std::string progName;
+    Options::parseOptions(&opts, 2, argv, progName);
     free(argv[0]);
     free(argv[1]);
     d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));