diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/Makefile.am | 8 | ||||
-rw-r--r-- | src/main/command_executor.cpp | 4 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 4 | ||||
-rw-r--r-- | src/main/options_handlers.h | 12 | ||||
-rw-r--r-- | src/main/util.cpp | 20 |
5 files changed, 34 insertions, 14 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 952951655..64a43eb02 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -41,9 +41,9 @@ pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS) if STATIC_BINARY -pcvc4_LINK = $(CXXLINK) -all-static +pcvc4_LINK = $(CXXLINK) -all-static $(pcvc4_LDFLAGS) else -pcvc4_LINK = $(CXXLINK) +pcvc4_LINK = $(CXXLINK) $(pcvc4_LDFLAGS) endif endif @@ -87,8 +87,8 @@ clean-local: rm -f $(BUILT_SOURCES) if STATIC_BINARY -cvc4_LINK = $(CXXLINK) -all-static +cvc4_LINK = $(CXXLINK) -all-static $(cvc4_LDFLAGS) else -cvc4_LINK = $(CXXLINK) +cvc4_LINK = $(CXXLINK) $(cvc4_LDFLAGS) endif diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 14625f1d8..6a4e18b5b 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -48,7 +48,7 @@ bool CommandExecutor::doCommand(Command* cmd) return status; } else { - if(d_options[options::verbosity] > 0) { + if(d_options[options::verbosity] > 2) { *d_options[options::out] << "Invoking: " << *cmd << std::endl; } @@ -59,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd) bool CommandExecutor::doCommandSingleton(Command *cmd) { bool status = true; - if(d_options[options::verbosity] >= 0) { + if(d_options[options::verbosity] >= -1) { status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]); } else { status = smtEngineInvoke(&d_smtEngine, cmd, NULL); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 741975b11..9fa40d3ab 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -239,7 +239,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { InteractiveShell shell(*exprMgr, opts); Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); - if(Configuration::isSubversionBuild()) { + if(Configuration::isGitBuild()) { + Message() << " [" << Configuration::getGitId() << "]"; + } else if(Configuration::isSubversionBuild()) { Message() << " [" << Configuration::getSubversionId() << "]"; } Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index c2eb489ed..f14a67d5f 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -26,14 +26,20 @@ inline void showConfiguration(std::string option, SmtEngine* smt) { fputs(Configuration::about().c_str(), stdout); printf("\n"); printf("version : %s\n", Configuration::getVersionString().c_str()); - if(Configuration::isSubversionBuild()) { - printf("subversion : yes [%s r%u%s]\n", + if(Configuration::isGitBuild()) { + printf("scm : git [%s %s%s]\n", + Configuration::getGitBranchName(), + std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), + Configuration::hasGitModifications() ? + " (with modifications)" : ""); + } else if(Configuration::isSubversionBuild()) { + printf("scm : svn [%s r%u%s]\n", Configuration::getSubversionBranchName(), Configuration::getSubversionRevision(), Configuration::hasSubversionModifications() ? " (with modifications)" : ""); } else { - printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no"); + printf("scm : no\n"); } printf("\n"); printf("library : %u.%u.%u\n", diff --git a/src/main/util.cpp b/src/main/util.cpp index d4d3e96d8..a6fcddf3b 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -19,10 +19,15 @@ #include <cerrno> #include <exception> #include <string.h> + +#ifndef __WIN32__ + #include <signal.h> #include <sys/resource.h> #include <unistd.h> +#endif /* __WIN32__ */ + #include "util/exception.h" #include "options/options.h" #include "util/statistics.h" @@ -44,9 +49,6 @@ namespace CVC4 { namespace main { -size_t cvc4StackSize; -void* cvc4StackBase; - /** * If true, will not spin on segfault even when CVC4_DEBUG is on. * Useful for nightly regressions, noninteractive performance runs @@ -54,6 +56,11 @@ void* cvc4StackBase; */ bool segvNoSpin = false; +#ifndef __WIN32__ + +size_t cvc4StackSize; +void* cvc4StackBase; + /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); @@ -150,10 +157,12 @@ void ill_handler(int sig, siginfo_t* info, void*) { #endif /* CVC4_DEBUG */ } +#endif /* __WIN32__ */ + static terminate_handler default_terminator; void cvc4unexpected() { -#ifdef CVC4_DEBUG +#if defined(CVC4_DEBUG) && !defined(__WIN32__) fprintf(stderr, "\n" "CVC4 threw an \"unexpected\" exception (one that wasn't properly " "specified\nin the throws() specifier for the throwing function)." @@ -214,6 +223,7 @@ void cvc4terminate() { /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception) { +#ifndef __WIN32__ stack_t ss; ss.ss_sp = malloc(SIGSTKSZ); if(ss.ss_sp == NULL) { @@ -272,6 +282,8 @@ void cvc4_init() throw(Exception) { throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); } +#endif /* __WIN32__ */ + set_unexpected(cvc4unexpected); default_terminator = set_terminate(cvc4terminate); } |