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

3 files changed, 9 insertions, 11 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index caa0340bd..697501d13 100644
--- 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 54abbdbe9..14d99f79c 100644
--- 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 d0628e2a7..b65600eb5 100644
--- 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 (;;)
     {