From 57b632c70aa01c95216fd5f43338cf2d76374b4e Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 8 Jun 2021 09:05:35 +0200 Subject: [PATCH] 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(). --- src/main/driver_unified.cpp | 10 ++++------ src/main/main.h | 2 +- src/main/signal_handlers.cpp | 8 ++++---- src/options/base_options.toml | 5 ----- src/options/options_public.cpp | 4 ---- src/options/options_public.h | 1 - src/options/options_template.cpp | 5 +++-- src/options/options_template.h | 3 ++- test/unit/node/node_black.cpp | 3 ++- 9 files changed, 16 insertions(+), 25 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 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 filenames = Options::parseOptions(&opts, argc, argv); + std::vector 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 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(STDERR_FILENO, getpid()); safe_print(STDERR_FILENO, "\n"); safe_print(STDERR_FILENO, " or: gdb --pid="); safe_print(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(STDERR_FILENO, getpid()); safe_print(STDERR_FILENO, "\n"); safe_print(STDERR_FILENO, " or: gdb --pid="); safe_print(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 7b2cde54a..f9d1c1a18 100644 --- 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 7d72496aa..35e891f5a 100644 --- 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 9b549601f..1d2f9edba 100644 --- 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 0d6b7f01b..e909a5f0a 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -364,7 +364,8 @@ public: */ std::vector 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 Options::parseOptions(Options* options, if(x != NULL) { progName = x + 1; } - options->base.binary_name = std::string(progName); + binaryName = std::string(progName); std::vector nonoptions; options->parseOptionsRecursive(argc, argv, &nonoptions); diff --git a/src/options/options_template.h b/src/options/options_template.h index 76c599d23..e9a4a6999 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -174,7 +174,8 @@ public: */ static std::vector 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 94a2e5fb6..98fabc727 100644 --- 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)); -- 2.30.2