summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/driver_unified.cpp10
-rw-r--r--src/main/main.h2
-rw-r--r--src/main/signal_handlers.cpp8
-rw-r--r--src/options/base_options.toml5
-rw-r--r--src/options/options_public.cpp4
-rw-r--r--src/options/options_public.h1
-rw-r--r--src/options/options_template.cpp5
-rw-r--r--src/options/options_template.h3
-rw-r--r--test/unit/node/node_black.cpp3
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<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 (;;)
{
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
@@ -2,11 +2,6 @@ id = "BASE"
name = "Base"
[[option]]
- name = "binary_name"
- category = "undocumented"
- type = "std::string"
-
-[[option]]
name = "in"
category = "undocumented"
type = "std::istream*"
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<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 76c599d23..e9a4a6999 100644
--- 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 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));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback